Haskell could not unify type instance equations

ghc, haskell

Solution

I don't think GADT pattern match refinement works this way round. You have `Opp p` as the result type of a constructor. So if you write something like

f :: Nat 'Even -> ...
f (Succ n) = ...

then the type checker knows that `Nat (Opp t) ~ Nat 'Even` and therefore `Opp t ~ 'Even`. But to solve this, the type checker has to invert the function `Opp`, which is asking a lot.

I suggest you change the definition of `Nat` to say:

data Nat :: Parity -> * where
  Zero :: Nat 'Even
  Succ :: Nat (Opp p) -> Nat p

This should just work.

Edit

Actually, let me expand slightly.

The suggestion above is not without a (minor) price. You lose a bit of type inference. For example, the type of `Succ Zero` is now `Succ Zero :: Opp p ~ 'Even => Nat p` and not `Nat 'Odd`. With an explicit type annotation, it resolves ok.

You can improve on this by adding a constraint to `Succ` that requires that `Opp` is self-inverse. The only two elements of `Parity` are `Even` and `Odd`, and for these the constraint holds, so it should never cause any problems:

data Nat :: Parity -> * where
  Zero :: Nat 'Even
  Succ :: (Opp (Opp p) ~ p) => Nat (Opp p) -> Nat p

Now `Succ Zero` is inferred to be of type `Nat 'Odd`, and the pattern match still works.

Problem

I am trying to tag canonical Nat datatype with (Even/Odd) Parity kind to see if we can get any free theorems. Here is the code: ``` {-# LANGUAGE GADTs #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE DataKinds #-} -- Use DataKind promotion with type function for even-odd module EvenOdd where data Parity = Even | Odd -- Parity is promoted to kind level Parity. -- Even & Odd to type level 'Even & 'Odd of kind Parity -- We define type-function opp to establish the relation that -- type 'Even is opposite of 'Odd, and vice-versa type family Opp (n :: Parity) :: Parity type instance Opp 'Even = 'Odd type instance Opp 'Odd = 'Even -- We tag natural number with the type of its parity data Nat :: Parity -> * where Zero :: Nat 'Even Succ :: Nat p -> Nat (Opp p) -- Now we (should) get free theorems. -- 1. Plus of two even numbers is even evenPlus :: Nat 'Even -> Nat 'Even -> Nat 'Even evenPlus Zero n2 = n2 -- Line 31 evenPlus (Succ (Succ n1)) n2 = Succ (Succ (evenPlus n1 n2)) ``` However, GHC throws type error: ``` Could not deduce (p1 ~ 'Even) from the context ('Even ~ Opp p) bound by a pattern with constructor Succ :: forall (p :: Parity). Nat p -> Nat (Opp p), in an equation for `evenPlus' at even-odd.hs:31:13-26 or from (p ~ Opp p1) bound by a pattern with constructor Succ :: forall (p :: Parity). Nat p -> Nat (Opp p), in an equation for `evenPlus' at even-odd.hs:31:19-25 `p1' is a rigid type variable bound by a pattern with constructor Succ :: forall (p :: Parity). Nat p -> Nat (Opp p), in an equation for `evenPlus' at even-odd.hs:31:19 Expected type: Nat 'Even Actual type: Nat p In the first argument of `evenPlus', namely `n1' In the first argument of `Succ', namely `(evenPlus n1 n2)' ``` As I understand it, the gist of the above error is that GHC was unable to deduce (p1 ~ 'Even), when the context has the equation: ((Opp (Opp p1)) ~ 'Even). Why does this happen? Is there something wrong with my approach?

Original source