#15009: Float equalities past local equalities -------------------------------------+------------------------------------- Reporter: goldfire | Owner: (none) Type: feature request | Status: closed Priority: normal | Milestone: 8.4.3 Component: Compiler | Version: 8.2.2 Resolution: fixed | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: gadt/T15009 Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by nfrisby): Replying to [comment:11 simonpj]: I've spent the evening reading all the examples I could find (see previous comment) and drafting this comment. I think the example you gave in #[comment:11] does address my precise question in #[comment:10] about {{{getNoGivenEqs}}} in a way that no other existing example does. So it would probably be useful in the Note. However, I can also now ask a more exact question! I pose two questions below. With GHC 8.6.0.20180810, the following does not typecheck, because {{{z}}} is untouchable under the pattern matches. {{{ data TFun z = MkTFun (forall y. T y -> z) data T a where T1 :: T Bool T2 :: T Char example () = MkTFun (\x -> case x of { T1 -> True; T2 -> False }) }}} The constraint solver gets stuck in this state in the {{{-ddump-tc- trace}}} (I grabbed this from the middle because the taus become sks after a certain point and I didn't intend for that to be relevant). {{{ solveNestedImplications starting { solveImplication { Implic { TcLevel = 2 Skolems = y_aWl[sk:2] No-eqs = True Status = Unsolved Given = Wanted = WC {wc_impl = Implic { TcLevel = 3 Skolems = No-eqs = False Status = Unsolved Given = co_aWq :: y_aWl[sk:2] GHC.Prim.~# Bool Wanted = WC {wc_simple = [WD] hole{co_aWB} {1}:: z_aWj[tau:1] GHC.Prim.~# Bool (CNonCanonical)} Binds = EvBindsVar<aWs> a pattern with constructor: T1 :: T Bool, in a case alternative } Implic { TcLevel = 3 Skolems = No-eqs = False Status = Unsolved Given = co_aWt :: y_aWl[sk:2] GHC.Prim.~# Char Wanted = WC {wc_simple = [WD] hole{co_aWC} {1}:: z_aWj[tau:1] GHC.Prim.~# Bool (CNonCanonical)} Binds = EvBindsVar<aWv> a pattern with constructor: T2 :: T Char, in a case alternative }} Binds = EvBindsVar<aWw> a type expected by the context: forall y. T y -> z_aWj[tau:1] } Inerts {Unsolved goals = 0} Inert fsks = [] }}} {{{co_aWB}}} and {{{co_aWC}}} do not float; their parent implication has a given equality (where {{{skolem_bound_here}}} is {{{False}}}), so the {{{floatEqualities}}} function gives up immediately. Thus, my first question is: Why wouldn't we want GHC to float {{{z[tau:1] ~ Bool}}} past {{{y[sk:2] ~ Bool}}} here? The rest of this comment explains why I don't think the existing examples answer that question. This simple rule that causes {{{floatEqualities}}} to currently give up here is motivated by examples found in {{{Note [Float Equalities out of Implications]}}} and also in Section 5.1 and Example 5.1 of jfp- outsidein.pdf (print pages 35 and 37). However, in all of those examples the given and the wanted equalities involve metavars with the same level. In this comment's example, the levels and {{{TcTyVarDetails}}} flavors are different and that seems relevant to me. In particular, because of the levels, {{{z := y}}} is not a valid assignment -- but such an assignment (which is valid when {{{level(y) <= level(z)}}}) motivates the conservative rule in both {{{Note [Float Equalities out of Implications]}}} and also Section 5.1 of the paper. Relatedly, Example 5.1 from the paper points out that an assignment akin to {{{z := F y}}} might become a solution; that assignment is also invalid if {{{level(y) > level(z)}}}. Your example from #[comment:11] ... {{{ data S a where MkS :: S Int g :: forall a. S a -> a -> () g x y = let h = \z -> ( z :: Int , case x of MkS -> [y,z]) in h (3 :: Int) `seq` () }}} ... gets stuck here in the {{{-ddump-tc-trace}}} ... {{{ setImplicationStatus(not-all-solved) } Implic { TcLevel = 1 Skolems = a_a1ln[sk:1] No-eqs = True Status = Unsolved Given = Wanted = WC {wc_impl = Implic { TcLevel = 2 Skolems = No-eqs = False Status = Unsolved Given = co_a1lH :: a_a1ln[sk:1] GHC.Prim.~# Int Wanted = WC {wc_simple = [WD] hole{co_a1lY} {2}:: b_a1ly[tau:1] GHC.Prim.~# [Int] (CNonCanonical)} Binds = EvBindsVar<a1lL> a pattern with constructor: MkS :: S Int, in a case alternative }} Binds = EvBindsVar<a1lV> the type signature for: g :: forall a. S a -> a -> () } Constraint solver steps = 3 unflattenGivens [] End simplifyTop } reportUnsolved { }}} ... as it should! The given and the wanted both have type variables of the same level, so {{{b := a}}} is a valid assignment. The example from #[comment:5] that directly motivated this exact ticket is a little more involved. In that case, the given equality is between variables of level 2 and 3, while the wanted equality is for a variable of level 2. To some degree, the {{{level(y) > level(z)}}} condition does hold here. It's certainly more subtle than my example, but maybe the let-bound skolem rule could be subsumed by my hypothetical "float equalities past equalities if the involved levels are OK" rule. My second question is: Does such a "float equalities past equalities if the involved levels are OK" rule seem feasible/practical? Has that been investigated at all? I'm particularly worried I'm overlooking some pitfall due to the open world assumption, though skolems seem relatively localized. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15009#comment:16 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler