[GHC] #11362: T6137 doesn't pass with reversed uniques

[GHC]

#11362: T6137 doesn't pass with reversed uniques
-------------------------------------+-------------------------------------
        Reporter:  niteria           |                Owner:  niteria
            Type:  bug               |               Status:  new
        Priority:  normal            |            Milestone:
       Component:  Compiler          |              Version:  8.1
      Resolution:                    |             Keywords:  TypeInType
Operating System:  Unknown/Multiple  |         Architecture:
 Type of failure:  GHC rejects       |  Unknown/Multiple
  valid program                      |            Test Case:
      Blocked By:                    |             Blocking:  4012
 Related Tickets:  #11371            |  Differential Rev(s):
       Wiki Page:                    |
-------------------------------------+-------------------------------------

Comment (by niteria):

 After clearing the `substTy` sanity check I'm back here with the original
 issue and I need some input on the underlying assumptions.
 The test fails with a lint failure:

 {{{
 *** Core Lint errors : in result of Tidy Core ***
 <no location info>: warning:
     [in body of lambda with binder dt_a18nZe :: In
                                                   g_a18o6Y
                                                   (Sum1 r_a18o6X (In ('F
 g_a18o6Y) r_a18o6X))
                                                   v_a18o6W]
     Kind application error in
       coercion ‘Sym
                   (D:R:InjuFrv0[0]
                      <u_a18nZB>_N <j_a18nZC>_N <g_a18o6Y>_N) <r_a18o6X>_N
 <v_a18o6W>_N’
       Function kind = Code (Sum j_a18nZC u_a18nZB) u_a18nZB -> *
       Arg kinds = [(v_a18o6W, u_a18nZB)]
 <no location info>: warning:
     [in body of lambda with binder dt_a18nZe :: In
                                                   g_a18o6Y
                                                   (Sum1 r_a18o6X (In ('F
 g_a18o6Y) r_a18o6X))
                                                   v_a18o6W]
     Kind application error in
       coercion ‘Sym
                   (D:R:InjuFrv0[0]
                      <u_a18nZB>_N <j_a18nZC>_N <g_a18o6Y>_N) <r_a18o6X>_N
 <v_a18o6W>_N’
       Function kind = Code (Sum j_a18nZC u_a18nZB) u_a18nZB -> *
       Arg kinds = [(v_a18o6W, u_a18nZB)]
 *** Offending Program ***
 $WMkIn [InlPrag=INLINE]
   :: forall u_a18nZB j_a18nZC (g_a18o6Y :: Code
                                              (Sum j_a18nZC u_a18nZB)
 u_a18nZB) (r_a18o6X :: j_a18nZC
 -> *) (v_a18o6W :: u_a18nZB).
      In g_a18o6Y (Sum1 r_a18o6X (In ('F g_a18o6Y) r_a18o6X)) v_a18o6W
      -> In ('F g_a18o6Y) r_a18o6X v_a18o6W
 [GblId[DataConWrapper],
  Arity=1,
  Caf=NoCafRefs,
  Str=DmdType <L,U>m,
  Unf=Unf{Src=InlineStable, TopLvl=True, Value=True, ConLike=True,
          WorkFree=True, Expandable=True,
          Guidance=ALWAYS_IF(arity=1,unsat_ok=False,boring_ok=True)
          Tmpl= \ (@ u_a18nZB)
                  (@ j_a18nZC)
                  (@ (g_a18o6Y :: Code (Sum j_a18nZC u_a18nZB) u_a18nZB))
                  (@ (r_a18o6X :: j_a18nZC -> *))
                  (@ (v_a18o6W :: u_a18nZB))
                  (dt_a18nZe [Occ=Once]
                     :: In
                          g_a18o6Y (Sum1 r_a18o6X (In ('F g_a18o6Y)
 r_a18o6X)) v_a18o6W) ->
                  (MkIn
                     @ u_a18nZB @ j_a18nZC @ g_a18o6Y @ r_a18o6X @ v_a18o6W
 dt_a18nZe)
                  `cast` (Sym
                            (D:R:InjuFrv0[0]
                               <u_a18nZB>_N <j_a18nZC>_N <g_a18o6Y>_N)
 <r_a18o6X>_N <v_a18o6W>_N

 }}}

 This didn't tell me much, so I kept digging. It seems that the case for
 `AxiomInstCo` in `lintCoercion`:

 {{{
 lintCoercion co@(AxiomInstCo con ind cos)
   = do { unless (0 <= ind && ind < numBranches (coAxiomBranches con))
                 (bad_ax (text "index out of range"))
        ; let CoAxBranch { cab_tvs   = ktvs
                         , cab_cvs   = cvs
                         , cab_roles = roles
                         , cab_lhs   = lhs
                         , cab_rhs   = rhs } = coAxiomNthBranch con ind
        ; unless (length ktvs + length cvs == length cos) $
            bad_ax (text "lengths")
        ; subst <- getTCvSubst
        ; let empty_subst = zapTCvSubst subst
        ; (subst_l, subst_r) <- foldlM check_ki
                                       (empty_subst, empty_subst)
                                       (zip3 (ktvs ++ cvs) roles cos)
        ; let lhs' = substTys subst_l lhs
              rhs' = substTy subst_r rhs
        ; case checkAxInstCo co of
            Just bad_branch -> bad_ax $ text "inconsistent with" <+>
                                        pprCoAxBranch con bad_branch
            Nothing -> return ()
        ; let s2 = mkTyConApp (coAxiomTyCon con) lhs'
        ; return (typeKind s2, typeKind rhs', s2, rhs', coAxiomRole con) }

 }}}

 assumes that `cab_lhs` and `cab_rhs` are in the same "order". When I
 printed out `cab_lhs` and `cab_rhs` I got `[j_a18o0a, u_a18o09, 'F
 g_a18o71]` and `R:InjuFrv u_a18o09 j_a18o0a g_a18o71` respectively (they
 do match up if I don't reverse the order of uniques).
 Later when we try to kind check `rhs'` and `s2 = mkTyConApp (coAxiomTyCon
 con) lhs'` we get a kind error.

 I don't know if the order is assumed to match up, there's no comment about
 that on the `CoAxBranch` constructor. If the assumption is that it should
 match up then the call to `mkSingleCoAxiom` in `tcDataFamInstDecl` breaks
 that.

 It reads:

 {{{
 mkSingleCoAxiom Representational axiom_name eta_tvs [] fam_tc
   eta_pats (mkTyConApp rep_tc (mkTyVarTys eta_tvs))
 }}}

 Where the last two parameters are `cab_lhs` and `cab_rhs` respectively.
 Notice that the "order" for `cab_rhs` is the same as the order of
 `eta_tvs`. This in turn is the order that `tcFamTyPats` returns them in.
 If we look at the code for `tcFamTyPats` the reordering happens when we
 call `qtkvs <- quantifyTyVars emptyVarSet $ splitDepVarsOfTypes typat`.
 `quantifyTyVars` takes a `VarSet` and then converts it into a list,
 effectively sorting by the value of the associated `Unique`.

 It's possible that I'm interpreting it wrong, any advice would be
 appreciated.

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