#11362: T6137 doesn't pass with reversed uniques -------------------------------------+------------------------------------- Reporter: niteria | Owner: goldfire 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: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by goldfire): * keywords: => TypeInType -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11362#comment:2 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#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] _N _N _N) _N _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] _N _N _N) _N _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 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] _N _N _N) _N _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

#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 Simon Peyton Jones ): In [changeset:"e2f7d777bb7e4c176e01e1c4f8184f115253dee0/ghc" e2f7d777/ghc]: {{{ #!CommitTicketReference repository="ghc" revision="e2f7d777bb7e4c176e01e1c4f8184f115253dee0" 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. }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11362#comment:6 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#11362: T6137 doesn't pass with reversed uniques -------------------------------------+------------------------------------- Reporter: niteria | Owner: niteria Type: bug | Status: merge 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): I will add a test. Thank you! This should unblock D1905 from #4012. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11362#comment:8 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#11362: T6137 doesn't pass with reversed uniques -------------------------------------+------------------------------------- Reporter: niteria | Owner: niteria Type: bug | Status: closed Priority: normal | Milestone: 8.0.1 Component: Compiler | Version: 8.1 Resolution: fixed | 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: | -------------------------------------+------------------------------------- Changes (by bgamari): * status: merge => closed * resolution: => fixed * milestone: => 8.0.1 Comment: Merged fix. Also merged test as 77de825300a71be0769f23d70015716672e91ca4. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11362#comment:10 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler