#15079: GHC HEAD regression: cannot instantiate higher-rank kind -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: high | Milestone: 8.6.1 Component: Compiler (Type | Version: 8.5 checker) | Resolution: | Keywords: TypeInType 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 RyanGlScott): * cc: goldfire (added) Comment: This regression was introduced in commit e3dbb44f53b2f9403d20d84e27f187062755a089 (Fix #12919 by making the flattener homegeneous.). -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15079#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#15079: GHC HEAD regression: cannot instantiate higher-rank kind -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: high | Milestone: 8.6.1 Component: Compiler (Type | Version: 8.5 checker) | Resolution: | Keywords: TypeInType 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 simonpj): The error message is perplexing, because it suggests that we have failed to prove {{{ forall i. i -> * ~# forall k. k -> * }}} Why? It seems that their visibility-flag differs, as you see if you use `-fprint-explicit-foralls` (which Joe User will never think of): {{{ T15079.hs:19:34: error: * Kind mismatch: cannot unify (c0 :: forall i. i -> *) with: Coerce :: forall {k}. k -> * Their kinds differ. Expected type: a -> c0 * a Actual type: Starify a -> Coerce a }}} `tcEqType` took no account of the visibility flag before. Is this anything to do with making the flattener homogeneous?? I see that `TcType.tcEqType` has grown two new bells * It returns a `Maybe Bool` with this rubric {{{ -- Nothing : the types are equal -- Just True : the types differ, and the point of difference is visible -- Just False : the types differ, and the point of difference is invisible }}} But why? We didn't do that before. * The treatment of `ForAllTy` has changed: {{{ go vis env (ForAllTy (TvBndr tv1 vis1) ty1) (ForAllTy (TvBndr tv2 vis2) ty2) = go (isVisibleArgFlag vis1) env (tyVarKind tv1) (tyVarKind tv2) go vis (rnBndr2 env tv1 tv2) ty1 ty2 check vis (vis1 == vis2) }}} Notice that `check vis (vis1 == vis2)`. That means we say not-equal if the visibility flags differ. But why? These flags are constants, so if they differ now they'll always differ and cannot be unified. I have no idea what is going on here. Richard can you shed some light? I'll grant that it's a bit suspicious to say that two forall type are the same if their visibility flags differ. But in this case, yes, `Coerce`'s kind has an Inferred forall, whereas `c`'s kind is Specified. Does that mean they are incompatible? I can't foresee all the consequences of such a decision. At very least, here's a pretty-printer suggestion: if we do print a `forall` at all (as we do in this error message) maybe we should always display its visibility status? Otherwise error messages like this are desperately confusing. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15079#comment:3 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#15079: GHC HEAD regression: cannot instantiate higher-rank kind -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: high | Milestone: 8.6.1 Component: Compiler (Type | Version: 8.5 checker) | Resolution: | Keywords: TypeInType 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 RyanGlScott): Now that I have a better understanding of why this is failing, here's a simpler program which demonstrates the issue (this typechecks on GHC 8.4.2, but not HEAD): {{{#!hs {-# LANGUAGE RankNTypes #-} {-# LANGUAGE TypeInType #-} module Bug where import Data.Kind newtype Foo (f :: forall (a :: Type). a -> Type) = MkFoo (f Int) data InferredProxy a = MkInferredProxy foo :: Foo InferredProxy foo = MkFoo MkInferredProxy }}} {{{ $ ~/Software/ghc/inplace/bin/ghc-stage2 Bug.hs [1 of 1] Compiling Bug ( Bug.hs, Bug.o ) Bug.hs:11:13: error: • Kind mismatch: cannot unify (f0 :: forall a. a -> *) with: InferredProxy :: forall k. k -> * Their kinds differ. Expected type: f0 * Int Actual type: InferredProxy Int • In the first argument of ‘MkFoo’, namely ‘MkInferredProxy’ In the expression: MkFoo MkInferredProxy In an equation for ‘foo’: foo = MkFoo MkInferredProxy | 11 | foo = MkFoo MkInferredProxy | ^^^^^^^^^^^^^^^ }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15079#comment:5 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#15079: GHC HEAD regression: cannot instantiate higher-rank kind -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: high | Milestone: 8.6.1 Component: Compiler (Type | Version: 8.5 checker) | Resolution: | Keywords: TypeInType 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 RyanGlScott): Richard and I discussed this yesterday. We noted that: 1. The interaction between higher-rank kinds and binder visibility has many parallels with other unexpected properties of higher-rank kinds. In particular, because there are (currently) no type-level lambdas, higher- rank kinds' `foralls` are more rigid than their type-level counterparts. As one example, in #13399 it was noted that higher-rank kinds' `foralls` don't "float" like the ones in higher-rank types. In this sense, it's perhaps somewhat understandable that higher-rank kinds' visibility might also be more rigid. 2. If we wanted to have a more permissive treatment of invisible binders in higher-rank kinds, then we'd need to come up with a better story. Richard considered various ideas like having a subtyping relation between visibilities, but in the end, he concluded that anything we could think of was likely far too complicated for such little payoff. Thus, the conclusion we reached was that we should keep the current behavior, and make note of this behavior in the users' guide. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15079#comment:7 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#15079: GHC HEAD regression: cannot instantiate higher-rank kind -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: patch Priority: high | Milestone: 8.6.1 Component: Compiler (Type | Version: 8.5 checker) | Resolution: | Keywords: TypeInType Operating System: Unknown/Multiple | Architecture: Type of failure: GHC rejects | Unknown/Multiple valid program | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Phab:D4803 Wiki Page: | -------------------------------------+------------------------------------- Comment (by Ben Gamari ): In [changeset:"bc9a838a27f40a6008e127d9105981713abe774b/ghc" bc9a838/ghc]: {{{ #!CommitTicketReference repository="ghc" revision="bc9a838a27f40a6008e127d9105981713abe774b" Document #15079 in the users' guide Trac #15079 revealed an interesting limitation in the interaction between variable visibility and higher-rank kinds. We (Richard and I) came to the conclusion that this is an acceptable (albeit surprising) limitation, so this documents in the users' guide to hopefully eliminate some confusion for others in the future. Test Plan: Read it Reviewers: goldfire, bgamari Reviewed By: bgamari Subscribers: rwbarton, thomie, carter GHC Trac Issues: #15079 Differential Revision: https://phabricator.haskell.org/D4803 }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15079#comment:9 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler