Re: TypeLits and type families wrt. equality

24 Jul 2015


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

Re: TypeLits and type families wrt. equality

Anthony Cowley