Add "quantified constraint" context in error message, fix #15231.
authorHE, Tao <sighingnow@gmail.com>
Fri, 15 Jun 2018 17:45:42 +0000 (13:45 -0400)
committerBen Gamari <ben@smart-cactus.org>
Fri, 15 Jun 2018 17:47:42 +0000 (13:47 -0400)
This patch adds "quantified constraint" context in error message when
UndecidableInstances checking fails for quantified constraints.
See Trac #15231:comment#1.

This patch also pretty-prints the instance head for better error messages.

Test Plan: make test TEST="T15231"

Reviewers: bgamari, simonpj

Reviewed By: simonpj

Subscribers: simonpj, rwbarton, thomie, carter

GHC Trac Issues: #15231

Differential Revision: https://phabricator.haskell.org/D4819

12 files changed:
compiler/typecheck/TcValidity.hs
testsuite/tests/deriving/should_fail/T8165_fail2.stderr
testsuite/tests/indexed-types/should_fail/NotRelaxedExamples.stderr
testsuite/tests/indexed-types/should_fail/T10817.stderr
testsuite/tests/indexed-types/should_fail/TyFamUndec.stderr
testsuite/tests/quantified-constraints/T15231.hs [new file with mode: 0644]
testsuite/tests/quantified-constraints/T15231.stderr [new file with mode: 0644]
testsuite/tests/quantified-constraints/all.T
testsuite/tests/typecheck/should_fail/fd-loop.stderr
testsuite/tests/typecheck/should_fail/tcfail108.stderr
testsuite/tests/typecheck/should_fail/tcfail154.stderr
testsuite/tests/typecheck/should_fail/tcfail157.stderr

index 8572d32..84309db 100644 (file)
@@ -1411,14 +1411,16 @@ checkInstTermination theta head_pred
               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
-                 ; checkInstTermination theta pred }
+         ForAllPred tvs theta' head_pred'
+           -> do { check (foralld_tvs `extendVarSetList` binderVars tvs) head_pred'
+                 ; addErrCtxt (text "In the quantified constraint"
+                              <+> quotes (ppr pred)) $
+                   checkInstTermination theta' head_pred' }
 
    check2 foralld_tvs pred pred_size
-     | not (null bad_tvs)     = addErrTc (noMoreMsg bad_tvs what)
+     | not (null bad_tvs)     = addErrTc (noMoreMsg bad_tvs what (ppr head_pred))
      | not (isTyFamFree pred) = addErrTc (nestedMsg what)
-     | pred_size >= head_size = addErrTc (smallerMsg what)
+     | pred_size >= head_size = addErrTc (smallerMsg what (ppr head_pred))
      | otherwise              = return ()
      -- isTyFamFree: see Note [Type families in instance contexts]
      where
@@ -1426,18 +1428,19 @@ checkInstTermination theta head_pred
         bad_tvs = filterOut (`elemVarSet` foralld_tvs) (fvType pred)
                   \\ head_fvs
 
-smallerMsg :: SDoc -> SDoc
-smallerMsg what
+smallerMsg :: SDoc -> SDoc -> SDoc
+smallerMsg what inst_head
   = vcat [ hang (text "The" <+> what)
-              2 (text "is no smaller than the instance head")
+              2 (sep [ text "is no smaller than"
+                     , text "the instance head" <+> quotes inst_head ])
          , parens undecidableMsg ]
 
-noMoreMsg :: [TcTyVar] -> SDoc -> SDoc
-noMoreMsg tvs what
+noMoreMsg :: [TcTyVar] -> SDoc -> SDoc -> SDoc
+noMoreMsg tvs what inst_head
   = vcat [ hang (text "Variable" <> plural tvs <+> quotes (pprWithCommas ppr tvs)
                 <+> occurs <+> text "more often")
               2 (sep [ text "in the" <+> what
-                     , text "than in the instance head" ])
+                     , text "than in the instance head" <+> quotes inst_head ])
          , parens undecidableMsg ]
   where
    occurs = if isSingleton tvs then text "occurs"
@@ -1799,12 +1802,13 @@ checkFamInstRhs tc lhsTys famInsts
    fvs      = fvTypes lhsTys
    check (tc, tys)
       | not (all isTyFamFree tys) = Just (nestedMsg what)
-      | not (null bad_tvs)        = Just (noMoreMsg bad_tvs what)
-      | lhs_size <= fam_app_size  = Just (smallerMsg what)
+      | not (null bad_tvs)        = Just (noMoreMsg bad_tvs what inst_head)
+      | lhs_size <= fam_app_size  = Just (smallerMsg what inst_head)
       | otherwise                 = Nothing
       where
         what         = text "type family application"
                        <+> quotes (pprType (TyConApp tc tys))
+        inst_head    = pprType (TyConApp tc lhsTys)
         bad_tvs      = fvTypes tys \\ fvs
         fam_app_size = sizeTyConAppArgs tc tys
 
index 5e19173..c0ceabf 100644 (file)
@@ -1,6 +1,6 @@
 
 T8165_fail2.hs:9:12: error:
     • The type family application ‘T Loop’
-        is no smaller than the instance head
+        is no smaller than the instance head ‘T Loop’
       (Use UndecidableInstances to permit this)
     • In the instance declaration for ‘C Loop’
index 8664c7b..500be78 100644 (file)
@@ -6,12 +6,12 @@ NotRelaxedExamples.hs:9:15: error:
 
 NotRelaxedExamples.hs:10:15: error:
     • The type family application ‘F2 [x]’
