[Haskell-cafe] Problems with Type family and Typeable

[Li-yao Xia]

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.