Commit e27b267f authored by eir@cis.upenn.edu's avatar eir@cis.upenn.edu

Perform a validity check on assoc type defaults.

This fixes #10817 and #10899. A knock-on effect is that we must
now remember locations of associated type defaults for error
messages during validity checking. This isn't too bad, but it
increases the size of the diff somewhat.

Test cases: indexed-types/should_fail/T108{17,99}
parent 2f9809ef
......@@ -1763,7 +1763,7 @@ classToIfaceDecl env clas
toIfaceAT :: ClassATItem -> IfaceAT
toIfaceAT (ATI tc def)
= IfaceAT if_decl (fmap (tidyToIfaceType env2) def)
= IfaceAT if_decl (fmap (tidyToIfaceType env2 . fst) def)
where
(env2, if_decl) = tyConToIfaceDecl env1 tc
......
......@@ -427,7 +427,7 @@ tc_iface_decl _parent ignore_prags
Just def -> forkM (mk_at_doc tc) $
extendIfaceTyVarEnv (tyConTyVars tc) $
do { tc_def <- tcIfaceType def
; return (Just tc_def) }
; return (Just (tc_def, noSrcSpan)) }
-- Must be done lazily in case the RHS of the defaults mention
-- the type constructor being defined here
-- e.g. type AT a; type AT b = AT [b] Trac #8002
......
......@@ -572,7 +572,7 @@ tcATDefault loc inst_subst defined_ats (ATI fam_tc defs)
-- Example: class C a where { type F a b :: *; type F a b = () }
-- instance C [x]
-- Then we want to generate the decl: type F [x] b = ()
| Just rhs_ty <- defs
| Just (rhs_ty, _loc) <- defs
= do { let (subst', pat_tys') = mapAccumL subst_tv inst_subst
(tyConTyVars fam_tc)
rhs' = substTy subst' rhs_ty
......@@ -580,6 +580,11 @@ tcATDefault loc inst_subst defined_ats (ATI fam_tc defs)
tvs' = varSetElemsKvsFirst tv_set'
; rep_tc_name <- newFamInstTyConName (L loc (tyConName fam_tc)) pat_tys'
; let axiom = mkSingleCoAxiom Nominal rep_tc_name tvs' fam_tc pat_tys' rhs'
-- NB: no validity check. We check validity of default instances
-- in the class definition. Because type instance arguments cannot
-- be type family applications and cannot be polytypes, the
-- validity check is redundant.
; traceTc "mk_deflt_at_instance" (vcat [ ppr fam_tc, ppr rhs_ty
, pprCoAxiom axiom ])
; fam_inst <- ASSERT( tyVarsOfType rhs' `subVarSet` tv_set' )
......
......@@ -939,8 +939,8 @@ checkBootTyCon tc1 tc2
(text "The associated type defaults differ")
-- Ignore the location of the defaults
eqATDef Nothing Nothing = True
eqATDef (Just ty1) (Just ty2) = eqTypeX env ty1 ty2
eqATDef Nothing Nothing = True
eqATDef (Just (ty1, _loc1)) (Just (ty2, _loc2)) = eqTypeX env ty1 ty2
eqATDef _ _ = False
eqFD (as1,bs1) (as2,bs2) =
......
......@@ -914,9 +914,9 @@ tcClassATs class_name parent ats at_defs
; return (ATI fam_tc atd) }
-------------------------
tcDefaultAssocDecl :: TyCon -- ^ Family TyCon
-> [LTyFamDefltEqn Name] -- ^ Defaults
-> TcM (Maybe Type) -- ^ Type checked RHS
tcDefaultAssocDecl :: TyCon -- ^ Family TyCon
-> [LTyFamDefltEqn Name] -- ^ Defaults
-> TcM (Maybe (Type, SrcSpan)) -- ^ Type checked RHS
tcDefaultAssocDecl _ []
= return Nothing -- No default declaration
......@@ -941,7 +941,7 @@ tcDefaultAssocDecl fam_tc [L loc (TyFamEqn { tfe_tycon = L _ tc_name
; let fam_tc_tvs = tyConTyVars fam_tc
subst = zipTopTvSubst tvs (mkTyVarTys fam_tc_tvs)
; return ( ASSERT( equalLength fam_tc_tvs tvs )
Just (substTy subst rhs_ty) ) }
Just (substTy subst rhs_ty, loc) ) }
-- We check for well-formedness and validity later, in checkValidClass
-------------------------
......@@ -1821,13 +1821,19 @@ checkValidClass cls
= when (tyVarsOfType pred `subVarSet` cls_tv_set)
(addErrTc (badMethPred sel_id pred))
check_at (ATI fam_tc _)
| cls_arity > 0 -- Check that the associated type mentions at least
check_at (ATI fam_tc m_dflt_rhs)
= do { checkTc (cls_arity == 0 || any (`elemVarSet` cls_tv_set) fam_tvs)
(noClassTyVarErr cls fam_tc)
-- Check that the associated type mentions at least
-- one of the class type variables
= checkTc (any (`elemVarSet` cls_tv_set) (tyConTyVars fam_tc))
(noClassTyVarErr cls fam_tc)
| otherwise -- The check is disabled for nullary type classes,
= return () -- since there is no possible ambiguity (Trac #10020)
-- The check is disabled for nullary type classes,
-- since there is no possible ambiguity (Trac #10020)
; whenIsJust m_dflt_rhs $ \ (rhs, loc) ->
checkValidTyFamEqn (Just (cls, mini_env)) fam_tc
fam_tvs (mkTyVarTys fam_tvs) rhs loc }
where
fam_tvs = tyConTyVars fam_tc
mini_env = zipVarEnv tyvars (mkTyVarTys tyvars)
checkFamFlag :: Name -> TcM ()
-- Check that we don't use families without -XTypeFamilies
......
......@@ -12,6 +12,7 @@ module TcValidity (
checkValidInstance, validDerivPred,
checkInstTermination,
ClsInfo, checkValidCoAxiom, checkValidCoAxBranch,
checkValidTyFamEqn,
checkConsistentFamInst,
arityErr, badATErr
) where
......@@ -1276,6 +1277,19 @@ checkValidCoAxBranch :: Maybe ClsInfo
checkValidCoAxBranch mb_clsinfo fam_tc
(CoAxBranch { cab_tvs = tvs, cab_lhs = typats
, cab_rhs = rhs, cab_loc = loc })
= checkValidTyFamEqn mb_clsinfo fam_tc tvs typats rhs loc
-- | Do validity checks on a type family equation, including consistency
-- with any enclosing class instance head, termination, and lack of
-- polytypes.
checkValidTyFamEqn :: Maybe ClsInfo
-> TyCon -- ^ of the type family
-> [TyVar] -- ^ bound tyvars in the equation
-> [Type] -- ^ type patterns
-> Type -- ^ rhs
-> SrcSpan
-> TcM ()
checkValidTyFamEqn mb_clsinfo fam_tc tvs typats rhs loc
= setSrcSpan loc $
do { checkValidFamPats fam_tc tvs typats
......@@ -1329,7 +1343,8 @@ checkValidFamPats :: TyCon -> [TyVar] -> [Type] -> TcM ()
-- type instance F (T a) = a
-- c) Have the right number of patterns
checkValidFamPats fam_tc tvs ty_pats
= ASSERT( length ty_pats == tyConArity fam_tc )
= ASSERT2( length ty_pats == tyConArity fam_tc
, ppr ty_pats $$ ppr fam_tc $$ ppr (tyConArity fam_tc) )
-- A family instance must have exactly the same number of type
-- parameters as the family declaration. You can't write
-- type family F a :: * -> *
......
......@@ -29,6 +29,7 @@ import Name
import BasicTypes
import Unique
import Util
import SrcLoc
import Outputable
import FastString
import BooleanFormula (BooleanFormula)
......@@ -100,7 +101,8 @@ data DefMeth = NoDefMeth -- No default method
data ClassATItem
= ATI TyCon -- See Note [Associated type tyvar names]
(Maybe Type) -- Default associated type (if any) from this template
(Maybe (Type, SrcSpan))
-- Default associated type (if any) from this template
-- Note [Associated type defaults]
type ClassMinimalDef = BooleanFormula Name -- Required methods
......@@ -147,6 +149,8 @@ Note that
the default Type rhs
The @mkClass@ function fills in the indirect superclasses.
The SrcSpan is for the entire original declaration.
-}
mkClass :: [TyVar]
......
{-# LANGUAGE TypeFamilies #-}
module T10817 where
import Data.Proxy
class C a where
type F a
type F a = F a
instance C Bool
x :: Proxy (F Bool)
x = Proxy
T10817.hs:9:3: error:
The type family application ‘F a’
is no smaller than the instance head
(Use UndecidableInstances to permit this)
In the class declaration for ‘C’
{-# LANGUAGE TypeFamilies, RankNTypes #-}
module T10899 where
class C a where
type F a
type F a = forall m. m a
T10899.hs:7:3: error:
Illegal polymorphic or qualified type: forall (m :: * -> *). m a
In the class declaration for ‘C’
......@@ -136,3 +136,5 @@ test('T7788', normal, compile_fail, [''])
test('T8550', normal, compile_fail, [''])
test('T9554', normal, compile_fail, [''])
test('T10141', normal, compile_fail, [''])
test('T10817', normal, compile_fail, [''])
test('T10899', normal, compile_fail, [''])
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE UndecidableInstances #-}
-- this is needed because |FamHelper a x| /< |Fam a x|
module ShouldCompile where
class Cls a where
......
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