[GHC] #13197: Perplexing levity polymorphism issue
#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
#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
#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: | -------------------------------------+------------------------------------- Comment (by bgamari): For the record the above fails with, {{{ Test.hs:34:33: error: • Could not deduce: (r2 :: RuntimeRep) ~~ ('LiftedRep :: RuntimeRep) from the context: ((* :: *) ~~ (* :: *), (k :: *) ~~ ((a2 -> b) :: *)) bound by a pattern with constructor: TypeFun :: forall (a :: TYPE r1) (b :: TYPE r2). TypeRep (TYPE r1) a -> TypeRep (TYPE r2) b -> TypeRep * (a -> b), in a pattern binding in pattern guard for an equation for ‘toApp’ at Test.hs:32:5-19 or from: ((* :: *) ~~ (TYPE r1 :: *), (k1 :: *) ~~ (a2 :: TYPE r1)) bound by a pattern with constructor: HRefl :: forall k2 (a :: k2). (:~~:) k2 k2 a a, in a pattern binding in pattern guard for an equation for ‘toApp’ at Test.hs:33:10-14 ‘r2’ is a rigid type variable bound by a pattern with constructor: TypeFun :: forall (a :: TYPE r1) (b :: TYPE r2). TypeRep (TYPE r1) a -> TypeRep (TYPE r2) b -> TypeRep * (a -> b), in a pattern binding in pattern guard for an equation for ‘toApp’ at Test.hs:32:5-19 When matching the kind of ‘b’ Expected type: TypeRep (k1 -> b) a Actual type: TypeRep k a • In the first argument of ‘TypeApp’, namely ‘f’ In the first argument of ‘SomeTypeRep’, namely ‘(TypeApp f a)’ In the second argument of ‘($)’, namely ‘SomeTypeRep (TypeApp f a)’ • Relevant bindings include res :: TypeRep (TYPE r2) b (bound at Test.hs:32:17) | 34 | = Just $ SomeTypeRep (TypeApp f a) | ^ }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13197#comment:2 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#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: | -------------------------------------+------------------------------------- Comment (by goldfire): This is expected behavior. Well, for me. After I've studied it and revised my expectation. The problem is that `k2` in the type of `TypeApp` has kind `Type`. But `f a`'s kind, `res`, has type `TYPE r2`, which we see looking at the type of `TypeFun`. So we get a type error. The fix is to convince GHC that `f a`'s type's kind is really `Type`. And we can do that with one extra check: {{{ toApp :: SomeTypeRep -> SomeTypeRep -> Maybe SomeTypeRep toApp (SomeTypeRep f) (SomeTypeRep a) | TypeFun arg res <- typeRepKind f , Just HRefl <- arg `eqTypeRep` typeRepKind a , Just HRefl <- typeRepKind res `eqTypeRep` (undefined :: TypeRep Type) = Just $ SomeTypeRep (TypeApp f a) toApp _ _ = Nothing }}} This compiles for me. Note that `arg`'s kind is discovered to be `Type` because `arg` equals the result of a `typeRepKind`, which always has kind `Type`. Fun times! GHC should really come little trophies that you can accrue by triggering certain bizarre scenarios. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13197#comment:3 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#13197: Perplexing levity polymorphism issue -------------------------------------+------------------------------------- Reporter: bgamari | Owner: Type: bug | Status: closed Priority: highest | Milestone: 8.2.1 Component: Compiler (Type | Version: 8.1 checker) | Resolution: invalid | 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: | -------------------------------------+------------------------------------- Changes (by goldfire): * status: new => closed * resolution: => invalid -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13197#comment:4 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
participants (1)
-
GHC