TypeLits and type families wrt. equality

[Gabor Greif]

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.