summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorSimon Peyton Jones <simonpj@microsoft.com>2020-03-11 15:23:52 +0000
committerMarge Bot <ben+marge-bot@smart-cactus.org>2020-03-14 05:31:07 -0400
commite3c374cc5bd7eb49649b9f507f9f7740697e3f70 (patch)
tree1eb150d64ca6c2d425617851222367cda7c59342
parent8b95ddd3f20a67acf5251347d80f9cab191bdfc4 (diff)
downloadhaskell-e3c374cc5bd7eb49649b9f507f9f7740697e3f70.tar.gz
Wrap an implication around class-sig kind errors
Ticket #17841 showed that we can get a kind error in a class signature, but lack an enclosing implication that binds its skolems. This patch * Adds the wrapping implication: the new call to checkTvConstraints in tcClassDecl1 * Simplifies the API to checkTvConstraints, which was not otherwise called at all. * Simplifies TcErrors.report_unsolved by *not* initialising the TidyEnv from the typechecker lexical envt. It's enough to do so from the free vars of the unsolved constraints; and we get silly renamings if we add variables twice: once from the lexical scope and once from the implication constraint.
-rw-r--r--compiler/typecheck/TcErrors.hs3
-rw-r--r--compiler/typecheck/TcEvidence.hs3
-rw-r--r--compiler/typecheck/TcTyClsDecls.hs6
-rw-r--r--compiler/typecheck/TcUnify.hs20
-rw-r--r--testsuite/tests/polykinds/T16902.stderr2
-rw-r--r--testsuite/tests/polykinds/T17841.hs7
-rw-r--r--testsuite/tests/polykinds/T17841.stderr13
-rw-r--r--testsuite/tests/polykinds/all.T1
8 files changed, 37 insertions, 18 deletions
diff --git a/compiler/typecheck/TcErrors.hs b/compiler/typecheck/TcErrors.hs
index e111afc08a..2d0104f434 100644
--- a/compiler/typecheck/TcErrors.hs
+++ b/compiler/typecheck/TcErrors.hs
@@ -210,10 +210,9 @@ report_unsolved type_errors expr_holes
; traceTc "reportUnsolved (before zonking and tidying)" (ppr wanted)
; wanted <- zonkWC wanted -- Zonk to reveal all information
- ; env0 <- tcInitTidyEnv
-- If we are deferring we are going to need /all/ evidence around,
-- including the evidence produced by unflattening (zonkWC)
- ; let tidy_env = tidyFreeTyCoVars env0 free_tvs
+ ; let tidy_env = tidyFreeTyCoVars emptyTidyEnv free_tvs
free_tvs = tyCoVarsOfWCList wanted
; traceTc "reportUnsolved (after zonking):" $
diff --git a/compiler/typecheck/TcEvidence.hs b/compiler/typecheck/TcEvidence.hs
index 89bf4149b7..e350ebeac6 100644
--- a/compiler/typecheck/TcEvidence.hs
+++ b/compiler/typecheck/TcEvidence.hs
@@ -442,8 +442,7 @@ use CoEvBindsVar (see newCoTcEvBinds) to signal that no term-level
evidence bindings are allowed. Notebly ():
- Places in types where we are solving kind constraints (all of which
- are equalities); see solveEqualities, solveLocalEqualities,
- checkTvConstraints
+ are equalities); see solveEqualities, solveLocalEqualities
- When unifying forall-types
-}
diff --git a/compiler/typecheck/TcTyClsDecls.hs b/compiler/typecheck/TcTyClsDecls.hs
index 7f4b7c6b6e..8d8f254a3e 100644
--- a/compiler/typecheck/TcTyClsDecls.hs
+++ b/compiler/typecheck/TcTyClsDecls.hs
@@ -39,7 +39,7 @@ import TcTyDecls
import TcClassDcl
import {-# SOURCE #-} TcInstDcls( tcInstDecls1 )
import TcDeriv (DerivInfo(..))
-import TcUnify ( unifyKind )
+import TcUnify ( unifyKind, checkTvConstraints )
import TcHsType
import ClsInst( AssocInstInfo(..) )
import TcMType
@@ -2026,6 +2026,9 @@ tcClassDecl1 roles_info class_name hs_ctxt meths fundeps sigs ats at_defs
; (ctxt, fds, sig_stuff, at_stuff)
<- pushTcLevelM_ $
solveEqualities $
+ checkTvConstraints skol_info (binderVars binders) $
+ -- The checkTvConstraints is needed bring into scope the
+ -- skolems bound by the class decl header (#17841)
do { ctxt <- tcHsContext hs_ctxt
; fds <- mapM (addLocM tc_fundep) fundeps
; sig_stuff <- tcClassSigs class_name sigs meths
@@ -2058,6 +2061,7 @@ tcClassDecl1 roles_info class_name hs_ctxt meths fundeps sigs ats at_defs
ppr fds)
; return clas }
where
+ skol_info = TyConSkol ClassFlavour class_name
tc_fundep (tvs1, tvs2) = do { tvs1' <- mapM (tcLookupTyVar . unLoc) tvs1 ;
; tvs2' <- mapM (tcLookupTyVar . unLoc) tvs2 ;
; return (tvs1', tvs2') }
diff --git a/compiler/typecheck/TcUnify.hs b/compiler/typecheck/TcUnify.hs
index 0832f80de4..4c1b18d89c 100644
--- a/compiler/typecheck/TcUnify.hs
+++ b/compiler/typecheck/TcUnify.hs
@@ -1195,18 +1195,14 @@ checkConstraints skol_info skol_tvs given thing_inside
; return (emptyTcEvBinds, res) } }
checkTvConstraints :: SkolemInfo
- -> Maybe SDoc -- User-written telescope, if present
- -> TcM ([TcTyVar], result)
- -> TcM ([TcTyVar], result)
-
-checkTvConstraints skol_info m_telescope thing_inside
- = do { (tclvl, wanted, (skol_tvs, result))
- <- pushLevelAndCaptureConstraints thing_inside
-
- ; emitResidualTvConstraint skol_info m_telescope
- skol_tvs tclvl wanted
-
- ; return (skol_tvs, result) }
+ -> [TcTyVar] -- Skolem tyvars
+ -> TcM result
+ -> TcM result
+
+checkTvConstraints skol_info skol_tvs thing_inside
+ = do { (tclvl, wanted, result) <- pushLevelAndCaptureConstraints thing_inside
+ ; emitResidualTvConstraint skol_info Nothing skol_tvs tclvl wanted
+ ; return result }
emitResidualTvConstraint :: SkolemInfo -> Maybe SDoc -> [TcTyVar]
-> TcLevel -> WantedConstraints -> TcM ()
diff --git a/testsuite/tests/polykinds/T16902.stderr b/testsuite/tests/polykinds/T16902.stderr
index e265866119..2da3e41c36 100644
--- a/testsuite/tests/polykinds/T16902.stderr
+++ b/testsuite/tests/polykinds/T16902.stderr
@@ -1,6 +1,6 @@
T16902.hs:11:10: error:
- • Expected a type, but found something with kind ‘a1’
+ • Expected a type, but found something with kind ‘a’
• In the type ‘F a’
In the definition of data constructor ‘MkF’
In the data declaration for ‘F’
diff --git a/testsuite/tests/polykinds/T17841.hs b/testsuite/tests/polykinds/T17841.hs
new file mode 100644
index 0000000000..c728a11f02
--- /dev/null
+++ b/testsuite/tests/polykinds/T17841.hs
@@ -0,0 +1,7 @@
+{-# LANGUAGE PolyKinds #-}
+
+module T17841 where
+
+data Proxy a = Proxy
+
+class Foo (t :: k) where foo :: Proxy (a :: t)
diff --git a/testsuite/tests/polykinds/T17841.stderr b/testsuite/tests/polykinds/T17841.stderr
new file mode 100644
index 0000000000..975f5a11d0
--- /dev/null
+++ b/testsuite/tests/polykinds/T17841.stderr
@@ -0,0 +1,13 @@
+
+T17841.hs:7:40: error:
+ • Couldn't match kind ‘k’ with ‘*’
+ ‘k’ is a rigid type variable bound by
+ the class declaration for ‘Foo’
+ at T17841.hs:7:17
+ When matching kinds
+ k0 :: *
+ t :: k
+ Expected kind ‘t’, but ‘a’ has kind ‘k0’
+ • In the first argument of ‘Proxy’, namely ‘(a :: t)’
+ In the type signature: foo :: Proxy (a :: t)
+ In the class declaration for ‘Foo’
diff --git a/testsuite/tests/polykinds/all.T b/testsuite/tests/polykinds/all.T
index 4312691755..454be6fc62 100644
--- a/testsuite/tests/polykinds/all.T
+++ b/testsuite/tests/polykinds/all.T
@@ -215,3 +215,4 @@ test('T16342', normal, compile, [''])
test('T16263', normal, compile_fail, [''])
test('T16902', normal, compile_fail, [''])
test('CuskFam', normal, compile, [''])
+test('T17841', normal, compile_fail, [''])