TypeLits and type families wrt. equality

[Gabor Greif]

Hi Anthony,

while I suspected that one would need to go the "value inference"
route (i.e. type classes), I had no idea how to get started. So thanks
for your snippet, it is very helpful.

Otoh, it only strips one segment

``` haskell
*GaborTEq> showPath $ stripOut (Proxy :: Proxy "Hey") (Longer (Proxy
:: Proxy "Du") $ Longer (Proxy :: Proxy "Hey") $ Longer (Proxy ::
Proxy "Bee") $ Longer (Proxy :: Proxy "Hey") $ Longer (Proxy :: Proxy
"Hey") $ Empty)
"Du -> Bee -> Hey -> Hey"
```
I'll play around a bit with FDs and see what I can figure out to make this work.

Cheers,

    Gabor


On 7/24/15, Anthony Cowley <acowley at gmail.com> wrote:
>
> 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
>
> _______________________________________________
> ghc-devs mailing list
> ghc-devs at haskell.org
> http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
>