[GHC] #10432: panic with kind polymorphism
#10432: panic with kind polymorphism -------------------------------------+------------------------------------- Reporter: Ashley | Owner: Yakeley | Status: new Type: bug | Milestone: Priority: normal | Version: 7.10.1 Component: Compiler | Operating System: Unknown/Multiple (Type checker) | Type of failure: None/Unknown Keywords: | Blocked By: Architecture: | Related Tickets: Unknown/Multiple | Test Case: | Blocking: | Differential Revisions: | -------------------------------------+------------------------------------- {{{#!hs {-# LANGUAGE ExistentialQuantification, PolyKinds, DataKinds, RankNTypes, GADTs, TypeOperators #-} module Bug 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; }}} give this: {{{ Bug.hs:8:15: Couldn't match kind ‘ka’ with ‘kb’ ‘ka’ is untouchable inside the constraints ('WrapType a ~ 'WrapType b) bound by the type signature for matchReflK :: ('WrapType a ~ 'WrapType b) => r at Bug.hs:(8,15)-(9,74)ghc: panic! (the 'impossible' happened) (GHC version 7.10.1 for x86_64-unknown-linux): No skolem info: ka_aqv[sk] Please report this as a GHC bug: http://www.haskell.org/ghc/reportabug }}} I actually think GHC should accept this (and furthermore infer `ka ~ kb`). -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10432 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#10432: panic with kind polymorphism -------------------------------------+------------------------------------- Reporter: Ashley Yakeley | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 7.10.1 checker) | Keywords: Resolution: | Architecture: Operating System: Unknown/Multiple | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Revisions: -------------------------------------+------------------------------------- Comment (by simonpj): This works in HEAD, but another variant makes HEAD, too, fail in the same way `No skolem info`: {{{ 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 }}} Reason: the type of `foo` mentions `a`, `b`, `r` as free variables; the ambiguity check doesn't bind them; the error message generator falls over. Need to look into this. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10432#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#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 just tested Simon's code and it works in HEAD. Originally reported code results in type ambiguity error (well, kind ambiguity in fact). 403cfc9187b9df560768bb809f4d280fb999639c added some comments about this ticket but I don't think that any commit explicitly addressed issues reported here. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10432#comment:2 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#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 simonpj): It does not work in HEAD for me. I get {{{ simonpj@cam-05-unx:~/tmp$ ~/5builds/HEAD-4/inplace/bin/ghc-stage1 -c -dcore-lint T10432.hs RAE1 [W] cobox_arV :: ka1_arO[sk] ~ kb1_arP[sk] (CNonCanonical) ka1_arO[sk] kb1_arP[sk] False T10432.hs:17:15: error: Couldn't match kind ‘ka1’ with ‘kb1’ ‘ka1’ is untouchable inside the constraints: 'WrapType a1 ~ 'WrapType b1 bound by the type signature for: foo :: ('WrapType a1 ~ 'WrapType b1) => r1 at T10432.hs:17:15-46ghc-stage1: panic! (the 'impossible' happened) (GHC version 7.11.20151006 for x86_64-unknown-linux): No skolem info: kb1_arP[sk] }}} for the code in comment:1 -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10432#comment:3 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#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
#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 thomie): I can reproduce jstolarek's findings. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10432#comment:5 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#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): Phab:D1691 Wiki Page: | -------------------------------------+------------------------------------- Changes (by jstolarek): * differential: => Phab:D1691 Comment: I tested again and now it seems that the code in original bug report as well as Simon's code in comment 1 are accepted. I added a regression test. Once it validates on Phab I think we can close this ticket. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10432#comment:6 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#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): Phab:D1691 Wiki Page: | -------------------------------------+------------------------------------- Comment (by simonpj): Terrific, thanks. Yes, pls add regression and close. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10432#comment:7 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#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): Phab:D1691
Wiki Page: |
-------------------------------------+-------------------------------------
Comment (by Jan Stolarek
#10432: panic with kind polymorphism -------------------------------------+------------------------------------- Reporter: Ashley Yakeley | Owner: Type: bug | Status: closed Priority: normal | Milestone: Component: Compiler (Type | Version: 7.10.1 checker) | Resolution: fixed | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: | typecheck/should_compile/T10432 Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Phab:D1691 Wiki Page: | -------------------------------------+------------------------------------- Changes (by jstolarek): * testcase: => typecheck/should_compile/T10432 * status: new => closed * resolution: => fixed -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10432#comment:9 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
participants (1)
-
GHC