[commit: ghc] wip/T2893: Wibbles (mainly comments) (8308b2d)
git at git.haskell.org
git at git.haskell.org
Fri Jun 1 14:53:13 UTC 2018
Repository : ssh://git@git.haskell.org/ghc
On branch : wip/T2893
Link : http://ghc.haskell.org/trac/ghc/changeset/8308b2dfc2fb1ab89e2c3449960cf577b43a1612/ghc
>---------------------------------------------------------------
commit 8308b2dfc2fb1ab89e2c3449960cf577b43a1612
Author: Simon Peyton Jones <simonpj at microsoft.com>
Date: Fri Jun 1 12:06:40 2018 +0100
Wibbles (mainly comments)
>---------------------------------------------------------------
8308b2dfc2fb1ab89e2c3449960cf577b43a1612
compiler/typecheck/TcCanonical.hs | 7 ++++--
compiler/typecheck/TcInteract.hs | 1 -
compiler/typecheck/TcValidity.hs | 27 ++++++++++++++++------
testsuite/tests/typecheck/should_fail/T7019.stderr | 2 +-
.../tests/typecheck/should_fail/T7019a.stderr | 2 +-
testsuite/tests/typecheck/should_fail/T9196.stderr | 4 ++--
6 files changed, 29 insertions(+), 14 deletions(-)
diff --git a/compiler/typecheck/TcCanonical.hs b/compiler/typecheck/TcCanonical.hs
index 87749da..980154c 100644
--- a/compiler/typecheck/TcCanonical.hs
+++ b/compiler/typecheck/TcCanonical.hs
@@ -452,8 +452,11 @@ makeSuperClasses cts = concatMapM go cts
(tvs, theta, cls, tys) = tcSplitDFunTy (ctEvPred ev)
go ct = pprPanic "makeSuperClasses" (ppr ct)
-mkStrictSuperClasses :: CtEvidence -> [TyVar] -> ThetaType
- -> Class -> [Type] -> TcS [Ct]
+mkStrictSuperClasses
+ :: CtEvidence
+ -> [TyVar] -> ThetaType -- These two args are non-empty only when taking
+ -- superclasses of a /quantified/ constraint
+ -> Class -> [Type] -> TcS [Ct]
-- Return constraints for the strict superclasses of
-- ev :: forall as. theta => cls tys
mkStrictSuperClasses ev tvs theta cls tys
diff --git a/compiler/typecheck/TcInteract.hs b/compiler/typecheck/TcInteract.hs
index 2c27e51..ec6ac0f 100644
--- a/compiler/typecheck/TcInteract.hs
+++ b/compiler/typecheck/TcInteract.hs
@@ -2041,7 +2041,6 @@ shortCutReduction old_ev fsk ax_co fam_tc tc_args
where
deeper_loc = bumpCtLocDepth (ctEvLoc old_ev)
-
{- Note [Top-level reductions for type functions]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
c.f. Note [The flattening story] in TcFlatten
diff --git a/compiler/typecheck/TcValidity.hs b/compiler/typecheck/TcValidity.hs
index f9e7831..927690c 100644
--- a/compiler/typecheck/TcValidity.hs
+++ b/compiler/typecheck/TcValidity.hs
@@ -442,7 +442,7 @@ rankZeroMonoType = MonoType (text "Perhaps you intended to use RankNTypes or R
tyConArgMonoType = MonoType (text "GHC doesn't yet support impredicative polymorphism")
synArgMonoType = MonoType (text "Perhaps you intended to use LiberalTypeSynonyms")
constraintMonoType = MonoType (vcat [ text "A constraint must be a monotype"
- , text "Perhpas you intended to use QuantifiedConstraints" ])
+ , text "Perhaps you intended to use QuantifiedConstraints" ])
funArgResRank :: Rank -> (Rank, Rank) -- Function argument and result
funArgResRank (LimitedRank _ arg_rank) = (arg_rank, LimitedRank (forAllAllowed arg_rank) arg_rank)
@@ -1409,6 +1409,7 @@ checkInstTermination theta head_pred
-> check2 foralld_tvs pred bogus_size
where
bogus_size = 1 + sizeTypes (filterOutInvisibleTypes (classTyCon cls) tys)
+ -- See Note [Invisible arguments and termination]
ForAllPred tvs theta pred
-> do { check (foralld_tvs `extendVarSetList` binderVars tvs) pred
@@ -1570,6 +1571,20 @@ Here the instance is kind-indexed and really looks like
type F (k->k) (b::k->k) = Int
But if the 'b' didn't scope, we would make F's instance too
poly-kinded.
+
+Note [Invisible arguments and termination]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+When checking the Paterson conditions for termination an instance
+declaration, we check for the number of "constructors and variables"
+in the instance head and constraints. Question: Do we look at
+
+ * All the arguments, visible or invisible?
+ * Just the visible arguments?
+
+I think both will ensure termination, provided we are consistent.
+Currently we are /not/ consistent, which is really a bug. It's
+described in Trac #15177, which contains a number of examples.
+The suspicious bits are the calls to filterOutInvisibleTypes.
-}
-- | Extra information about the parent instance declaration, needed
@@ -2001,10 +2016,7 @@ sizeTypes = foldr ((+) . sizeType) 0
sizeTyConAppArgs :: TyCon -> [Type] -> Int
sizeTyConAppArgs _tc tys = sizeTypes tys -- (filterOutInvisibleTypes tc tys)
-
--- instance (Category w, Prelude.Monad m) => Monad (WriterT w m) where
--- Category * w_auL
--- Monad (WriterT w_auL m_auM)
+ -- See Note [Invisible arguments and termination]
-- Size of a predicate
--
@@ -2020,10 +2032,11 @@ sizePred ty = goClass ty
go (ClassPred cls tys')
| isTerminatingClass cls = 0
| otherwise = sizeTypes (filterOutInvisibleTypes (classTyCon cls) tys')
- -- The filtering looks bogus: see Trac #15177
+ -- The filtering looks bogus
+ -- See Note [Invisible arguments and termination]
go (EqPred {}) = 0
go (IrredPred ty) = sizeType ty
- go (ForAllPred _ _ pred) = goClass pred -- Is this right?
+ go (ForAllPred _ _ pred) = goClass pred
-- | When this says "True", ignore this class constraint during
-- a termination check
diff --git a/testsuite/tests/typecheck/should_fail/T7019.stderr b/testsuite/tests/typecheck/should_fail/T7019.stderr
index 98ceb6e..09827e4 100644
--- a/testsuite/tests/typecheck/should_fail/T7019.stderr
+++ b/testsuite/tests/typecheck/should_fail/T7019.stderr
@@ -2,5 +2,5 @@
T7019.hs:11:1: error:
• Illegal polymorphic type: forall a. c (Free c a)
A constraint must be a monotype
- Perhpas you intended to use QuantifiedConstraints
+ Perhaps you intended to use QuantifiedConstraints
• In the type synonym declaration for ‘C’
diff --git a/testsuite/tests/typecheck/should_fail/T7019a.stderr b/testsuite/tests/typecheck/should_fail/T7019a.stderr
index 580496b..e0e0342 100644
--- a/testsuite/tests/typecheck/should_fail/T7019a.stderr
+++ b/testsuite/tests/typecheck/should_fail/T7019a.stderr
@@ -2,7 +2,7 @@
T7019a.hs:11:1: error:
• Illegal polymorphic type: forall b. Context (Associated a b)
A constraint must be a monotype
- Perhpas you intended to use QuantifiedConstraints
+ Perhaps you intended to use QuantifiedConstraints
• In the context: forall b. Context (Associated a b)
While checking the super-classes of class ‘Class’
In the class declaration for ‘Class’
diff --git a/testsuite/tests/typecheck/should_fail/T9196.stderr b/testsuite/tests/typecheck/should_fail/T9196.stderr
index f417e6a..d6ca149 100644
--- a/testsuite/tests/typecheck/should_fail/T9196.stderr
+++ b/testsuite/tests/typecheck/should_fail/T9196.stderr
@@ -2,11 +2,11 @@
T9196.hs:4:6: error:
• Illegal polymorphic type: forall a1. Eq a1
A constraint must be a monotype
- Perhpas you intended to use QuantifiedConstraints
+ Perhaps you intended to use QuantifiedConstraints
• In the type signature: f :: (forall a. Eq a) => a -> a
T9196.hs:7:6: error:
• Illegal qualified type: Eq a => Ord a
A constraint must be a monotype
- Perhpas you intended to use QuantifiedConstraints
+ Perhaps you intended to use QuantifiedConstraints
• In the type signature: g :: (Eq a => Ord a) => a -> a
More information about the ghc-commits
mailing list