[commit: ghc] master: Orient improvement constraints better (b255ae7)
git at git.haskell.org
git at git.haskell.org
Mon Oct 10 10:51:25 UTC 2016
Repository : ssh://git@git.haskell.org/ghc
On branch : master
Link : http://ghc.haskell.org/trac/ghc/changeset/b255ae7b555b4b63085a6de4a7a6bd742326b9c9/ghc
>---------------------------------------------------------------
commit b255ae7b555b4b63085a6de4a7a6bd742326b9c9
Author: Simon Peyton Jones <simonpj at microsoft.com>
Date: Fri Oct 7 23:51:44 2016 +0100
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.
>---------------------------------------------------------------
b255ae7b555b4b63085a6de4a7a6bd742326b9c9
compiler/typecheck/TcInteract.hs | 78 ++++++++++++++++------
.../tests/indexed-types/should_compile/T12522.hs | 50 ++++++++++++++
testsuite/tests/indexed-types/should_compile/all.T | 1 +
3 files changed, 107 insertions(+), 22 deletions(-)
diff --git a/compiler/typecheck/TcInteract.hs b/compiler/typecheck/TcInteract.hs
index 75224d8..05efceb 100644
--- a/compiler/typecheck/TcInteract.hs
+++ b/compiler/typecheck/TcInteract.hs
@@ -782,9 +782,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
@@ -807,8 +806,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
@@ -824,7 +834,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.
@@ -1501,11 +1511,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
@@ -1690,7 +1702,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
@@ -1712,19 +1723,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.
-}
{- *******************************************************************
diff --git a/testsuite/tests/indexed-types/should_compile/T12522.hs b/testsuite/tests/indexed-types/should_compile/T12522.hs
new file mode 100644
index 0000000..7779942
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_compile/T12522.hs
@@ -0,0 +1,50 @@
+{-# 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
+-}
diff --git a/testsuite/tests/indexed-types/should_compile/all.T b/testsuite/tests/indexed-types/should_compile/all.T
index 84cd5dc..4eeb777 100644
--- a/testsuite/tests/indexed-types/should_compile/all.T
+++ b/testsuite/tests/indexed-types/should_compile/all.T
@@ -274,3 +274,4 @@ test('T11361', normal, compile, ['-dunique-increment=-1'])
test('T11361a', normal, compile_fail, [''])
test('T11581', normal, compile, [''])
test('T12175', normal, compile, [''])
+test('T12522', normal, compile, [''])
More information about the ghc-commits
mailing list