Commit 4b3df0bb authored by Simon Peyton Jones's avatar Simon Peyton Jones

Further improvements to floating equalities

This equality-floating stuff is horribly delicate!  Trac #9316 showed
up yet another corner case.

The main changes are
 * include CTyVarEqs when "growing" the skolem set
 * do not include the kind argument to (~) when growing the skolem set

I added a lot more comments as well
parent 3214ec5a
......@@ -843,39 +843,6 @@ Consider floated_eqs (all wanted or derived):
simpl_loop. So we iterate if there any of these
\begin{code}
floatEqualities :: [TcTyVar] -> Bool -> WantedConstraints
-> TcS (Cts, WantedConstraints)
-- Post: The returned floated constraints (Cts) are only Wanted or Derived
-- and come from the input wanted ev vars or deriveds
-- Also performs some unifications, adding to monadically-carried ty_binds
-- These will be used when processing floated_eqs later
floatEqualities skols no_given_eqs wanteds@(WC { wc_flat = flats })
| not no_given_eqs -- There are some given equalities, so don't float
= return (emptyBag, wanteds) -- Note [Float Equalities out of Implications]
| otherwise
= do { let (float_eqs, remaining_flats) = partitionBag is_floatable flats
; untch <- TcS.getUntouchables
; mapM_ (promoteTyVar untch) (varSetElems (tyVarsOfCts float_eqs))
-- See Note [Promoting unification variables]
; ty_binds <- getTcSTyBindsMap
; traceTcS "floatEqualities" (vcat [ text "Flats =" <+> ppr flats
, text "Floated eqs =" <+> ppr float_eqs
, text "Ty binds =" <+> ppr ty_binds])
; return (float_eqs, wanteds { wc_flat = remaining_flats }) }
where
-- See Note [Float equalities from under a skolem binding]
skol_set = fixVarSet mk_next (mkVarSet skols)
mk_next tvs = foldrBag grow_one tvs flats
grow_one (CFunEqCan { cc_tyargs = xis, cc_rhs = rhs }) tvs
| intersectsVarSet tvs (tyVarsOfTypes xis)
= tvs `unionVarSet` tyVarsOfType rhs
grow_one _ tvs = tvs
is_floatable :: Ct -> Bool
is_floatable ct = isEqPred pred && skol_set `disjointVarSet` tyVarsOfType pred
where
pred = ctPred ct
promoteTyVar :: Untouchables -> TcTyVar -> TcS ()
-- When we float a constraint out of an implication we must restore
-- invariant (MetaTvInv) in Note [Untouchable type variables] in TcType
......@@ -1036,6 +1003,80 @@ should! If we don't solve the constraint, we'll stupidly quantify over
(b:*) instead of (a:OpenKind), which can lead to disaster; see Trac #7332.
Trac #7641 is a simpler example.
Note [Promoting unification variables]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
When we float an equality out of an implication we must "promote" free
unification variables of the equality, in order to maintain Invariant
(MetaTvInv) from Note [Untouchable type variables] in TcType. for the
leftover implication.
This is absolutely necessary. Consider the following example. We start
with two implications and a class with a functional dependency.
class C x y | x -> y
instance C [a] [a]
(I1) [untch=beta]forall b. 0 => F Int ~ [beta]
(I2) [untch=beta]forall c. 0 => F Int ~ [[alpha]] /\ C beta [c]
We float (F Int ~ [beta]) out of I1, and we float (F Int ~ [[alpha]]) out of I2.
They may react to yield that (beta := [alpha]) which can then be pushed inwards
the leftover of I2 to get (C [alpha] [a]) which, using the FunDep, will mean that
(alpha := a). In the end we will have the skolem 'b' escaping in the untouchable
beta! Concrete example is in indexed_types/should_fail/ExtraTcsUntch.hs:
class C x y | x -> y where
op :: x -> y -> ()
instance C [a] [a]
type family F a :: *
h :: F Int -> ()
h = undefined
data TEx where
TEx :: a -> TEx
f (x::beta) =
let g1 :: forall b. b -> ()
g1 _ = h [x]
g2 z = case z of TEx y -> (h [[undefined]], op x [y])
in (g1 '3', g2 undefined)
Note [Solving Family Equations]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
After we are done with simplification we may be left with constraints of the form:
[Wanted] F xis ~ beta
If 'beta' is a touchable unification variable not already bound in the TyBinds
then we'd like to create a binding for it, effectively "defaulting" it to be 'F xis'.
When is it ok to do so?
1) 'beta' must not already be defaulted to something. Example:
[Wanted] F Int ~ beta <~ Will default [beta := F Int]
[Wanted] F Char ~ beta <~ Already defaulted, can't default again. We
have to report this as unsolved.
2) However, we must still do an occurs check when defaulting (F xis ~ beta), to
set [beta := F xis] only if beta is not among the free variables of xis.
3) Notice that 'beta' can't be bound in ty binds already because we rewrite RHS
of type family equations. See Inert Set invariants in TcInteract.
This solving is now happening during zonking, see Note [Unflattening while zonking]
in TcMType.
*********************************************************************************
* *
* Floating equalities *
* *
*********************************************************************************
Note [Float Equalities out of Implications]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
For ordinary pattern matches (including existentials) we float
......@@ -1081,8 +1122,59 @@ Consequence: classes with functional dependencies don't matter (since there is
no evidence for a fundep equality), but equality superclasses do matter (since
they carry evidence).
\begin{code}
floatEqualities :: [TcTyVar] -> Bool -> WantedConstraints
-> TcS (Cts, WantedConstraints)
-- Main idea: see Note [Float Equalities out of Implications]
--
-- Post: The returned floated constraints (Cts) are only Wanted or Derived
-- and come from the input wanted ev vars or deriveds
-- Also performs some unifications (via promoteTyVar), adding to
-- monadically-carried ty_binds. These will be used when processing
-- floated_eqs later
--
-- Subtleties: Note [Float equalities from under a skolem binding]
-- Note [Skolem escape]
floatEqualities skols no_given_eqs wanteds@(WC { wc_flat = flats })
| not no_given_eqs -- There are some given equalities, so don't float
= return (emptyBag, wanteds) -- Note [Float Equalities out of Implications]
| otherwise
= do { let (float_eqs, remaining_flats) = partitionBag is_floatable flats
; untch <- TcS.getUntouchables
; mapM_ (promoteTyVar untch) (varSetElems (tyVarsOfCts float_eqs))
-- See Note [Promoting unification variables]
; ty_binds <- getTcSTyBindsMap
; traceTcS "floatEqualities" (vcat [ text "Skols =" <+> ppr skols
, text "Flats =" <+> ppr flats
, text "Skol set =" <+> ppr skol_set
, text "Floated eqs =" <+> ppr float_eqs
, text "Ty binds =" <+> ppr ty_binds])
; return (float_eqs, wanteds { wc_flat = remaining_flats }) }
where
is_floatable :: Ct -> Bool
is_floatable ct
= case classifyPredType (ctPred ct) of
EqPred ty1 ty2 -> skol_set `disjointVarSet` tyVarsOfType ty1
&& skol_set `disjointVarSet` tyVarsOfType ty2
_ -> False
skol_set = fixVarSet mk_next (mkVarSet skols)
mk_next tvs = foldr grow_one tvs flat_eqs
flat_eqs :: [(TcTyVarSet, TcTyVarSet)]
flat_eqs = [ (tyVarsOfType ty1, tyVarsOfType ty2)
| EqPred ty1 ty2 <- map (classifyPredType . ctPred) (bagToList flats)]
grow_one (tvs1,tvs2) tvs
| intersectsVarSet tvs tvs1 = tvs `unionVarSet` tvs2
| intersectsVarSet tvs tvs2 = tvs `unionVarSet` tvs2
| otherwise = tvs
\end{code}
Note [When does an implication have given equalities?]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
NB: This note is mainly referred to from TcSMonad
but it relates to floating equalities, so I've
left it here
Consider an implication
beta => alpha ~ Int
where beta is a unification variable that has already been unified
......@@ -1126,116 +1218,95 @@ This seems like the Right Thing, but it's more code, and more work
at runtime, so we are using the FlatSkolOrigin idea intead. It's less
obvious that it works, but I think it does, and it's simple and efficient.
Note [Float equalities from under a skolem binding]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
You might worry about skolem escape with all this floating.
For example, consider
[2] forall a. (a ~ F beta[2] delta,
Maybe beta[2] ~ gamma[1])
The (Maybe beta ~ gamma) doesn't mention 'a', so we float it, and
solve with gamma := beta. But what if later delta:=Int, and
F b Int = b.
Then we'd get a ~ beta[2], and solve to get beta:=a, and now the
skolem has escaped!
But it's ok: when we float (Maybe beta[2] ~ gamma[1]), we promote beta[2]
to beta[1], and that means the (a ~ beta[1]) will be stuck, as it should be.
Previously we tried to "grow" the skol_set with the constraints, to get
all the tyvars that could *conceivably* unify with the skolems, but that
was far too conservative (Trac #7804). Example: this should be fine:
f :: (forall a. a -> Proxy x -> Proxy (F x)) -> Int
f = error "Urk" :: (forall a. a -> Proxy x -> Proxy (F x)) -> Int
BUT (sigh) we have to be careful. Here are some edge cases:
Which of the flat equalities can we float out? Obviously, only
ones that don't mention the skolem-bound variables. But that is
over-eager. Consider
[2] forall a. F a beta[1] ~ gamma[2], G beta[1] gamma[2] ~ Int
The second constraint doesn't mention 'a'. But if we float it
we'll promote gamma to gamma'[1]. Now suppose that we learn that
beta := Bool, and F a Bool = a, and G Bool _ = Int. Then we'll
we left with the constraint
[2] forall a. a ~ gamma'[1]
which is insoluble because gamma became untouchable.
Solution: only promote a constraint if its free variables cannot
possibly be connected with the skolems. Procedurally, start with
the skolems and "grow" that set as follows:
* For each flat equality F ts ~ s, or tv ~ s,
if the current set intersects with the LHS of the equality,
add the free vars of the RHS, and vice versa
That gives us a grown skolem set. Now float an equality if its free
vars don't intersect the grown skolem set.
This seems very ad hoc (sigh). But here are some tricky edge cases:
a) [2]forall a. (F a delta[1] ~ beta[2], delta[1] ~ Maybe beta[2])
b) [2]forall a. (F b ty ~ beta[2], G beta[2] ~ gamma[2])
b1) [2]forall a. (F a ty ~ beta[2], G beta[2] ~ gamma[2])
b2) [2]forall a. (a ~ beta[2], G beta[2] ~ gamma[2])
c) [2]forall a. (F a ty ~ beta[2], delta[1] ~ Maybe beta[2])
d) [2]forall a. (gamma[1] ~ Tree beta[2], F ty ~ beta[2])
In (a) we *must* float out the second equality,
else we can't solve at all (Trac #7804).
In (b) we *must not* float out the second equality.
It will ultimately be solved (by flattening) in situ, but if we
float it we'll promote beta,gamma, and render the first equality insoluble.
In (b1, b2) we *must not* float out the second equality.
It will ultimately be solved (by flattening) in situ, but if we float
it we'll promote beta,gamma, and render the first equality insoluble.
Trac #9316 was an example of (b2). You may wonder why (a ~ beta[2]) isn't
solved; in #9316 it wasn't solved because (a:*) and (beta:kappa[1]), so the
equality was kind-mismatched, and hence was a CIrredEvCan. There was
another equality alongside, (kappa[1] ~ *). We must first float *that*
one out and *then* we can solve (a ~ beta).
In (c) it would be OK to float the second equality but better not to.
If we flatten we see (delta[1] ~ Maybe (F a ty)), which is a
skolem-escape problem. If we float the secodn equality we'll
skolem-escape problem. If we float the second equality we'll
end up with (F a ty ~ beta'[1]), which is a less explicable error.
Hence we start with the skolems, grow them by the CFunEqCans, and
float ones that don't mention the grown variables. Seems very ad hoc.
Note [Promoting unification variables]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
When we float an equality out of an implication we must "promote" free
unification variables of the equality, in order to maintain Invariant
(MetaTvInv) from Note [Untouchable type variables] in TcType. for the
leftover implication.
This is absolutely necessary. Consider the following example. We start
with two implications and a class with a functional dependency.
class C x y | x -> y
instance C [a] [a]
(I1) [untch=beta]forall b. 0 => F Int ~ [beta]
(I2) [untch=beta]forall c. 0 => F Int ~ [[alpha]] /\ C beta [c]
We float (F Int ~ [beta]) out of I1, and we float (F Int ~ [[alpha]]) out of I2.
They may react to yield that (beta := [alpha]) which can then be pushed inwards
the leftover of I2 to get (C [alpha] [a]) which, using the FunDep, will mean that
(alpha := a). In the end we will have the skolem 'b' escaping in the untouchable
beta! Concrete example is in indexed_types/should_fail/ExtraTcsUntch.hs:
class C x y | x -> y where
op :: x -> y -> ()
instance C [a] [a]
type family F a :: *
h :: F Int -> ()
h = undefined
data TEx where
TEx :: a -> TEx
In (d) we must float the first equality, so that we can unify gamma.
But that promotes beta, so we must float the second equality too,
Trac #7196 exhibits this case
Some notes
f (x::beta) =
let g1 :: forall b. b -> ()
g1 _ = h [x]
g2 z = case z of TEx y -> (h [[undefined]], op x [y])
in (g1 '3', g2 undefined)
* When "growing", do not simply take the free vars of the predicate!
Example [2]forall a. (a:* ~ beta[2]:kappa[1]), (kappa[1] ~ *)
We must float the second, and we must not float the first.
But the first actually looks like ((~) kappa a beta), so if we just
look at its free variables we'll see {a,kappa,beta), and that might
make us think kappa should be in the grown skol set.
(In any case, the kind argument for a kind-mis-matched equality like
this one doesn't really make sense anyway.)
That's why we use classifyPred when growing.
Note [Solving Family Equations]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
After we are done with simplification we may be left with constraints of the form:
[Wanted] F xis ~ beta
If 'beta' is a touchable unification variable not already bound in the TyBinds
then we'd like to create a binding for it, effectively "defaulting" it to be 'F xis'.
When is it ok to do so?
1) 'beta' must not already be defaulted to something. Example:
* Previously we tried to "grow" the skol_set with *all* the
constraints (not just equalities), to get all the tyvars that could
*conceivably* unify with the skolems, but that was far too
conservative (Trac #7804). Example: this should be fine:
f :: (forall a. a -> Proxy x -> Proxy (F x)) -> Int
f = error "Urk" :: (forall a. a -> Proxy x -> Proxy (F x)) -> Int
[Wanted] F Int ~ beta <~ Will default [beta := F Int]
[Wanted] F Char ~ beta <~ Already defaulted, can't default again. We
have to report this as unsolved.
2) However, we must still do an occurs check when defaulting (F xis ~ beta), to
set [beta := F xis] only if beta is not among the free variables of xis.
Note [Skolem escape]
~~~~~~~~~~~~~~~~~~~~
You might worry about skolem escape with all this floating.
For example, consider
[2] forall a. (a ~ F beta[2] delta,
Maybe beta[2] ~ gamma[1])
3) Notice that 'beta' can't be bound in ty binds already because we rewrite RHS
of type family equations. See Inert Set invariants in TcInteract.
The (Maybe beta ~ gamma) doesn't mention 'a', so we float it, and
solve with gamma := beta. But what if later delta:=Int, and
F b Int = b.
Then we'd get a ~ beta[2], and solve to get beta:=a, and now the
skolem has escaped!
This solving is now happening during zonking, see Note [Unflattening while zonking]
in TcMType.
But it's ok: when we float (Maybe beta[2] ~ gamma[1]), we promote beta[2]
to beta[1], and that means the (a ~ beta[1]) will be stuck, as it should be.
*********************************************************************************
......
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE QuasiQuotes #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE FlexibleInstances #-}
module SingletonsBug where
import Control.Applicative
import Data.Traversable (for)
import GHC.Exts( Constraint )
-----------------------------------
-- From 'constraints' library
-- import Data.Constraint (Dict(..))
data Dict :: Constraint -> * where
Dict :: a => Dict a
-----------------------------------
-- From 'singletons' library
-- import Data.Singletons hiding( withSomeSing )
class SingI (a :: k) where
-- | Produce the singleton explicitly. You will likely need the @ScopedTypeVariables@
-- extension to use this method the way you want.
sing :: Sing a
data family Sing (a :: k)
data KProxy (a :: *) = KProxy
data SomeSing (kproxy :: KProxy k) where
SomeSing :: Sing (a :: k) -> SomeSing ('KProxy :: KProxy k)
-- SingKind :: forall k. KProxy k -> Constraint
class (kparam ~ 'KProxy) => SingKind (kparam :: KProxy k) where
-- | Get a base type from a proxy for the promoted kind. For example,
-- @DemoteRep ('KProxy :: KProxy Bool)@ will be the type @Bool@.
type DemoteRep kparam :: *
-- | Convert a singleton to its unrefined version.
fromSing :: Sing (a :: k) -> DemoteRep kparam
-- | Convert an unrefined type to an existentially-quantified singleton type.
toSing :: DemoteRep kparam -> SomeSing kparam
withSomeSing :: SingKind ('KProxy :: KProxy k)
=> DemoteRep ('KProxy :: KProxy k)
-> (forall (a :: k). Sing a -> r)
-> r
withSomeSing = error "urk"
-----------------------------------
data SubscriptionChannel = BookingsChannel
type BookingsChannelSym0 = BookingsChannel
data instance Sing (z_a5I7 :: SubscriptionChannel) where
SBookingsChannel :: Sing BookingsChannel
instance SingKind ('KProxy :: KProxy SubscriptionChannel) where
type DemoteRep ('KProxy :: KProxy SubscriptionChannel) = SubscriptionChannel
fromSing SBookingsChannel = BookingsChannel
toSing BookingsChannel = SomeSing SBookingsChannel
instance SingI BookingsChannel where
sing = SBookingsChannel
type family T (c :: SubscriptionChannel) :: *
type instance T 'BookingsChannel = Bool
witnessC :: Sing channel -> Dict (Show (T channel), SingI channel)
witnessC SBookingsChannel = Dict
forAllSubscriptionChannels
:: forall m r. (Applicative m)
=> (forall channel. (SingI channel, Show (T channel)) => Sing channel -> m r)
-> m r
forAllSubscriptionChannels f =
withSomeSing BookingsChannel $ \(sChannel) ->
case witnessC sChannel of
Dict -> f sChannel
......@@ -244,3 +244,4 @@ test('T8913', normal, compile, [''])
test('T8978', normal, compile, [''])
test('T8979', normal, compile, [''])
test('T9085', normal, compile, [''])
test('T9316', normal, compile, [''])
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment