TypeLits and type families wrt. equality

[Simon Peyton Jones]

Yes. Here's a simpler example:

=====================================
type family Equal a b where
  Equal a a = 'True
  Equal a b = 'False

foo :: Proxy 'True -> Bool
foo x = True

f :: forall a b. Maybe (a :~: b) -> Bool
f x = case x of
        Just Refl -> True
        Nothing   -> foo (undefined :: Proxy (Equal a b))
=====================================

In the 'Nothing' branch of the case, we know that a is not equal to b; but we don't exploit that negative information when trying to reduce (Equal a b).

Making type inference (and system FC) exploit negative info would be a Big Deal, I think.

Simon

|  -----Original Message-----
|  From: ghc-devs [mailto:ghc-devs-bounces at haskell.org] On Behalf Of
|  Gabor Greif
|  Sent: 24 July 2015 16:02
|  To: ghc-devs; Richard Eisenberg
|  Subject: TypeLits and type families wrt. equality
|  
|  Hi all!
|  
|  I have a problem with following disconnect: equalities for types as
|  detectable by type families, while I am missing a convincing technique
|  to do the same at the value level. (convincing means here: without
|  resorting to unsafeCoerce)
|  
|  Here is a demo snippet illustrating the issue. Try to get the
|  commented line to compile without using unsafeCoerce.
|  
|  ##############################################################
|  {-# LANGUAGE DataKinds, GADTs, TypeOperators
|             , KindSignatures, ScopedTypeVariables, TypeFamilies #-}
|  
|  import Data.Type.Equality
|  import GHC.TypeLits
|  import Data.Proxy
|  
|  data Path (names :: [Symbol]) where
|    Empty :: Path '[]
|    Longer :: KnownSymbol name => Proxy name -> Path names -> Path (name
|  ': names)
|  
|  type family StripOut (name :: Symbol) (path :: [Symbol]) where
|    StripOut name '[] = '[]
|    StripOut name (name ': ns) = StripOut name ns
|    StripOut n (name ': ns) = n ': StripOut name ns
|  
|  stripOut :: KnownSymbol name => Proxy name -> Path names -> Path
|  (StripOut name names)
|  stripOut _ Empty = Empty
|  stripOut n (Longer n' path) | Just Refl <- n `sameSymbol` n' =
|  stripOut n path
|  --stripOut n (Longer n' path) = Longer n' (stripOut n path)
|  ##############################################################
|  
|  I get the error reproduced at the end of this message.
|  
|  My suspicion is that we need to model type inequality (with a new
|  built-in eliminator, perhaps?) that helps us to skip the equation
|  "StripOut name (name ': ns) = StripOut name ns" in the case when
|  sameSymbol would return Nothing.
|  
|  Any ideas?
|  
|  Cheers and thanks
|  
|      Gabor
|  
|  
|  -----------------------------------------------------
|  
|  
|  Lits.hs:20:31: error:
|      Could not deduce: StripOut name (name1 : names1)
|                        ~ (name1 : StripOut name names1)
|      from the context: (names ~ (name1 : names1), KnownSymbol name1)
|        bound by a pattern with constructor:
|                   Longer :: forall (name :: Symbol) (names ::
|  [Symbol]).
|                             KnownSymbol name =>
|                             Proxy name -> Path names -> Path (name :
|  names),
|                 in an equation for  stripOut
|        at Lits.hs:20:13-26
|      Expected type: Path (StripOut name names)
|        Actual type: Path (name1 : StripOut name names1)
|      Relevant bindings include
|        path :: Path names1
|          (bound at Lits.hs:20:23)
|        n' :: Proxy name1
|          (bound at Lits.hs:20:20)
|        n :: Proxy name
|          (bound at Lits.hs:20:10)
|        stripOut :: Proxy name -> Path names -> Path (StripOut name
|  names)
|          (bound at Lits.hs:18:1)
|      In the expression: Longer n' (stripOut n path)
|      In an equation for  stripOut :
|          stripOut n (Longer n' path) = Longer n' (stripOut n path)
|  Failed, modules loaded: none.
|  _______________________________________________
|  ghc-devs mailing list
|  ghc-devs at haskell.org
|  http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs