TypeLits and type families wrt. equality

[Gabor Greif]

Simon,

yes, this is the the same problem. You probably meant:

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

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

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

When saying "Big Deal" did you mean
  - highly desirable and somebody should go for it
  - or a terrible amount of work, and who tackles it is probably a
fool on a hubris trip?

(I still have my problems deciphering British irony.)

I guess a full-blown solution is too much work for now (also considering
previous comments from Richard). But what about a simpler construct

decideRefl :: Proxy (a :: Symbol) -> Proxy b
               -> Proxy (Equal a b :~: 'False)
               -> Either (Equal a b :~: 'False) (a :~: b)

The Right case is just rewrapping the Refl from a `sameSymbol`, while
the Left injection
would suppress the clause "Equal a a = 'True" from the type family,
knowing that it cannot contribute to an outcome, arriving at the 'False result.

(I have no idea how this could be represented in Core, though.)

What do you think?

Cheers,

    Gabor

On 7/27/15, Simon Peyton Jones <simonpj at microsoft.com> wrote:
> 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
>