#13197: Perplexing levity polymorphism issue -------------------------------------+------------------------------------- Reporter: bgamari | Owner: Type: bug | Status: new Priority: highest | Milestone: 8.2.1 Component: Compiler | Version: 8.1 (Type checker) | Keywords: typeable | Operating System: Unknown/Multiple Architecture: | Type of failure: GHC rejects Unknown/Multiple | valid program Test Case: | Blocked By: Blocking: | Related Tickets: Differential Rev(s): | Wiki Page: -------------------------------------+------------------------------------- I would have expected this to compile since the levity polymorphism patch was merged, but sadly it seems the typechecker isn't quite clever enough yet (or perhaps I'm the not clever one), {{{#!hs {-# 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 }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13197 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler