[GHC] #13879: Strange interaction between higher-rank kinds and type synonyms

[GHC]

#13879: Strange interaction between higher-rank kinds and type synonyms
-------------------------------------+-------------------------------------
        Reporter:  RyanGlScott       |                Owner:  (none)
            Type:  bug               |               Status:  new
        Priority:  normal            |            Milestone:
       Component:  Compiler (Type    |              Version:  8.0.1
  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):

 I could not resist investigating. Here are my conclusions.

 * With a DEBUG compiler, I immediately tripped over
 {{{
         ASSERT failed!
   in_scope InScope {z_aUa y_aUb}
   tenv [aSo :-> z0_aUa[tau:1], aSp :-> y0_aUb[tau:1]]
   cenv []
   tys [(:~~:) j0_aU1[tau:1] k0_aU2[tau:1] a_aSl[sk:1] y_aSp[sk:1]
        -> *]
   cos []
   needInScope [aSj :-> j_aSj[sk:1], aSl :-> a_aSl[sk:1],
                aU1 :-> j_aU1[tau:1], aU2 :-> k_aU2[tau:1]]
   Call stack:
       CallStack (from HasCallStack):
         prettyCurrentCallStack, called at
 compiler\utils\Outputable.hs:1133:58 in ghc:Outputable
         callStackDoc, called at compiler\utils\Outputable.hs:1188:22 in
 ghc:Outputable
         assertPprPanic, called at compiler\types\TyCoRep.hs:2099:51 in
 ghc:TyCoRep
         checkValidSubst, called at compiler\types\TyCoRep.hs:2122:29 in
 ghc:TyCoRep
         substTy, called at compiler\typecheck\TcHsType.hs:936:27 in
 ghc:TcHsType
 }}}
   This was just a missing in-scope set setup in `TcHsType.instantiateTyN`.
 Easy to fix.

 * Next up, the original program. The bug here was that in a type signature
 like
 {{{
      f :: forall (p :: forall z (y::z). <blah>). <more blah>
 }}}
   when instanting p's kind at occurrences of p in <more blah> it's crucial
 that the kind we instantiate is fully zonked,  else we may fail to
 substitute properly.  But `tcLHsKind` (which converts the `LHsKind` to a
 `Kind` didn't zonk its result.  Also easily fixed, and that makes the
 original program work.

 * Next, the mysterious message when you use `HRApp`.  This arises because
 we try to unify the kinds
 {{{
     forall z1 (y1::z1). HR a1 b1 c1 d1  ~#  forall z2 (y2::z2). HR a2 b2
 c2 d2
 }}}
   (I'm using `HR` instead of infix `:~~:`, just to keep my head straight.)
 The first thing is that, at least by the time the constraint solver gets
 it, if we zonked LHS and RHS we'd see they were equal. But that's a small
 thing.  What we do in `TcCanonical` is this:
 {{{
 can_eq_nc' _flat _rdr_env _envs ev eq_rel
              s1@(ForAllTy {}) _ s2@(ForAllTy {}) _
  | CtWanted { ctev_loc = loc, ctev_dest = orig_dest } <- ev
  = do { let (bndrs1,body1) = tcSplitForAllTyVarBndrs s1
             (bndrs2,body2) = tcSplitForAllTyVarBndrs s2
       ; kind_cos <- zipWithM (unifyWanted loc Nominal)
                              (map binderKind bndrs1) (map binderKind
 bndrs2)
       ; all_co <- deferTcSForAllEq (eqRelRole eq_rel) loc
                                     kind_cos (bndrs1,body1) (bndrs2,body2)
       ; setWantedEq orig_dest all_co
       ; stopWith ev "Deferred polytype equality" }
 }}}
   Look at that `zipWithM`.  It's obvously bogus in the case above, because
 we produce a constraint `z1~z2` which is insoluble.

   I need Richard's help here; but I think we just need to spit out that
 kind equality ''inside'' the new implication constraint, and after the
 alpha-renaming, rather than outside and before.

--
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/13879#comment:1>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler