#11362 closed bug (fixed)

T6137 doesn't pass with reversed uniques

Reported by: niteria Owned by: niteria
Priority: normal Milestone: 8.0.1
Component: Compiler Version: 8.1
Keywords: TypeInType Cc: simonmar, simonpj, goldfire
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: GHC rejects valid program Test Case:
Blocked By: Blocking: #4012
Related Tickets: #11371 Differential Rev(s):
Wiki Page:

Description

It fails with (full trace https://phabricator.haskell.org/P81):

*** Core Lint errors : in result of Tidy Core ***
<no location info>: warning:
    [in body of lambda with binder dt_a18nYf :: In
                                                  f_a18o2M
                                                  (Sum1 r_a18o2L (In ('F f_a18o2M) r_a18o2L))
                                                  o_a18o2K]
    Kind application error in
      coercion ‘Sym
                  (TFCo:R:InioFro[0]
                     <o_a18nYC>_N <i_a18nYD>_N <f_a18o2M>_N) <r_a18o2L>_N <o_a18o2K>_N’
      Function kind = Code (Sum i_a18nYD o_a18nYC) o_a18nYC -> *
      Arg kinds = [(o_a18o2K, o_a18nYC)]
<no location info>: warning:
    [in body of lambda with binder dt_a18nYf :: In
                                                  f_a18o2M
                                                  (Sum1 r_a18o2L (In ('F f_a18o2M) r_a18o2L))
                                                  o_a18o2K]
    Kind application error in
      coercion ‘Sym
                  (TFCo:R:InioFro[0]
                     <o_a18nYC>_N <i_a18nYD>_N <f_a18o2M>_N) <r_a18o2L>_N <o_a18o2K>_N’
      Function kind = Code (Sum i_a18nYD o_a18nYC) o_a18nYC -> *
      Arg kinds = [(o_a18o2K, o_a18nYC)]

Steps to reproduce:

  1. Add line

TEST_HC_OPTS += -dinitial-unique=16777000 -dunique-increment=-1

after line

TEST_HC_OPTS = -fforce-recomp -dcore-lint -dcmm-lint -dno-debug-output -no-user-$(GhcPackageDbFlag) -rtsopts $(EXTRA_HC_OPTS)

in mk/test.mk

  1. make TESTS=T6137

Change History (10)

comment:2 Changed 19 months ago by goldfire

Keywords: TypeInType added

comment:3 Changed 18 months ago by niteria

Blocking: 4012 added
Owner: changed from goldfire to niteria

This is a symptom of #11371. I just got this:

ghc-stage2: panic! (the 'impossible' happened)
  (GHC version 8.1.20160121 for x86_64-unknown-linux):
        ASSERT failed!
  CallStack (from ImplicitParams):
  assertPprPanic, called at compiler/types/TyCoRep.hs:1868:61 in ghc:TyCoRep
  substTy, called at compiler/types/TyCoRep.hs:1799:23 in ghc:TyCoRep
  substTyWith, called at compiler/types/Type.hs:799:46 in ghc:Type
  in_scope InScope [aph :-> k1_aph]
  tenv [aph :-> k1_aph]
  cenv []
  ty (k1_aph -> *) -> (k2_apj -> *) -> Sum k1_aph k2_apj -> *
  needInScope [apj :-> k2_apj]

comment:4 Changed 17 months ago 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.

comment:5 Changed 17 months ago by goldfire

I have not been following this ticket, but I'm very lost at the last comment.

  • cab_lhs is a list of types that are the type patterns on the LHS of an axiom.
  • cab_rhs is the type on the RHS of an axiom.

What do you mean by an order of the RHS? There's just one thing.

The line of code you include is for data family axioms, where the RHS has a certain prescribed form. I can see how "order" might apply here. But the Core Lint code should work over all axioms, including type family axioms, for which the RHS has no notion of ordering at all. What makes you say that Core Lint is assuming this?

It is possible something somewhere is assuming an ordering property about data family axioms, in particular, but it's not Core Lint.

comment:6 Changed 17 months ago by Simon Peyton Jones <simonpj@…>

In e2f7d777/ghc:

A tiny, outright bug in tcDataFamInstDecl

This bug was revealed by Trac #11362.  It turns out that in my patch
for Trac #11148 (namely 1160dc5), I failed to turn one occurrence of
tvs' into full_tvs.  Sigh.  This is tricky stuff and it cost me
several hours to page it back in and figure out what was happening.

The result was a CoAxiom whose lhs had rhs had different kinds.  Eeek!

Anyway it's fixed.

I also added an ASSERT, in FamInst.newFamInst, that trips on such
bogus CoAxioms.

comment:7 Changed 17 months ago by simonpj

Status: newmerge

OK fixed. Merge to stable branch please.

Would someone (Bartosz) like to add a regression test? Perhaps just compiling this test with reversed uniques. Thanks!

I'll put it in merge state, but let's not forget that test.

comment:8 Changed 17 months ago by niteria

I will add a test. Thank you! This should unblock D1905 from #4012.

comment:9 Changed 17 months ago by Bartosz Nitka <niteria@…>

In 023742e4/ghc:

Add a testcase for #11362

This reproduces the issue that I encountered in #11362.

Test Plan: this testcase

Reviewers: simonpj, bgamari, austin

Reviewed By: simonpj

Subscribers: thomie, simonmar

Differential Revision: https://phabricator.haskell.org/D1917

GHC Trac Issues: #11362

comment:10 Changed 17 months ago by bgamari

Milestone: 8.0.1
Resolution: fixed
Status: mergeclosed

Merged fix.

Also merged test as 77de825300a71be0769f23d70015716672e91ca4.

Note: See TracTickets for help on using tickets.