Commit 12cfcbeb authored by Simon Peyton Jones's avatar Simon Peyton Jones Committed by Ben Gamari

Orient improvement constraints better

This patch fixes an infinite loop in the constraint solver,
shown up by Trac #12522.

The solution is /very/ simple: just reverse the orientation of the
derived constraints arising from improvement using type-family
injectivity.  I'm not very proud of the fix --- it seems fragile
--- but it has the very great merit of simplicity, and it works
fine.

See Note [Improvement orientation] in TcInteract, and some
discussion on the Trac ticket.

(cherry picked from commit b255ae7b)
parent 5662ceae
......@@ -779,9 +779,8 @@ interactGivenIP inerts workItem@(CDictCan { cc_ev = ev, cc_class = cls
interactGivenIP _ wi = pprPanic "interactGivenIP" (ppr wi)
{-
Note [Shadowing of Implicit Parameters]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
{- Note [Shadowing of Implicit Parameters]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Consider the following example:
f :: (?x :: Char) => Char
......@@ -804,8 +803,19 @@ signature, and we implement this as follows: when we add a new
*given* implicit parameter to the inert set, it replaces any existing
givens for the same implicit parameter.
This works for the normal cases but it has an odd side effect
in some pathological programs like this:
Similarly, consider
f :: (?x::a) => Bool -> a
g v = let ?x::Int = 3
in (f v, let ?x::Bool = True in f v)
This should probably be well typed, with
g :: Bool -> (Int, Bool)
So the inner binding for ?x::Bool *overrides* the outer one.
All this works for the normal cases but it has an odd side effect in
some pathological programs like this:
-- This is accepted, the second parameter shadows
f1 :: (?x :: Int, ?x :: Char) => Char
......@@ -821,7 +831,7 @@ which would lead to an error.
I can think of two ways to fix this:
1. Simply disallow multiple constratits for the same implicit
1. Simply disallow multiple constraints for the same implicit
parameter---this is never useful, and it can be detected completely
syntactically.
......@@ -1498,11 +1508,13 @@ improve_top_fun_eqs fam_envs fam_tc args rhs_ty
-- part of the tuple, which is the range of the substitution then
-- the order could be important.
let subst = theta `unionTCvSubst` theta'
return [ Pair arg (substTyUnchecked subst ax_arg)
return [ Pair (substTyUnchecked subst ax_arg) arg
-- NB: the ax_arg part is on the left
-- see Note [Improvement orientation]
| case cabr of
Just cabr' -> apartnessCheck (substTys subst ax_args) cabr'
_ -> True
, (arg, ax_arg, True) <- zip3 args ax_args inj_args ]
, (ax_arg, arg, True) <- zip3 ax_args args inj_args ]
shortCutReduction :: CtEvidence -> TcTyVar -> TcCoercion
......@@ -1687,7 +1699,6 @@ Then it is solvable, but its very hard to detect this on the spot.
It's exactly the same with implicit parameters, except that the
"aggressive" approach would be much easier to implement.
Note [Weird fundeps]
~~~~~~~~~~~~~~~~~~~~
Consider class Het a b | a -> b where
......@@ -1709,19 +1720,42 @@ as the fundeps.
Trac #7875 is a case in point.
Note [Overriding implicit parameters]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Consider
f :: (?x::a) -> Bool -> a
g v = let ?x::Int = 3
in (f v, let ?x::Bool = True in f v)
This should probably be well typed, with
g :: Bool -> (Int, Bool)
So the inner binding for ?x::Bool *overrides* the outer one.
Hence a work-item Given overrides an inert-item Given.
Note [Improvement orientation]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
A very delicate point is the orientation of derived equalities
arising from injectivity improvement (Trac #12522). Suppse we have
type family F x = t | t -> x
type instance F (a, Int) = (Int, G a)
where G is injective; and wanted constraints
[W] TF (alpha, beta) ~ fuv
[W] fuv ~ (Int, <some type>)
The injectivity will give rise to derived constraionts
[D] gamma1 ~ alpha
[D] Int ~ beta
The fresh unification variable gamma1 comes from the fact that we
can only do "partial improvement" here; see Section 5.2 of
"Injective type families for Haskell" (HS'15).
Now, it's very important to orient the equations this way round,
so that the fresh unification variable will be eliminated in
favour of alpha. If we instead had
[D] alpha ~ gamma1
then we would unify alpha := gamma1; and kick out the wanted
constraint. But when we grough it back in, it'd look like
[W] TF (gamma1, beta) ~ fuv
and exactly the same thing would happen again! Infnite loop.
This all sesms fragile, and it might seem more robust to avoid
introducing gamma1 in the first place, in the case where the
actual argument (alpha, beta) partly matches the improvement
template. But that's a bit tricky, esp when we remember that the
kinds much match too; so it's easier to let the normal machinery
handle it. Instead we are careful to orient the new derived
equality with the template on the left. Delicate, but it works.
-}
{- *******************************************************************
......
{-# LANGUAGE TypeFamilyDependencies #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE AllowAmbiguousTypes #-}
module T12522 where
foo = f (Just 'c')
data D1 x
data D2
type family TF x = t | t -> x
type instance TF (D1 x, a) = Maybe (TF (x, a))
type instance TF (D2, ()) = Char
f :: TF (x, a) -> ()
f _ = ()
foo1 = f_good (Just 'c')
foo2 = f_bad (Just 'c')
type family TF2 x y = t | t -> x y
type instance TF2 Int Float = Char
type family TF_Good x y = t | t -> x y
type instance TF_Good a (Maybe x) = Maybe (TF2 a x)
f_good :: TF_Good a x -> ()
f_good _ = ()
type family TF_Bad x y = t | t -> x y
type instance TF_Bad (Maybe x) a = Maybe (TF2 a x)
f_bad :: TF_Bad x a -> ()
f_bad _ = ()
{-
Maybe Char ~ TF (xx, aa)
Model [D] s_aF4 ~ Maybe Char
[W] TF (x_aDY, a_aJn) ~ s_aF4 FunEq
--> {aJn = aJp)
[W} TF (x_aDY, a_aJp) ~ s_aF4 FunEq
--> {new derived equalities}
[D] x_aDY ~ D1 x_aJq
[D] a_aJp ~ a_aJR
-}
......@@ -274,3 +274,4 @@ test('T11408', normal, compile, [''])
test('T11361', normal, compile, [''])
test('T11361a', normal, compile_fail, [''])
test('T12175', normal, compile, [''])
test('T12522', 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