I am trying to fill the hole in the following snippet
import Data.Proxy
import GHC.TypeLits
import Data.Type.Equality
import Data.Type.Bool
import Unsafe.Coerce
ifThenElse :: forall (a :: Nat) (b :: Nat) x l r.
(KnownNat a, KnownNat b, x ~ If (a==b) l r) =>
Proxy a -> Proxy b -> Either (x :~: l) (x :~: r)
ifThenElse pa pb = case sameNat pa pb of
Just Refl -> Left Refl
Nothing -> Right $ unsafeCoerce Refl -- This was the hole
Is it possible?
Edit: Checked the source of sameNat and it turns out they use unsafeCoerce. I edited the code above accordingly.
Nat(rather than the broken one inGHC.TypeLits). How did you manage to paint yourself into this particular corner? We might be able to advise you on how to redesign your program so that you don't need such gnarly proofs. – Benjamin Hodgson♦ Feb 15 '17 at 10:20Generic1typeclass that should have the structureE s = E0 s | E1 O1 (E s) | E2 O2 (E s) | ...I have implemented various generic functionalities over this so it seems to be working. I want a safe way to extract theOis from a given arityiin a type safe way. So (for some notion ofi :: Nat)getOp :: Proxy i -> e s -> Maybe (OpType i e). Sinceiis known at compile time GHC can (and does) infer what the exact type of the above signature on each call site is. – fakedrake Feb 15 '17 at 13:53Nat(which can be easily converted from arity to tree depth) because GHC needs to be able to typecheck each step, so I need to tell her (I see it as a mother fiure) how to figure out the types. – fakedrake Feb 15 '17 at 14:10