Commit 91822e4e authored by Tao He's avatar Tao He Committed by Ben Gamari
Browse files

Add "quantified constraint" context in error message, fix #15231.

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
parent b67b9717
......@@ -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
......
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’
......@@ -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’
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’
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’
......
{-# 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)
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)’
......@@ -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, [''])
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)’
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)’
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)’
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 -> ())’
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment