#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