From 80afdf6be11ae3b5bfd1b09dbc5f5118a9dde55a Mon Sep 17 00:00:00 2001
From: Simon Peyton Jones <simonpj@microsoft.com>
Date: Thu, 4 Jul 2019 08:41:12 +0100
Subject: [PATCH] Fix over-eager implication constraint discard
Ticket #16247 showed that we were discarding an implication
constraint that had empty ic_wanted, when we still needed to
keep it so we could check whether it had a bad telescope.
Happily it's a one line fix. All the rest is comments!
---
compiler/typecheck/TcHsType.hs | 2 ++
compiler/typecheck/TcRnTypes.hs | 44 +++++++++++++++++++++---
compiler/typecheck/TcUnify.hs | 7 ++++
testsuite/tests/polykinds/T16247.hs | 10 ++++++
testsuite/tests/polykinds/T16247.stderr | 7 ++++
testsuite/tests/polykinds/T16247a.hs | 23 +++++++++++++
testsuite/tests/polykinds/T16247a.stderr | 8 +++++
testsuite/tests/polykinds/all.T | 2 ++
8 files changed, 98 insertions(+), 5 deletions(-)
create mode 100644 testsuite/tests/polykinds/T16247.hs
create mode 100644 testsuite/tests/polykinds/T16247.stderr
create mode 100644 testsuite/tests/polykinds/T16247a.hs
create mode 100644 testsuite/tests/polykinds/T16247a.stderr
diff --git a/compiler/typecheck/TcHsType.hs b/compiler/typecheck/TcHsType.hs
index fac6f2e31cfa..a7e3cf7945fd 100644
--- a/compiler/typecheck/TcHsType.hs
+++ b/compiler/typecheck/TcHsType.hs
@@ -1652,6 +1652,8 @@ is correct, choosing ImplicationStatus IC_BadTelescope if they aren't.
Then, in TcErrors, we report if there is a bad telescope. This way,
we can report a suggested ordering to the user if there is a problem.
+See also Note [Checking telescopes] in TcRnTypes
+
Note [Keeping scoped variables in order: Implicit]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
When the user implicitly quantifies over variables (say, in a type
diff --git a/compiler/typecheck/TcRnTypes.hs b/compiler/typecheck/TcRnTypes.hs
index c8d83215fd15..8882bbc6c7dc 100644
--- a/compiler/typecheck/TcRnTypes.hs
+++ b/compiler/typecheck/TcRnTypes.hs
@@ -2587,11 +2587,9 @@ data Implication
ic_skols :: [TcTyVar], -- Introduced skolems
ic_info :: SkolemInfo, -- See Note [Skolems in an implication]
-- See Note [Shadowing in a constraint]
+
ic_telescope :: Maybe SDoc, -- User-written telescope, if there is one
- -- The list of skolems is order-checked
- -- if and only if this is a Just.
- -- See Note [Keeping scoped variables in order: Explicit]
- -- in TcHsType
+ -- See Note [Checking telescopes]
ic_given :: [EvVar], -- Given evidence variables
-- (order does not matter)
@@ -2708,7 +2706,43 @@ instance Outputable ImplicStatus where
ppr (IC_Solved { ics_dead = dead })
= text "Solved" <+> (braces (text "Dead givens =" <+> ppr dead))
-{-
+{- Note [Checking telescopes]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+When kind-checking a /user-written/ type, we might have a "bad telescope"
+like this one:
+ data SameKind :: forall k. k -> k -> Type
+ type Foo :: forall a k (b :: k). SameKind a b -> Type
+
+The kind of 'a' mentions 'k' which is bound after 'a'. Oops.
+
+Knowing this means that unification etc must have happened, so it's
+convenient to detect it in the constraint solver:
+
+* We make a single implication constraint when kind-checking
+ the 'forall' in Foo's kind, something like
+ forall a k (b::k). { wanted constraints }
+
+* Having solved {wanted}, before discarding the now-solved implication,
+ the costraint solver checks the dependency order of the skolem
+ variables (ic_skols). This is done in setImplicationStatus.
+
+* This check is only necessary if the implication was born from a
+ user-written signature. If, say, it comes from checking a pattern
+ match that binds existentials, where the type of the data constructor
+ is known to be valid (it in tcConPat), no need for the check.
+
+ So the check is done if and only if ic_telescope is (Just blah).
+
+* If ic_telesope is (Just d), the d::SDoc displays the original,
+ user-written type variables.
+
+* Be careful /NOT/ to discard an implication with non-Nothing
+ ic_telescope, even if ic_wanted is empty. We must give the
+ constraint solver a chance to make that bad-telesope test! Hence
+ the extra guard in emitResidualTvConstraint; see #16247
+
+See also TcHsTYpe Note [Keeping scoped variables in order: Explicit]
+
Note [Needed evidence variables]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Th ic_need_evs field holds the free vars of ic_binds, and all the
diff --git a/compiler/typecheck/TcUnify.hs b/compiler/typecheck/TcUnify.hs
index 35f4d00f3981..45cc3f916849 100644
--- a/compiler/typecheck/TcUnify.hs
+++ b/compiler/typecheck/TcUnify.hs
@@ -64,6 +64,7 @@ import Util
import qualified GHC.LanguageExtensions as LangExt
import Outputable
+import Data.Maybe( isNothing )
import Control.Monad
import Control.Arrow ( second )
@@ -1176,7 +1177,13 @@ emitResidualTvConstraint :: SkolemInfo -> Maybe SDoc -> [TcTyVar]
-> TcLevel -> WantedConstraints -> TcM ()
emitResidualTvConstraint skol_info m_telescope skol_tvs tclvl wanted
| isEmptyWC wanted
+ , isNothing m_telescope || skol_tvs `lengthAtMost` 1
+ -- If m_telescope is (Just d), we must do the bad-telescope check,
+ -- so we must /not/ discard the implication even if there are no
+ -- wanted constraints. See Note [Checking telescopes] in TcRnTypes.
+ -- Lacking this check led to #16247
= return ()
+
| otherwise
= do { ev_binds <- newNoTcEvBinds
; implic <- newImplication
diff --git a/testsuite/tests/polykinds/T16247.hs b/testsuite/tests/polykinds/T16247.hs
new file mode 100644
index 000000000000..617f3c4acae8
--- /dev/null
+++ b/testsuite/tests/polykinds/T16247.hs
@@ -0,0 +1,10 @@
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TypeInType #-}
+module Bug where
+
+import Data.Kind
+
+data SameKind :: forall k. k -> k -> Type
+data Foo :: forall a k (b :: k). SameKind a b -> Type where
+ MkFoo :: Foo sameKind
diff --git a/testsuite/tests/polykinds/T16247.stderr b/testsuite/tests/polykinds/T16247.stderr
new file mode 100644
index 000000000000..34a131999678
--- /dev/null
+++ b/testsuite/tests/polykinds/T16247.stderr
@@ -0,0 +1,7 @@
+
+T16247.hs:9:13: error:
+ • These kind and type variables: a k (b :: k)
+ are out of dependency order. Perhaps try this ordering:
+ k (a :: k) (b :: k)
+ • In the kind ‘forall a k (b :: k). SameKind a b -> Type’
+ In the data type declaration for ‘Foo’
diff --git a/testsuite/tests/polykinds/T16247a.hs b/testsuite/tests/polykinds/T16247a.hs
new file mode 100644
index 000000000000..60a98d6c8f4e
--- /dev/null
+++ b/testsuite/tests/polykinds/T16247a.hs
@@ -0,0 +1,23 @@
+{-# LANGUAGE ConstraintKinds #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE TypeInType #-}
+{-# LANGUAGE TypeOperators #-}
+module Bug where
+
+import Data.Kind (Constraint, Type)
+import GHC.Generics (Rep1, U1(..))
+
+data TyFun :: Type -> Type -> Type
+type a ~> b = TyFun a b -> Type
+infixr 0 ~>
+type family Apply (f :: a ~> b) (x :: a) :: b
+type SameKind (a :: k) (b :: k) = (() :: Constraint)
+
+type family From1 (z :: (f :: Type -> Type) a) :: Rep1 f a
+
+type family From1U1 (x :: U1 (p :: k)) :: Rep1 U1 p where {}
+data From1U1Sym0 :: forall p k. (U1 :: k -> Type) p ~> Rep1 (U1 :: k -> Type) p where
+ From1Sym0KindInference :: forall z arg. SameKind (Apply From1U1Sym0 arg) (From1U1 arg)
+ => From1U1Sym0 z
diff --git a/testsuite/tests/polykinds/T16247a.stderr b/testsuite/tests/polykinds/T16247a.stderr
new file mode 100644
index 000000000000..ce75878f389b
--- /dev/null
+++ b/testsuite/tests/polykinds/T16247a.stderr
@@ -0,0 +1,8 @@
+
+T16247a.hs:21:21: error:
+ • These kind and type variables: p k
+ are out of dependency order. Perhaps try this ordering:
+ k (p :: k)
+ • In the kind ‘forall p k.
+ (U1 :: k -> Type) p ~> Rep1 (U1 :: k -> Type) p’
+ In the data type declaration for ‘From1U1Sym0’
diff --git a/testsuite/tests/polykinds/all.T b/testsuite/tests/polykinds/all.T
index c67d80d621a0..6238fbe770a0 100644
--- a/testsuite/tests/polykinds/all.T
+++ b/testsuite/tests/polykinds/all.T
@@ -206,6 +206,8 @@ test('T14887a', normal, compile, [''])
test('T14847', normal, compile, [''])
test('T15795', normal, compile, [''])
test('T15795a', normal, compile, [''])
+test('T16247', normal, compile_fail, [''])
+test('T16247a', normal, compile_fail, [''])
test('KindVarOrder', normal, ghci_script, ['KindVarOrder.script'])
test('T16221', normal, compile, [''])
test('T16221a', normal, compile_fail, [''])
--
GitLab