<div dir="ltr">I think this question was answered here: <a href="https://stackoverflow.com/questions/32408110/datakinds-and-type-class-instances">https://stackoverflow.com/questions/32408110/datakinds-and-type-class-instances</a><br><br><div class="gmail_quote"><div dir="ltr">On Mon, Jul 31, 2017 at 10:07 AM Kai Zhang <<a href="mailto:zk65900931@gmail.com">zk65900931@gmail.com</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div dir="ltr">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? </div><div dir="ltr"><br><br><div class="gmail_quote"><div dir="ltr">On Mon, Jul 31, 2017 at 5:41 AM Li-yao Xia <<a href="mailto:lysxia@gmail.com" target="_blank">lysxia@gmail.com</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">Hello,<br>
<br>
<br>
"Data.Type.Equality.EqStar s t || Elem s ts" resolves to True or False, which are values of type Bool.<br>
To understand why that constraint can't be solved, think about how such a function is compiled. At run time, types are erased.<br>
A "Proxy p" value carries no more information than unit "()", and a "Tagged _ a" value is in fact just an "a" value.<br>
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:<br>
<br>
     -- Original function<br>
     elemTag :: Proxy s -> Tagged (t ': ts) a -> Bool<br>
<br>
     -- After type erasure<br>
     elemTag :: () -> a -> Bool<br>
<br>
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.<br>
<br>
     elemTag :: forall a s t ts<br>
             .  Typeable (Elem s (t ': ts))<br>
             => Proxy s<br>
             -> Tagged (t ': ts) a<br>
             -> Bool<br>
<br>
<br>
Li-yao<br>
<br>
<br>
<br>
On 07/31/2017 07:15 AM, Kai Zhang wrote:<br>
> I got an error when compiling the following codes:<br>
><br>
> {-# LANGUAGE TypeOperators #-}<br>
> {-# LANGUAGE DataKinds #-}<br>
> {-# LANGUAGE TypeFamilies #-}<br>
> {-# LANGUAGE ScopedTypeVariables #-}<br>
> {-# LANGUAGE UndecidableInstances #-}<br>
><br>
> import Data.Type.Bool<br>
> import Data.Type.Equality<br>
> import Data.Tagged (Tagged(..))<br>
> import Data.Typeable<br>
><br>
> type family Elem x  xs :: Bool where<br>
>      Elem _ '[] = 'False<br>
>      Elem a (x ': xs) = a == x || Elem a xs<br>
><br>
> elemTag :: forall a s t ts . Proxy s<br>
>          -> Tagged (t ': ts) a -> Bool<br>
> elemTag _ _ = if typeOf (Proxy :: Proxy (Elem s (t ': ts))) == typeOf<br>
> (Proxy :: Proxy 'True)<br>
>                   then True<br>
>                   else False<br>
><br>
> GHC says:<br>
><br>
> • No instance for (Typeable<br>
>                           (Data.Type.Equality.EqStar s t || Elem s ts))<br>
>          arising from a use of ‘typeOf’<br>
>      • In the first argument of ‘(==)’, namely<br>
>          ‘typeOf (Proxy :: Proxy (Elem s (t : ts)))’<br>
>        In the expression:<br>
>          typeOf (Proxy :: Proxy (Elem s (t : ts)))<br>
>          == typeOf (Proxy :: Proxy True)<br>
>        In the expression:<br>
>          if typeOf (Proxy :: Proxy (Elem s (t : ts)))<br>
>             == typeOf (Proxy :: Proxy True) then<br>
>              True<br>
>          else<br>
>              False<br>
><br>
> My question: why is ghc unable to deduce that "Data.Type.Equality.EqStar s<br>
> t || Elem s ts" resolves to "Bool" which should be an instance of Typeable?<br>
> How to fix this?<br>
><br>
><br>
><br>
> _______________________________________________<br>
> Haskell-Cafe mailing list<br>
> To (un)subscribe, modify options or view archives go to:<br>
> <a href="http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe" rel="noreferrer" target="_blank">http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe</a><br>
> Only members subscribed via the mailman list are allowed to post.<br>
<br>
</blockquote></div></div></blockquote></div></div>