Unit is not ()

gistfile1.hs

{-# LANGUAGE TypeFamilies, GADTs, EmptyDataDecls #-}

data Empty

data Unit = Unit

data Equal a b where
  Refl :: Equal a a

type family F a :: *
type instance F Unit = Unit
type instance F () = Empty

newtype Wrap a = Wrap { unwrap :: F a }

subst :: Equal a b -> p a -> p b
subst Refl = id

proof :: Equal Unit () -> Empty
proof eq = unwrap . subst eq . Wrap $ Unit