[Haskell-cafe] Problems with Type family and Typeable
Kai Zhang
zk65900931 at gmail.com
Mon Jul 31 18:34:18 UTC 2017
I think this question was answered here:
https://stackoverflow.com/questions/32408110/datakinds-and-type-class-instances
On Mon, Jul 31, 2017 at 10:07 AM Kai Zhang <zk65900931 at gmail.com> wrote:
> Thanks! Could you elaborate a little more about the Typeable constraint?
> What argument does it add during runtime? In the beginning I thought this
> constraint is redundant, as what it claims is always true in this case. If
> my understanding is correct, the purpose of this constraint is to tell GHC
> to retain the necessary type annotations in runtime?
>
>
> On Mon, Jul 31, 2017 at 5:41 AM Li-yao Xia <lysxia at gmail.com> wrote:
>
>> 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.
>>
>>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/haskell-cafe/attachments/20170731/6bdee15d/attachment.html>
More information about the Haskell-Cafe
mailing list