-        is no smaller than the instance head
+        is no smaller than the instance head ‘F2 [x]’
       (Use UndecidableInstances to permit this)
     • In the type instance declaration for ‘F2’
 
 NotRelaxedExamples.hs:11:15: error:
     • The type family application ‘F3 [Char]’
-        is no smaller than the instance head
+        is no smaller than the instance head ‘F3 Bool’
       (Use UndecidableInstances to permit this)
     • In the type instance declaration for ‘F3’
index 32c0e7f..715febd 100644 (file)
@@ -1,6 +1,6 @@
 
 T10817.hs:9:3: error:
     The type family application ‘F a’
-      is no smaller than the instance head
+      is no smaller than the instance head ‘F a’
     (Use UndecidableInstances to permit this)
     In the class declaration for ‘C’
index 04dd2d3..4ac7e25 100644 (file)
@@ -1,13 +1,14 @@
 
 TyFamUndec.hs:6:15: error:
     • Variable ‘b’ occurs more often
-        in the type family application ‘T (b, b)’ than in the instance head
+        in the type family application ‘T (b, b)’
+        than in the instance head ‘T (a, [b])’
       (Use UndecidableInstances to permit this)
     • In the type instance declaration for ‘T’
 
 TyFamUndec.hs:7:15: error:
     • The type family application ‘T (a, Maybe b)’
-        is no smaller than the instance head
+        is no smaller than the instance head ‘T (a, Maybe b)’
       (Use UndecidableInstances to permit this)
     • In the type instance declaration for ‘T’
 
diff --git a/testsuite/tests/quantified-constraints/T15231.hs b/testsuite/tests/quantified-constraints/T15231.hs
new file mode 100644 (file)
index 0000000..7b7834d
--- /dev/null
@@ -0,0 +1,15 @@
+{-# LANGUAGE ConstraintKinds #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE KindSignatures #-}
+{-# LANGUAGE QuantifiedConstraints #-}
+module Bug where
+
+import Data.Kind
+
+data ECC :: Constraint -> Type -> Type
+
+class Y a
+class Z a
+
+instance  c         => Y (ECC c a)
+instance (c => Z a) => Z (ECC c a)
diff --git a/testsuite/tests/quantified-constraints/T15231.stderr b/testsuite/tests/quantified-constraints/T15231.stderr
new file mode 100644 (file)
index 0000000..afb7ac3
--- /dev/null
@@ -0,0 +1,7 @@
+
+T15231.hs:15:10: error:
+    • Variable ‘c’ occurs more often
+        in the constraint ‘c’ than in the instance head ‘Z a’
+      (Use UndecidableInstances to permit this)
+    • In the quantified constraint ‘c => Z a’
+      In the instance declaration for ‘Z (ECC c a)’
index e546a7c..75fcf8c 100644 (file)
@@ -9,3 +9,4 @@ test('T14863', normal, compile, [''])
 test('T14961', normal, compile, [''])
 test('T9123a', normal, compile, [''])
 test('T15244', normal, compile, [''])
+test('T15231', normal, compile_fail, [''])
index f0f11f5..31fd91b 100644 (file)
@@ -1,12 +1,12 @@
 
 fd-loop.hs:12:10: error:
     • Variable ‘b’ occurs more often
-        in the constraint ‘C a b’ than in the instance head
+        in the constraint ‘C a b’ than in the instance head ‘Eq (T a)’
       (Use UndecidableInstances to permit this)
     • In the instance declaration for ‘Eq (T a)’
 
 fd-loop.hs:12:10: error:
     • Variable ‘b’ occurs more often
-        in the constraint ‘Eq b’ than in the instance head
+        in the constraint ‘Eq b’ than in the instance head ‘Eq (T a)’
       (Use UndecidableInstances to permit this)
     • In the instance declaration for ‘Eq (T a)’
index ce07df6..4096ad3 100644 (file)
@@ -1,6 +1,7 @@
 
 tcfail108.hs:7:10: error:
     • Variable ‘f’ occurs more often
-        in the constraint ‘Eq (f (Rec f))’ than in the instance head
+        in the constraint ‘Eq (f (Rec f))’
+        than in the instance head ‘Eq (Rec f)’
       (Use UndecidableInstances to permit this)
     • In the instance declaration for ‘Eq (Rec f)’
index 0b42e0d..3e61320 100644 (file)
@@ -1,6 +1,6 @@
 
 tcfail154.hs:12:10: error:
     • Variable ‘a’ occurs more often
-        in the constraint ‘C a a’ than in the instance head
+        in the constraint ‘C a a’ than in the instance head ‘Eq (T a)’
       (Use UndecidableInstances to permit this)
     • In the instance declaration for ‘Eq (T a)’
index edc0506..e81778c 100644 (file)
@@ -1,12 +1,14 @@
 
 tcfail157.hs:27:10: error:
     • Variable ‘b’ occurs more often
-        in the constraint ‘E m a b’ than in the instance head
+        in the constraint ‘E m a b’
+        than in the instance head ‘Foo m (a -> ())’
       (Use UndecidableInstances to permit this)
     • In the instance declaration for ‘Foo m (a -> ())’
 
 tcfail157.hs:27:10: error:
     • Variable ‘b’ occurs more often
-        in the constraint ‘Foo m b’ than in the instance head
+        in the constraint ‘Foo m b’
+        than in the instance head ‘Foo m (a -> ())’
       (Use UndecidableInstances to permit this)
     • In the instance declaration for ‘Foo m (a -> ())’