TypeLits and type families wrt. equality

[Anthony Cowley]

I think you are already very familiar with what I'll show here, but I figured I'd offer this alternative approach just in case. It does not directly address your type error, but does show one way of loosely steering values from the type level.

https://gist.github.com/acowley/57724b6facd6a39a196f

Anthony

Gabor Greif writes:

> 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