Wibbles (mainly comments)wip/T2893

6 files changed, 29 insertions, 14 deletions

diff --git a/compiler/typecheck/TcCanonical.hs b/compiler/typecheck/TcCanonical.hs
index 87749da764..980154c8dc 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 2c27e51ccc..ec6ac0f650 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 f9e7831d9a..927690c796 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 98ceb6e031..09827e458b 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 580496b5ed..e0e0342b61 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 f417e6a934..d6ca149f23 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