Prove that (1 + k) ~ 0 and (k + 1) ~ 0 are unsatisfiable

[RyanGlScott]

Disclaimer: I don't know if GHC typechecker plugins have the power to do what I'm seeking, so if the answer is "no", feel free to close this issue. That being said, sometimes I feel masochistic adventurous and try to do inductive-style definitions over Nat. Inevitably, I run into the sort of trouble that is exemplified in the code below:

{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeInType #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
{-# OPTIONS_GHC -fplugin GHC.TypeLits.Normalise #-}

import Data.Type.Equality
import GHC.TypeNats

type family Replicate (n :: Nat) (x :: a) :: [a] where
  Replicate 0 _ = '[]
  Replicate n x = x : Replicate (n - 1) x

replicateSucc :: (Replicate (k + 1) x) :~: (x : Replicate k x)
replicateSucc = Refl

Alas, replicateSucc doesn't typecheck. GHC can't reduce Replicate (k + 1) x because it's not sure if k + 1 equals 0 or not, so Replicate gets stuck. Intuitively, k + 1 is never equal to 0, but the typechecker is sadly unaware of this fact.

My question is: can we leverage the power of ghc-typelits-natnormalise to accomplish this? This is a bit of different territory for ghc-typelits-natnormalise, which is normally used to conclude that things are equal, but here, we want to inform the typechecker that k + 1 is not equal to 0 (and similarly, 1 + k is not equal to 0).

[adamgundry]

I suspect this is tricky given the way type-checker plugins and closed type families interact, unfortunately. There isn't a way to directly hook into the evaluation of Replicate (k + 1) x to make it reduce, nor a first-class way to express the required apartness constraint. In principle, a plugin could look for stuck closed type family applications and implement its own fall-through pattern-matching based on a custom apartness relation, but it's decidedly nontrivial...

[RyanGlScott]

I was afraid that might be the case. In any event, thanks for entertaining the idea!