Commit 0c7d2d75 authored by eir@cis.upenn.edu's avatar eir@cis.upenn.edu Committed by Krzysztof Gogolewski
Browse files

Fix Trac #8368.

Two different fixes were necessary here. First, we need to fail eagerly
in kcConDecl, to prevent the return-type error in tcConDecl from firing
twice. (This wasn't caught earlier because of the eager fail in the
datatype kind-checking code -- which isn't used for data instances!)
We also must check again in tcDataFamInstDecl, because it's possible for
a data instance return type to have the right head but the wrong body
(i.e., doesn't conform to the data instance type patterns). This check
is only possible *after* desugaring from HsType to Type, so it can't be
done in tcConRes with the first check.

This is documented in a comment at check_valid_data_con, a local
function within tcDataFamInstDecl.
parent 9d908c52
......@@ -37,6 +37,7 @@ import TcDeriv
import TcEnv
import TcHsType
import TcUnify
import Unify ( tcMatchTy )
import TcTyDecls ( emptyRoleAnnots )
import MkCore ( nO_METHOD_BINDING_ERROR_ID )
import Type
......@@ -710,8 +711,8 @@ tcDataFamInstDecl mb_clsinfo
; return (rep_tc, fam_inst) }
-- Remember to check validity; no recursion to worry about here
; let role_annots = emptyRoleAnnots
; checkValidTyCon rep_tc role_annots
; checkNoErrs $ mapM_ (check_valid_data_con fam_tc rep_tc pats') (tyConDataCons rep_tc)
; checkValidTyCon rep_tc emptyRoleAnnots
; return fam_inst } }
where
-- See Note [Eta reduction for data family axioms]
......@@ -723,6 +724,24 @@ tcDataFamInstDecl mb_clsinfo
, not (tv `elemVarSet` tyVarsOfTypes pats)
= go tvs pats
go tvs pats = (reverse tvs, reverse pats)
-- This checks for validity of GADT-like return types. The check for normal
-- (i.e., not data instance) datatypes is done in tcConRes. But, this check
-- just checks the *head* of the return type, because that is all that is
-- necessary there. Here, we check to make sure that the whole return type
-- is an instance of the header, even when the header contains some patterns.
-- It is quite inconvenient to do this elsewhere. See also Note
-- [Checking GADT return types] in TcTyClsDecls and Trac #8368.
check_valid_data_con fam_tc rep_tc pats datacon
= setSrcSpan (srcLocSpan (getSrcLoc datacon)) $
addErrCtxt (dataConCtxt datacon) $
let tmpl_vars = mkVarSet $ tyConTyVars rep_tc
tmpl_ty = mkTyConApp fam_tc pats
res_ty = dataConOrigResTy datacon
dc_name = dataConName datacon in
checkTc (isJust (tcMatchTy tmpl_vars tmpl_ty res_ty))
(badDataConTyCon dc_name (ppr tmpl_ty) (ppr res_ty))
\end{code}
Note [Eta reduction for data family axioms]
......
......@@ -16,7 +16,7 @@ module TcTyClsDecls (
kcDataDefn, tcConDecls, dataDeclChecks, checkValidTyCon,
tcSynFamInstDecl, tcFamTyPats,
tcAddTyFamInstCtxt, tcAddDataFamInstCtxt,
wrongKindOfFamily,
wrongKindOfFamily, dataConCtxt, badDataConTyCon
) where
#include "HsVersions.h"
......@@ -900,7 +900,8 @@ kcDataDefn :: Name -> HsDataDefn Name -> TcKind -> TcM ()
kcDataDefn tc_name
(HsDataDefn { dd_ctxt = ctxt, dd_cons = cons, dd_kindSig = mb_kind }) res_k
= do { _ <- tcHsContext ctxt
; mapM_ (wrapLocM (kcConDecl tc_name)) cons
; checkNoErrs $ mapM_ (wrapLocM (kcConDecl tc_name)) cons
-- See Note [Failing early in kcDataDefn]
; kcResultKind mb_kind res_k }
------------------
......@@ -930,6 +931,18 @@ type families.
tcFamTyPats type checks the patterns, zonks, and then calls thing_inside
to generate a desugaring. It is used during type-checking (not kind-checking).
Note [Failing early in kcDataDefn]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
We need to use checkNoErrs when calling kcConDecl. This is because kcConDecl
calls tcConDecl, which checks that the return type of a GADT-like constructor
is actually an instance of the type head. Without the checkNoErrs, potentially
two bad things could happen:
1) Duplicate error messages, because tcConDecl will be called again during
*type* checking (as opposed to kind checking)
2) If we just keep blindly forging forward after both kind checking and type
checking, we can get a panic in rejigConRes. See Trac #8368.
\begin{code}
-----------------
-- Note that we can't use the family TyCon, because this is sometimes called
......@@ -1187,7 +1200,8 @@ tcConRes tc_name dc_name (ResTyGADT res_ty)
case hsTyGetAppHead_maybe res_ty of
Just (tc_name', _)
| tc_name' == tc_name -> return ()
_ -> addErrTc (badDataConTyCon dc_name tc_name res_ty)
_ -> addErrTc (badDataConTyCon dc_name (ppr tc_name)
(ppr res_ty))
; res_ty' <- tcHsLiftedType res_ty
; return (ResTyGADT res_ty') }
......@@ -1596,8 +1610,7 @@ checkValidDataCon :: DynFlags -> Bool -> TyCon -> DataCon -> TcM ()
checkValidDataCon dflags existential_ok tc con
= setSrcSpan (srcLocSpan (getSrcLoc con)) $
addErrCtxt (dataConCtxt con) $
do { traceTc "Validity of data con" (ppr con)
; traceTc "checkValidDataCon" (ppr con $$ ppr tc)
do { traceTc "checkValidDataCon" (ppr con $$ ppr tc)
-- IA0_TODO: we should also check that kind variables
-- are only instantiated with kind variables
; checkValidMonoType (dataConOrigResTy con)
......@@ -2048,11 +2061,11 @@ recClsErr cycles
= addErr (sep [ptext (sLit "Cycle in class declaration (via superclasses):"),
nest 2 (hsep (intersperse (text "->") (map ppr cycles)))])
badDataConTyCon :: Name -> Name -> LHsType Name -> SDoc
badDataConTyCon data_con tc actual_res_ty
badDataConTyCon :: Name -> SDoc -> SDoc -> SDoc
badDataConTyCon data_con tc_doc actual_res_ty_doc
= hang (ptext (sLit "Data constructor") <+> quotes (ppr data_con) <+>
ptext (sLit "returns type") <+> quotes (ppr actual_res_ty))
2 (ptext (sLit "instead of an instance of its parent type") <+> quotes (ppr tc))
ptext (sLit "returns type") <+> quotes actual_res_ty_doc)
2 (ptext (sLit "instead of an instance of its parent type") <+> quotes tc_doc)
badGadtKindCon :: DataCon -> SDoc
badGadtKindCon data_con
......
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