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@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@haskell.org | http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs