[GHC] #15079: GHC HEAD regression: cannot instantiate higher-rank kind

[GHC]

#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