#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