<div dir="ltr">I got an error when compiling the following codes:<div><br></div><div><div>{-# LANGUAGE TypeOperators #-}</div><div>{-# LANGUAGE DataKinds #-}</div><div>{-# LANGUAGE TypeFamilies #-}</div><div>{-# LANGUAGE ScopedTypeVariables #-}</div><div>{-# LANGUAGE UndecidableInstances #-}</div><div><br></div><div>import Data.Type.Bool</div><div>import Data.Type.Equality</div><div>import Data.Tagged (Tagged(..))</div><div>import Data.Typeable</div><div><br></div><div>type family Elem x  xs :: Bool where</div><div>    Elem _ '[] = 'False</div><div>    Elem a (x ': xs) = a == x || Elem a xs</div><div><br></div><div>elemTag :: forall a s t ts . Proxy s</div><div>        -> Tagged (t ': ts) a -> Bool</div><div>elemTag _ _ = if typeOf (Proxy :: Proxy (Elem s (t ': ts))) == typeOf (Proxy :: Proxy 'True)</div><div>                 then True</div><div>                 else False</div></div><div><br></div><div>GHC says:</div><div><br></div><div><div>• No instance for (Typeable</div><div>                         (Data.Type.Equality.EqStar s t || Elem s ts))</div><div>        arising from a use of ‘typeOf’</div><div>    • In the first argument of ‘(==)’, namely</div><div>        ‘typeOf (Proxy :: Proxy (Elem s (t : ts)))’</div><div>      In the expression:</div><div>        typeOf (Proxy :: Proxy (Elem s (t : ts)))</div><div>        == typeOf (Proxy :: Proxy True)</div><div>      In the expression:</div><div>        if typeOf (Proxy :: Proxy (Elem s (t : ts)))</div><div>           == typeOf (Proxy :: Proxy True) then</div><div>            True</div><div>        else</div><div>            False</div></div><div><br></div><div>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?</div></div>