[Haskell-cafe] Problems with Type family and Typeable

[Dmitry Olshansky]

Additionally, as I understand now, you will have better compile-time
performance if write

type Elem x xs = Elem' 'False x xs

type family Elem' (b::Bool) x  xs :: Bool where
    Elem' 'True _ _ = 'True
    Elem' 'False a (x ': xs) = Elem' (a == x) a xs
    Elem' 'False _ '[] = 'False

All type calculation is not enough lazy!

2017-07-31 15:41 GMT+03:00 Li-yao Xia <lysxia at gmail.com>:

> Hello,
>
>
> "Data.Type.Equality.EqStar s t || Elem s ts" resolves to True or False,
> which are values of type Bool.
> To understand why that constraint can't be solved, think about how such a
> function is compiled. At run time, types are erased.
> A "Proxy p" value carries no more information than unit "()", and a
> "Tagged _ a" value is in fact just an "a" value.
> So elemTag is compiled to something equivalent to a function of this type,
> which has no way of performing the comparison you requested since the
> type-level boolean was erased:
>
>     -- Original function
>     elemTag :: Proxy s -> Tagged (t ': ts) a -> Bool
>
>     -- After type erasure
>     elemTag :: () -> a -> Bool
>
> As suggested by the type error, you can reify the boolean "Elem s (t ':
> ts)" by adding a Typeable constraint, which gets compiled to an additional
> run time argument.
>
>     elemTag :: forall a s t ts
>             .  Typeable (Elem s (t ': ts))
>             => Proxy s
>             -> Tagged (t ': ts) a
>             -> Bool
>
>
> Li-yao
>
>
>
>
> On 07/31/2017 07:15 AM, Kai Zhang wrote:
>
>> I got an error when compiling the following codes:
>>
>> {-# LANGUAGE TypeOperators #-}
>> {-# LANGUAGE DataKinds #-}
>> {-# LANGUAGE TypeFamilies #-}
>> {-# LANGUAGE ScopedTypeVariables #-}
>> {-# LANGUAGE UndecidableInstances #-}
>>
>> import Data.Type.Bool
>> import Data.Type.Equality
>> import Data.Tagged (Tagged(..))
>> import Data.Typeable
>>
>> type family Elem x  xs :: Bool where
>>      Elem _ '[] = 'False
>>      Elem a (x ': xs) = a == x || Elem a xs
>>
>> elemTag :: forall a s t ts . Proxy s
>>          -> Tagged (t ': ts) a -> Bool
>> elemTag _ _ = if typeOf (Proxy :: Proxy (Elem s (t ': ts))) == typeOf
>> (Proxy :: Proxy 'True)
>>                   then True
>>                   else False
>>
>> GHC says:
>>
>> • No instance for (Typeable
>>                           (Data.Type.Equality.EqStar s t || Elem s ts))
>>          arising from a use of ‘typeOf’
>>      • In the first argument of ‘(==)’, namely
>>          ‘typeOf (Proxy :: Proxy (Elem s (t : ts)))’
>>        In the expression:
>>          typeOf (Proxy :: Proxy (Elem s (t : ts)))
>>          == typeOf (Proxy :: Proxy True)
>>        In the expression:
>>          if typeOf (Proxy :: Proxy (Elem s (t : ts)))
>>             == typeOf (Proxy :: Proxy True) then
>>              True
>>          else
>>              False
>>
>> My question: why is ghc unable to deduce that "Data.Type.Equality.EqStar s
>> t || Elem s ts" resolves to "Bool" which should be an instance of
>> Typeable?
>> How to fix this?
>>
>>
>>
>> _______________________________________________
>> Haskell-Cafe mailing list
>> To (un)subscribe, modify options or view archives go to:
>> http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
>> Only members subscribed via the mailman list are allowed to post.
>>
>
> _______________________________________________
> Haskell-Cafe mailing list
> To (un)subscribe, modify options or view archives go to:
> http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
> Only members subscribed via the mailman list are allowed to post.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/haskell-cafe/attachments/20170731/df71f8a3/attachment.html>