Perplexing levity polymorphism issue
I would have expected this to compile since the levity polymorphism patch (along with D2038) was merged, but sadly it seems the typechecker isn't quite clever enough yet (or perhaps I'm the not clever one),
{-# LANGUAGE GADTs, PolyKinds, PatternSynonyms, RankNTypes,
TypeOperators, ViewPatterns #-}
{-# LANGUAGE TypeInType #-}
module Test where
import Data.Kind
import GHC.Exts
data TypeRep (a :: k) where
TypeCon :: String -> TypeRep a
TypeApp :: forall k1 k2 (f :: k1 -> k2) (x :: k1). TypeRep f -> TypeRep x -> TypeRep (f x)
TypeFun :: forall r1 r2 (a :: TYPE r1) (b :: TYPE r2). TypeRep a -> TypeRep b -> TypeRep (a -> b)
data SomeTypeRep where
SomeTypeRep :: forall k (a :: k). TypeRep a -> SomeTypeRep
data (a :: k1) :~~: (b :: k2) where
HRefl :: a :~~: a
eqTypeRep :: TypeRep (a :: k1) -> TypeRep (b :: k2) -> Maybe (a :~~: b)
eqTypeRep = undefined
typeRepKind :: forall (k :: *). forall (a :: k). TypeRep a -> TypeRep k
typeRepKind = undefined
toApp :: SomeTypeRep -> SomeTypeRep -> Maybe SomeTypeRep
toApp (SomeTypeRep f) (SomeTypeRep a)
| TypeFun arg res <- typeRepKind f
, Just HRefl <- arg `eqTypeRep` typeRepKind a
= Just $ SomeTypeRep (TypeApp f a)
toApp _ _ = Nothing