[GHC] #15009: Float equalities past local equalities
GHC
ghc-devs at haskell.org
Thu Oct 4 06:57:24 UTC 2018
#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
More information about the ghc-tickets
mailing list