Commit e3c374cc authored by Simon Peyton Jones's avatar Simon Peyton Jones Committed by Marge Bot

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.
parent 8b95ddd3
......@@ -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):" $
......
......@@ -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
-}
......
......@@ -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') }
......
......@@ -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 ()
......
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’
{-# LANGUAGE PolyKinds #-}
module T17841 where
data Proxy a = Proxy
class Foo (t :: k) where foo :: Proxy (a :: t)
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’
......@@ -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, [''])
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