
#10432: panic with kind polymorphism -------------------------------------+------------------------------------- Reporter: Ashley Yakeley | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 7.10.1 checker) | Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): -------------------------------------+------------------------------------- Comment (by jstolarek): I'm using a compiler built by `./validate` from commit e2b579e8d77357e8b36f57d15daead101586ac8e and here's what I get for originally reported code: {{{ [killy@xerxes : /dane/projekty/ghc/ghc-tests/types/T10432] cat T10432.hs {-# LANGUAGE ExistentialQuantification, PolyKinds, DataKinds, RankNTypes, GADTs, TypeOperators #-} module T10432 where import Data.Type.Equality data WrappedType = forall a. WrapType a; matchReflK :: forall (a :: ka) (b :: kb) (r :: *). ('WrapType a :~: 'WrapType b) -> (('WrapType a ~ 'WrapType b) => r) -> r; matchReflK Refl r = r; [killy@xerxes : /dane/projekty/ghc/ghc-tests/types/T10432] ghc-validate- stage1 -c -dcore-lint T10432.hs T10432.hs:8:15: error: Could not deduce: ka ~ kb from the context: 'WrapType a ~ 'WrapType b bound by the type signature for: matchReflK :: ('WrapType a ~ 'WrapType b) => r at T10432.hs:(8,15)-(9,74) ‘ka’ is a rigid type variable bound by the type signature for: matchReflK :: 'WrapType a :~: 'WrapType b -> (('WrapType a ~ 'WrapType b) => r) -> r at T10432.hs:8:15 ‘kb’ is a rigid type variable bound by the type signature for: matchReflK :: 'WrapType a :~: 'WrapType b -> (('WrapType a ~ 'WrapType b) => r) -> r at T10432.hs:8:15 Expected type: 'WrapType b Actual type: 'WrapType a In the ambiguity check for the type signature for ‘matchReflK’: matchReflK :: forall (ka :: BOX) (kb :: BOX) (a :: ka) (b :: kb) r. 'WrapType a :~: 'WrapType b -> (('WrapType a ~ 'WrapType b) => r) -> r To defer the ambiguity check to use sites, enable AllowAmbiguousTypes In the type signature for ‘matchReflK’: matchReflK :: forall (a :: ka) (b :: kb) (r :: *). (WrapType a :~: WrapType b) -> ((WrapType a ~ WrapType b) => r) -> r }}} And for the code in comment:1: {{{ [killy@xerxes : /dane/projekty/ghc/ghc-tests/types/T10432] cat T10432.hs {-# LANGUAGE ExistentialQuantification, PolyKinds, DataKinds, RankNTypes, GADTs, TypeOperators #-} module T10432 where import Data.Type.Equality data WrappedType = forall a. WrapType a; matchReflK2 :: forall (a :: ka) (b :: kb) (r :: *). ('WrapType a :~: 'WrapType b) -> r matchReflK2 x = let foo :: ('WrapType a ~ 'WrapType b) => r foo = undefined in undefined [killy@xerxes : /dane/projekty/ghc/ghc-tests/types/T10432] ghc-validate- stage1 -c -dcore-lint T10432.hs [killy@xerxes : /dane/projekty/ghc/ghc-tests/types/T10432] }}} I have no idea why are we getting different behaviours :-/ -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10432#comment:4 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler