Orient improvement constraints better
authorSimon Peyton Jones <simonpj@microsoft.com>
Fri, 7 Oct 2016 22:51:44 +0000 (23:51 +0100)
committerBen Gamari <ben@smart-cactus.org>
Mon, 10 Oct 2016 13:56:03 +0000 (09:56 -0400)
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 b255ae7b555b4b63085a6de4a7a6bd742326b9c9)

compiler/typecheck/TcInteract.hs
testsuite/tests/indexed-types/should_compile/T12522.hs [new file with mode: 0644]
testsuite/tests/indexed-types/should_compile/all.T

index 259c570..402e6da 100644 (file)
@@ -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.
 -}
 
 {- *******************************************************************
diff --git a/testsuite/tests/indexed-types/should_compile/T12522.hs b/testsuite/tests/indexed-types/should_compile/T12522.hs
new file mode 100644 (file)
index 0000000..7779942
--- /dev/null
@@ -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
+-}
index d88505e..9763d89 100644 (file)
@@ -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, [''])