[Haskell-cafe] Problems with Type family and Typeable

[Kai Zhang]

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?
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/haskell-cafe/attachments/20170731/4c1caaea/attachment.html>