#13197: Perplexing levity polymorphism issue -------------------------------------+------------------------------------- Reporter: bgamari | Owner: Type: bug | Status: new Priority: highest | Milestone: 8.2.1 Component: Compiler (Type | Version: 8.1 checker) | Resolution: | 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: | -------------------------------------+------------------------------------- Description changed by bgamari: @@ -2,2 +2,2 @@ - was merged, but sadly it seems the typechecker isn't quite clever enough - yet (or perhaps I'm the not clever one), + (along with Phab:D2038) was merged, but sadly it seems the typechecker + isn't quite clever enough yet (or perhaps I'm the not clever one), New description: I would have expected this to compile since the levity polymorphism patch (along with Phab:D2038) 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#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler