CODEWITHSUNDEEP
haskellvoidtype-families
fakedrake
fakedrake

Reputation: 6856

Convincing GHC that `Maybe Void` is a unit type

I have a type family IfEq (n :: Nat) (m :: Nat) o that evaluates to o or Void depending on wether n :== m. Since Maybe Void is only inibited by Nothing I should be able to define a function Maybe (IfEq n m o) -> Maybe o but I can't figure it out.

Follow up: Can this generalized from the Maybe monad to a more general type? (eg. all MonadPluss)

EDIT: I had initially rolled my own Nat but (thank's to @chi) with the GHC Nat kind KnownNat constrait it pretty straightforward to do what I describe above. However GHC can not infer KnownNat a => KnownNat (1+a) which is imperative to me so I am back at square 1.

Upvotes: 1

Views: 127

Answers (1)

chi
chi

Reputation: 116174

Try something like

foo :: forall n m o . (KnownNat n, KnownNat m) =>
       IfEq n m o -> Maybe o
foo x = case sameNat (Proxy :: Proxy n) (Proxy :: Proxy m) of
   Just Refl -> Just x
   Nothing -> Nothing

Upvotes: 2

Related Questions