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.

  • 1
    You should probably post your edit as an answer (and roll-back the edit). – Alec Feb 15 '17 at 6:03
  • The general issue seems to be that, while GADT pattern matching provides equality constraints, it never provides inequality constraints, so we can't convince GHC that the first clause of the closed type family is not taken. We probably need more support from GHC to do that in the future, AFAICS. – chi Feb 15 '17 at 9:11
  • Ugh, you can tell just from looking at the type that this isn't going to be easy to prove, even with an inductive Nat (rather than the broken one in GHC.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:20
  • @BenjaminHodgson I 've been rewriting this over and over for a few days so suggestions are indeed welcome. I am building a Generic1 typeclass that should have the structure E 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 the Ois from a given arity i in a type safe way. So (for some notion of i :: Nat) getOp :: Proxy i -> e s -> Maybe (OpType i e). Since i is 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:53
  • @BenjaminHodgson so here is the problem: I need to traverse the tree with type level Nat (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
up vote 2 down vote accepted

One possible solution is to use the singletons library to get term-level functions representing the type-level ones (or vice-versa).

The gist of it is:

import Data.Singletons.Prelude

(...)

case (sing :: Sing a) %:== (sing :: Sing b) of
  STrue  -> Left Refl
  SFalse -> Right Refl

I've put up a self-contained file with all the imports and language extensions too.

  • Thanks a lot! Is %:== undocumented? I can't find it. – fakedrake Feb 15 '17 at 14:55
  • 1
    Data.Singletons.Prelude re-exports Data.Singletons.Prelude.Eq where you can find (%:==) – gallais Feb 15 '17 at 15:17

Your Answer

 

By clicking "Post Your Answer", you acknowledge that you have read our updated terms of service, privacy policy and cookie policy, and that your continued use of the website is subject to these policies.

Not the answer you're looking for? Browse other questions tagged or ask your own question.