diff options
author | Richard Eisenberg <eir@cis.upenn.edu> | 2013-06-21 13:54:49 +0100 |
---|---|---|
committer | Richard Eisenberg <eir@cis.upenn.edu> | 2013-06-21 13:54:49 +0100 |
commit | 569b26526403df4d88fe2a6d64c7dade09d003ad (patch) | |
tree | f216a5ceaf5d655248564abefab6765aaa9da37d | |
parent | 11db9cf82e014de43d8ab04947ef2a2b7fa30f37 (diff) | |
download | haskell-569b26526403df4d88fe2a6d64c7dade09d003ad.tar.gz |
Revise implementation of overlapping type family instances.
This commit changes the syntax and story around overlapping type
family instances. Before, we had "unbranched" instances and
"branched" instances. Now, we have closed type families and
open ones.
The behavior of open families is completely unchanged. In particular,
coincident overlap of open type family instances still works, despite
emails to the contrary.
A closed type family is declared like this:
> type family F a where
> F Int = Bool
> F a = Char
The equations are tried in order, from top to bottom, subject to
certain constraints, as described in the user manual. It is not
allowed to declare an instance of a closed family.
58 files changed, 1428 insertions, 1165 deletions
diff --git a/compiler/coreSyn/CoreLint.lhs b/compiler/coreSyn/CoreLint.lhs index b00b452502..f9256e18ad 100644 --- a/compiler/coreSyn/CoreLint.lhs +++ b/compiler/coreSyn/CoreLint.lhs @@ -939,7 +939,7 @@ lintCoercion co@(AxiomInstCo con ind cos) ; let lhs' = Type.substTys subst_l lhs rhs' = Type.substTy subst_r rhs ; case checkAxInstCo co of - Just bad_index -> bad_ax $ ptext (sLit "inconsistent with") <+> (ppr bad_index) + Just bad_branch -> bad_ax $ ptext (sLit "inconsistent with") <+> (pprCoAxBranch (coAxiomTyCon con) bad_branch) Nothing -> return () ; return (typeKind rhs', mkTyConApp (coAxiomTyCon con) lhs', rhs') } where diff --git a/compiler/deSugar/DsMeta.hs b/compiler/deSugar/DsMeta.hs index 8232d91037..a60f18ded5 100644 --- a/compiler/deSugar/DsMeta.hs +++ b/compiler/deSugar/DsMeta.hs @@ -258,18 +258,29 @@ repSynDecl tc bndrs ty ; repTySyn tc bndrs ty1 } repFamilyDecl :: LFamilyDecl Name -> DsM (SrcSpan, Core TH.DecQ) -repFamilyDecl (L loc (FamilyDecl { fdFlavour = flavour, +repFamilyDecl (L loc (FamilyDecl { fdInfo = info, fdLName = tc, fdTyVars = tvs, fdKindSig = opt_kind })) = do { tc1 <- lookupLOcc tc -- See note [Binders and occurrences] ; dec <- addTyClTyVarBinds tvs $ \bndrs -> - do { flav <- repFamilyFlavour flavour - ; case opt_kind of - Nothing -> repFamilyNoKind flav tc1 bndrs - Just ki -> do { ki1 <- repLKind ki - ; repFamilyKind flav tc1 bndrs ki1 } - } + case (opt_kind, info) of + (Nothing, ClosedTypeFamily eqns) -> + do { eqns1 <- mapM repTyFamEqn eqns + ; eqns2 <- coreList tySynEqnQTyConName eqns1 + ; repClosedFamilyNoKind tc1 bndrs eqns2 } + (Just ki, ClosedTypeFamily eqns) -> + do { eqns1 <- mapM repTyFamEqn eqns + ; eqns2 <- coreList tySynEqnQTyConName eqns1 + ; ki1 <- repLKind ki + ; repClosedFamilyKind tc1 bndrs ki1 eqns2 } + (Nothing, _) -> + do { info' <- repFamilyInfo info + ; repFamilyNoKind info' tc1 bndrs } + (Just ki, _) -> + do { info' <- repFamilyInfo info + ; ki1 <- repLKind ki + ; repFamilyKind info' tc1 bndrs ki1 } ; return (loc, dec) } @@ -317,9 +328,10 @@ repLFunDep (L _ (xs, ys)) = do xs' <- repList nameTyConName lookupBinder xs -- represent family declaration flavours -- -repFamilyFlavour :: FamilyFlavour -> DsM (Core TH.FamFlavour) -repFamilyFlavour TypeFamily = rep2 typeFamName [] -repFamilyFlavour DataFamily = rep2 dataFamName [] +repFamilyInfo :: FamilyInfo Name -> DsM (Core TH.FamFlavour) +repFamilyInfo OpenTypeFamily = rep2 typeFamName [] +repFamilyInfo DataFamily = rep2 dataFamName [] +repFamilyInfo ClosedTypeFamily {} = panic "repFamilyInfo" -- Represent instance declarations -- @@ -362,12 +374,11 @@ repClsInstD (ClsInstDecl { cid_poly_ty = ty, cid_binds = binds Just (tvs, cxt, cls, tys) = splitLHsInstDeclTy_maybe ty repTyFamInstD :: TyFamInstDecl Name -> DsM (Core TH.DecQ) -repTyFamInstD decl@(TyFamInstDecl { tfid_eqns = eqns }) +repTyFamInstD decl@(TyFamInstDecl { tfid_eqn = eqn }) = do { let tc_name = tyFamInstDeclLName decl - ; tc <- lookupLOcc tc_name -- See note [Binders and occurrences] - ; eqns1 <- mapM repTyFamEqn eqns - ; eqns2 <- coreList tySynEqnQTyConName eqns1 - ; repTySynInst tc eqns2 } + ; tc <- lookupLOcc tc_name -- See note [Binders and occurrences] + ; eqn1 <- repTyFamEqn eqn + ; repTySynInst tc eqn1 } repTyFamEqn :: LTyFamInstEqn Name -> DsM (Core TH.TySynEqnQ) repTyFamEqn (L loc (TyFamInstEqn { tfie_pats = HsWB { hswb_cts = tys @@ -1688,9 +1699,24 @@ repFamilyKind :: Core TH.FamFlavour -> Core TH.Name -> Core [TH.TyVarBndr] repFamilyKind (MkC flav) (MkC nm) (MkC tvs) (MkC ki) = rep2 familyKindDName [flav, nm, tvs, ki] -repTySynInst :: Core TH.Name -> Core [TH.TySynEqnQ] -> DsM (Core TH.DecQ) -repTySynInst (MkC nm) (MkC eqns) - = rep2 tySynInstDName [nm, eqns] +repTySynInst :: Core TH.Name -> Core TH.TySynEqnQ -> DsM (Core TH.DecQ) +repTySynInst (MkC nm) (MkC eqn) + = rep2 tySynInstDName [nm, eqn] + +repClosedFamilyNoKind :: Core TH.Name + -> Core [TH.TyVarBndr] + -> Core [TH.TySynEqnQ] + -> DsM (Core TH.DecQ) +repClosedFamilyNoKind (MkC nm) (MkC tvs) (MkC eqns) + = rep2 closedTypeFamilyNoKindDName [nm, tvs, eqns] + +repClosedFamilyKind :: Core TH.Name + -> Core [TH.TyVarBndr] + -> Core TH.Kind + -> Core [TH.TySynEqnQ] + -> DsM (Core TH.DecQ) +repClosedFamilyKind (MkC nm) (MkC tvs) (MkC ki) (MkC eqns) + = rep2 closedTypeFamilyKindDName [nm, tvs, ki, eqns] repTySynEqn :: Core [TH.TypeQ] -> Core TH.TypeQ -> DsM (Core TH.TySynEqnQ) repTySynEqn (MkC lhs) (MkC rhs) @@ -1994,7 +2020,8 @@ templateHaskellNames = [ pragInlDName, pragSpecDName, pragSpecInlDName, pragSpecInstDName, pragRuleDName, familyNoKindDName, familyKindDName, dataInstDName, newtypeInstDName, - tySynInstDName, infixLDName, infixRDName, infixNDName, + tySynInstDName, closedTypeFamilyKindDName, closedTypeFamilyNoKindDName, + infixLDName, infixRDName, infixNDName, -- Cxt cxtName, -- Pred @@ -2207,6 +2234,7 @@ funDName, valDName, dataDName, newtypeDName, tySynDName, classDName, instanceDName, sigDName, forImpDName, pragInlDName, pragSpecDName, pragSpecInlDName, pragSpecInstDName, pragRuleDName, familyNoKindDName, familyKindDName, dataInstDName, newtypeInstDName, tySynInstDName, + closedTypeFamilyKindDName, closedTypeFamilyNoKindDName, infixLDName, infixRDName, infixNDName :: Name funDName = libFun (fsLit "funD") funDIdKey valDName = libFun (fsLit "valD") valDIdKey @@ -2227,6 +2255,10 @@ familyKindDName = libFun (fsLit "familyKindD") familyKindDIdKey dataInstDName = libFun (fsLit "dataInstD") dataInstDIdKey newtypeInstDName = libFun (fsLit "newtypeInstD") newtypeInstDIdKey tySynInstDName = libFun (fsLit "tySynInstD") tySynInstDIdKey +closedTypeFamilyKindDName + = libFun (fsLit "closedTypeFamilyKindD") closedTypeFamilyKindDIdKey +closedTypeFamilyNoKindDName + = libFun (fsLit "closedTypeFamilyNoKindD") closedTypeFamilyNoKindDIdKey infixLDName = libFun (fsLit "infixLD") infixLDIdKey infixRDName = libFun (fsLit "infixRD") infixRDIdKey infixNDName = libFun (fsLit "infixND") infixNDIdKey @@ -2543,29 +2575,32 @@ funDIdKey, valDIdKey, dataDIdKey, newtypeDIdKey, tySynDIdKey, pragSpecDIdKey, pragSpecInlDIdKey, pragSpecInstDIdKey, pragRuleDIdKey, familyNoKindDIdKey, familyKindDIdKey, dataInstDIdKey, newtypeInstDIdKey, tySynInstDIdKey, + closedTypeFamilyKindDIdKey, closedTypeFamilyNoKindDIdKey, infixLDIdKey, infixRDIdKey, infixNDIdKey :: Unique -funDIdKey = mkPreludeMiscIdUnique 330 -valDIdKey = mkPreludeMiscIdUnique 331 -dataDIdKey = mkPreludeMiscIdUnique 332 -newtypeDIdKey = mkPreludeMiscIdUnique 333 -tySynDIdKey = mkPreludeMiscIdUnique 334 -classDIdKey = mkPreludeMiscIdUnique 335 -instanceDIdKey = mkPreludeMiscIdUnique 336 -sigDIdKey = mkPreludeMiscIdUnique 337 -forImpDIdKey = mkPreludeMiscIdUnique 338 -pragInlDIdKey = mkPreludeMiscIdUnique 339 -pragSpecDIdKey = mkPreludeMiscIdUnique 340 -pragSpecInlDIdKey = mkPreludeMiscIdUnique 341 -pragSpecInstDIdKey = mkPreludeMiscIdUnique 412 -pragRuleDIdKey = mkPreludeMiscIdUnique 413 -familyNoKindDIdKey = mkPreludeMiscIdUnique 342 -familyKindDIdKey = mkPreludeMiscIdUnique 343 -dataInstDIdKey = mkPreludeMiscIdUnique 344 -newtypeInstDIdKey = mkPreludeMiscIdUnique 345 -tySynInstDIdKey = mkPreludeMiscIdUnique 346 -infixLDIdKey = mkPreludeMiscIdUnique 347 -infixRDIdKey = mkPreludeMiscIdUnique 348 -infixNDIdKey = mkPreludeMiscIdUnique 349 +funDIdKey = mkPreludeMiscIdUnique 330 +valDIdKey = mkPreludeMiscIdUnique 331 +dataDIdKey = mkPreludeMiscIdUnique 332 +newtypeDIdKey = mkPreludeMiscIdUnique 333 +tySynDIdKey = mkPreludeMiscIdUnique 334 +classDIdKey = mkPreludeMiscIdUnique 335 +instanceDIdKey = mkPreludeMiscIdUnique 336 +sigDIdKey = mkPreludeMiscIdUnique 337 +forImpDIdKey = mkPreludeMiscIdUnique 338 +pragInlDIdKey = mkPreludeMiscIdUnique 339 +pragSpecDIdKey = mkPreludeMiscIdUnique 340 +pragSpecInlDIdKey = mkPreludeMiscIdUnique 341 +pragSpecInstDIdKey = mkPreludeMiscIdUnique 412 +pragRuleDIdKey = mkPreludeMiscIdUnique 413 +familyNoKindDIdKey = mkPreludeMiscIdUnique 342 +familyKindDIdKey = mkPreludeMiscIdUnique 343 +dataInstDIdKey = mkPreludeMiscIdUnique 344 +newtypeInstDIdKey = mkPreludeMiscIdUnique 345 +tySynInstDIdKey = mkPreludeMiscIdUnique 346 +closedTypeFamilyKindDIdKey = mkPreludeMiscIdUnique 347 +closedTypeFamilyNoKindDIdKey = mkPreludeMiscIdUnique 348 +infixLDIdKey = mkPreludeMiscIdUnique 349 +infixRDIdKey = mkPreludeMiscIdUnique 350 +infixNDIdKey = mkPreludeMiscIdUnique 351 -- type Cxt = ... cxtIdKey :: Unique diff --git a/compiler/hsSyn/Convert.lhs b/compiler/hsSyn/Convert.lhs index 8caf987336..a07fafe00d 100644 --- a/compiler/hsSyn/Convert.lhs +++ b/compiler/hsSyn/Convert.lhs @@ -215,7 +215,7 @@ cvtDec (FamilyD flav tc tvs kind) ; kind' <- cvtMaybeKind kind ; returnL $ TyClD (FamDecl (FamilyDecl (cvtFamFlavour flav) tc' tvs' kind')) } where - cvtFamFlavour TypeFam = TypeFamily + cvtFamFlavour TypeFam = OpenTypeFamily cvtFamFlavour DataFam = DataFamily cvtDec (DataInstD ctxt tc tys constrs derivs) @@ -243,13 +243,18 @@ cvtDec (NewtypeInstD ctxt tc tys constr derivs) { dfid_inst = DataFamInstDecl { dfid_tycon = tc', dfid_pats = typats' , dfid_defn = defn, dfid_fvs = placeHolderNames } }} -cvtDec (TySynInstD tc eqns) +cvtDec (TySynInstD tc eqn) = do { tc' <- tconNameL tc - ; eqns' <- mapM (cvtTySynEqn tc') eqns + ; eqn' <- cvtTySynEqn tc' eqn ; returnL $ InstD $ TyFamInstD - { tfid_inst = TyFamInstDecl { tfid_eqns = eqns' - , tfid_group = (length eqns' /= 1) + { tfid_inst = TyFamInstDecl { tfid_eqn = eqn' , tfid_fvs = placeHolderNames } } } + +cvtDec (ClosedTypeFamilyD tc tyvars mkind eqns) + = do { (_, tc', tvs') <- cvt_tycl_hdr [] tc tyvars + ; mkind' <- cvtMaybeKind mkind + ; eqns' <- mapM (cvtTySynEqn tc') eqns + ; returnL $ TyClD (FamDecl (FamilyDecl (ClosedTypeFamily eqns') tc' tvs' mkind')) } ---------------- cvtTySynEqn :: Located RdrName -> TySynEqn -> CvtM (LTyFamInstEqn RdrName) cvtTySynEqn tc (TySynEqn lhs rhs) diff --git a/compiler/hsSyn/HsDecls.lhs b/compiler/hsSyn/HsDecls.lhs index ce391c73e2..e088af7c18 100644 --- a/compiler/hsSyn/HsDecls.lhs +++ b/compiler/hsSyn/HsDecls.lhs @@ -24,7 +24,7 @@ module HsDecls ( FamilyDecl(..), LFamilyDecl, -- ** Instance declarations - InstDecl(..), LInstDecl, NewOrData(..), FamilyFlavour(..), + InstDecl(..), LInstDecl, NewOrData(..), FamilyInfo(..), TyFamInstDecl(..), LTyFamInstDecl, instDeclDataFamInsts, DataFamInstDecl(..), LDataFamInstDecl, pprDataFamInstFlavour, TyFamInstEqn(..), LTyFamInstEqn, @@ -470,16 +470,17 @@ data TyClDecl name type LFamilyDecl name = Located (FamilyDecl name) data FamilyDecl name = FamilyDecl - { fdFlavour :: FamilyFlavour -- type or data + { fdInfo :: FamilyInfo name -- type or data, closed or open , fdLName :: Located name -- type constructor , fdTyVars :: LHsTyVarBndrs name -- type variables , fdKindSig :: Maybe (LHsKind name) } -- result kind deriving( Data, Typeable ) -data FamilyFlavour - = TypeFamily - | DataFamily - deriving( Data, Typeable, Eq ) +data FamilyInfo name + = DataFamily + | OpenTypeFamily + | ClosedTypeFamily [LTyFamInstEqn name] + deriving( Data, Typeable ) \end{code} @@ -510,12 +511,15 @@ isFamilyDecl _other = False -- | type family declaration isTypeFamilyDecl :: TyClDecl name -> Bool -isTypeFamilyDecl (FamDecl d) = fdFlavour d == TypeFamily -isTypeFamilyDecl _other = False +isTypeFamilyDecl (FamDecl (FamilyDecl { fdInfo = info })) = case info of + OpenTypeFamily -> True + ClosedTypeFamily {} -> True + _ -> False +isTypeFamilyDecl _ = False -- | data family declaration isDataFamilyDecl :: TyClDecl name -> Bool -isDataFamilyDecl (FamDecl d) = fdFlavour d == DataFamily +isDataFamilyDecl (FamDecl (FamilyDecl { fdInfo = DataFamily })) = True isDataFamilyDecl _other = False \end{code} @@ -528,11 +532,9 @@ tyFamInstDeclName = unLoc . tyFamInstDeclLName tyFamInstDeclLName :: OutputableBndr name => TyFamInstDecl name -> Located name -tyFamInstDeclLName (TyFamInstDecl { tfid_eqns = - (L _ (TyFamInstEqn { tfie_tycon = ln })) : _ }) - -- there may be more than one equation, but grab the name from the first +tyFamInstDeclLName (TyFamInstDecl { tfid_eqn = + (L _ (TyFamInstEqn { tfie_tycon = ln })) }) = ln -tyFamInstDeclLName decl = pprPanic "tyFamInstDeclLName" (ppr decl) tyClDeclLName :: TyClDecl name -> Located name tyClDeclLName (FamDecl { tcdFam = FamilyDecl { fdLName = ln } }) = ln @@ -598,17 +600,26 @@ instance OutputableBndr name <+> pprFundeps (map unLoc fds) instance (OutputableBndr name) => Outputable (FamilyDecl name) where - ppr (FamilyDecl { fdFlavour = flavour, fdLName = ltycon, + ppr (FamilyDecl { fdInfo = info, fdLName = ltycon, fdTyVars = tyvars, fdKindSig = mb_kind}) - = ppr flavour <+> pp_vanilla_decl_head ltycon tyvars [] <+> pp_kind + = vcat [ pprFlavour info <+> pp_vanilla_decl_head ltycon tyvars [] <+> pp_kind <+> pp_where + , nest 2 $ pp_eqns ] where pp_kind = case mb_kind of Nothing -> empty Just kind -> dcolon <+> ppr kind + (pp_where, pp_eqns) = case info of + ClosedTypeFamily eqns -> ( ptext (sLit "where") + , vcat $ map ppr eqns ) + _ -> (empty, empty) + +pprFlavour :: FamilyInfo name -> SDoc +pprFlavour DataFamily = ptext (sLit "data family") +pprFlavour OpenTypeFamily = ptext (sLit "type family") +pprFlavour (ClosedTypeFamily {}) = ptext (sLit "type family") -instance Outputable FamilyFlavour where - ppr TypeFamily = ptext (sLit "type family") - ppr DataFamily = ptext (sLit "data family") +instance Outputable (FamilyInfo name) where + ppr = pprFlavour pp_vanilla_decl_head :: OutputableBndr name => Located name @@ -838,10 +849,9 @@ pprConDecl decl@(ConDecl { con_details = InfixCon ty1 ty2, con_res = ResTyGADT { \begin{code} ----------------- Type synonym family instances ------------- --- See note [Family instance equation groups] type LTyFamInstEqn name = Located (TyFamInstEqn name) --- | One equation in a family instance declaration +-- | One equation in a type family instance declaration data TyFamInstEqn name = TyFamInstEqn { tfie_tycon :: Located name @@ -854,15 +864,10 @@ data TyFamInstEqn name type LTyFamInstDecl name = Located (TyFamInstDecl name) data TyFamInstDecl name = TyFamInstDecl - { tfid_eqns :: [LTyFamInstEqn name] -- ^ list of (possibly-overlapping) eqns - -- Always non-empty - , tfid_group :: Bool -- Was this declared with the "where" syntax? - , tfid_fvs :: NameSet } -- The group is type-checked as one, - -- so one NameSet will do - -- INVARIANT: tfid_group == False --> length tfid_eqns == 1 + { tfid_eqn :: LTyFamInstEqn name + , tfid_fvs :: NameSet } deriving( Typeable, Data ) - ----------------- Data family instances ------------- type LDataFamInstDecl name = Located (DataFamInstDecl name) @@ -925,24 +930,13 @@ tvs are fv(pat_tys), *including* ones that are already in scope so that we can compare the type patter in the 'instance' decl and in the associated 'type' decl -Note [Family instance equation groups] -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -A TyFamInstDecl contains a list of FamInstEqn's, one for each -equation defined in the instance group. For a standalone -instance declaration, this list contains exactly one element. -It is not possible for this list to have 0 elements -- -'type instance where' without anything else is not allowed. - \begin{code} instance (OutputableBndr name) => Outputable (TyFamInstDecl name) where ppr = pprTyFamInstDecl TopLevel pprTyFamInstDecl :: OutputableBndr name => TopLevelFlag -> TyFamInstDecl name -> SDoc -pprTyFamInstDecl top_lvl (TyFamInstDecl { tfid_group = False, tfid_eqns = [eqn] }) +pprTyFamInstDecl top_lvl (TyFamInstDecl { tfid_eqn = eqn }) = ptext (sLit "type") <+> ppr_instance_keyword top_lvl <+> (ppr eqn) -pprTyFamInstDecl top_lvl (TyFamInstDecl { tfid_eqns = eqns }) - = hang (ptext (sLit "type") <+> ppr_instance_keyword top_lvl <+> ptext (sLit "where")) - 2 (vcat (map ppr eqns)) ppr_instance_keyword :: TopLevelFlag -> SDoc ppr_instance_keyword TopLevel = ptext (sLit "instance") diff --git a/compiler/iface/BinIface.hs b/compiler/iface/BinIface.hs index 9390ee4377..ba1a7e28e2 100644 --- a/compiler/iface/BinIface.hs +++ b/compiler/iface/BinIface.hs @@ -1307,27 +1307,30 @@ instance Binary IfaceDecl where return (IfaceAxiom occ a2 a3) instance Binary IfaceAxBranch where - put_ bh (IfaceAxBranch a1 a2 a3) = do + put_ bh (IfaceAxBranch a1 a2 a3 a4) = do put_ bh a1 put_ bh a2 put_ bh a3 + put_ bh a4 get bh = do a1 <- get bh a2 <- get bh a3 <- get bh - return (IfaceAxBranch a1 a2 a3) + a4 <- get bh + return (IfaceAxBranch a1 a2 a3 a4) -instance Binary ty => Binary (SynTyConRhs ty) where - put_ bh (SynFamilyTyCon a b) = putByte bh 0 >> put_ bh a >> put_ bh b - put_ bh (SynonymTyCon ty) = putByte bh 1 >> put_ bh ty +instance Binary IfaceSynTyConRhs where + put_ bh IfaceOpenSynFamilyTyCon = putByte bh 0 + put_ bh (IfaceClosedSynFamilyTyCon ax) = putByte bh 1 >> put_ bh ax + put_ bh (IfaceSynonymTyCon ty) = putByte bh 2 >> put_ bh ty get bh = do { h <- getByte bh ; case h of - 0 -> do { a <- get bh - ; b <- get bh - ; return (SynFamilyTyCon a b) } + 0 -> do { return IfaceOpenSynFamilyTyCon } + 1 -> do { ax <- get bh + ; return (IfaceClosedSynFamilyTyCon ax) } _ -> do { ty <- get bh - ; return (SynonymTyCon ty) } } + ; return (IfaceSynonymTyCon ty) } } instance Binary IfaceClsInst where put_ bh (IfaceClsInst cls tys dfun flag orph) = do @@ -1345,19 +1348,17 @@ instance Binary IfaceClsInst where return (IfaceClsInst cls tys dfun flag orph) instance Binary IfaceFamInst where - put_ bh (IfaceFamInst fam group tys name orph) = do + put_ bh (IfaceFamInst fam tys name orph) = do put_ bh fam - put_ bh group put_ bh tys put_ bh name put_ bh orph get bh = do fam <- get bh - group <- get bh tys <- get bh name <- get bh orph <- get bh - return (IfaceFamInst fam group tys name orph) + return (IfaceFamInst fam tys name orph) instance Binary OverlapFlag where put_ bh (NoOverlap b) = putByte bh 0 >> put_ bh b diff --git a/compiler/iface/BuildTyCl.lhs b/compiler/iface/BuildTyCl.lhs index d5e4a4a62e..a541e32b7b 100644 --- a/compiler/iface/BuildTyCl.lhs +++ b/compiler/iface/BuildTyCl.lhs @@ -47,7 +47,7 @@ import Outputable \begin{code} ------------------------------------------------------ buildSynTyCon :: Name -> [TyVar] - -> SynTyConRhs Type + -> SynTyConRhs -> Kind -- ^ Kind of the RHS -> TyConParent -> TcRnIf m n TyCon diff --git a/compiler/iface/IfaceEnv.lhs b/compiler/iface/IfaceEnv.lhs index 81f1b33e96..0441fdbf41 100644 --- a/compiler/iface/IfaceEnv.lhs +++ b/compiler/iface/IfaceEnv.lhs @@ -57,7 +57,7 @@ import Data.IORef ( atomicModifyIORef, readIORef ) Note [The Name Cache] ~~~~~~~~~~~~~~~~~~~~~ -The Name Cache makes sure that, during any invocation of GHC, each +The Name Cache makes sure that, during any invovcation of GHC, each External Name "M.x" has one, and only one globally-agreed Unique. * The first time we come across M.x we make up a Unique and record that diff --git a/compiler/iface/IfaceSyn.lhs b/compiler/iface/IfaceSyn.lhs index 7632b38d81..ad327d6428 100644 --- a/compiler/iface/IfaceSyn.lhs +++ b/compiler/iface/IfaceSyn.lhs @@ -14,7 +14,7 @@ module IfaceSyn ( module IfaceType, - IfaceDecl(..), IfaceClassOp(..), IfaceAT(..), + IfaceDecl(..), IfaceSynTyConRhs(..), IfaceClassOp(..), IfaceAT(..), IfaceConDecl(..), IfaceConDecls(..), IfaceExpr(..), IfaceAlt, IfaceLetBndr(..), IfaceBinding(..), IfaceConAlt(..), @@ -36,13 +36,13 @@ module IfaceSyn ( #include "HsVersions.h" -import TyCon( SynTyConRhs(..) ) import IfaceType import PprCore() -- Printing DFunArgs import Demand import Annotations import Class import NameSet +import CoAxiom ( BranchIndex ) import Name import CostCentre import Literal @@ -91,7 +91,7 @@ data IfaceDecl | IfaceSyn { ifName :: OccName, -- Type constructor ifTyVars :: [IfaceTvBndr], -- Type variables ifSynKind :: IfaceKind, -- Kind of the *rhs* (not of the tycon) - ifSynRhs :: SynTyConRhs IfaceType } + ifSynRhs :: IfaceSynTyConRhs } | IfaceClass { ifCtxt :: IfaceContext, -- Context... ifName :: OccName, -- Name of the class TyCon @@ -112,6 +112,11 @@ data IfaceDecl -- beyond .NET ifExtName :: Maybe FastString } +data IfaceSynTyConRhs + = IfaceOpenSynFamilyTyCon + | IfaceClosedSynFamilyTyCon IfExtName -- name of associated axiom + | IfaceSynonymTyCon IfaceType + data IfaceClassOp = IfaceClassOp OccName DefMethSpec IfaceType -- Nothing => no default method -- Just False => ordinary polymorphic default method @@ -122,13 +127,35 @@ data IfaceAT = IfaceAT IfaceDecl [IfaceAxBranch] -- Just ds => default associated type instance from these templates instance Outputable IfaceAxBranch where - ppr (IfaceAxBranch { ifaxbTyVars = tvs, ifaxbLHS = pat_tys, ifaxbRHS = ty }) - = ppr tvs <+> hsep (map ppr pat_tys) <+> char '=' <+> ppr ty + ppr = pprAxBranch Nothing + +pprAxBranch :: Maybe IfaceTyCon -> IfaceAxBranch -> SDoc +pprAxBranch mtycon (IfaceAxBranch { ifaxbTyVars = tvs + , ifaxbLHS = pat_tys + , ifaxbRHS = ty + , ifaxbIncomps = incomps }) + = ppr tvs <+> ppr_lhs <+> char '=' <+> ppr ty $+$ + nest 4 maybe_incomps + where + ppr_lhs + | Just tycon <- mtycon + = ppr (IfaceTyConApp tycon pat_tys) + | otherwise + = hsep (map ppr pat_tys) + + maybe_incomps + | [] <- incomps + = empty + + | otherwise + = parens (ptext (sLit "incompatible indices:") <+> ppr incomps) -- this is just like CoAxBranch -data IfaceAxBranch = IfaceAxBranch { ifaxbTyVars :: [IfaceTvBndr] - , ifaxbLHS :: [IfaceType] - , ifaxbRHS :: IfaceType } +data IfaceAxBranch = IfaceAxBranch { ifaxbTyVars :: [IfaceTvBndr] + , ifaxbLHS :: [IfaceType] + , ifaxbRHS :: IfaceType + , ifaxbIncomps :: [BranchIndex] } + -- See Note [Storing compatibility] in CoAxiom data IfaceConDecls = IfAbstractTyCon Bool -- c.f TyCon.AbstractTyCon @@ -173,12 +200,10 @@ data IfaceClsInst -- and if the head does not change it won't be used if it wasn't before -- The ifFamInstTys field of IfaceFamInst contains a list of the rough --- match types, one per branch... but each "rough match types" is itself --- a list of Maybe IfaceTyCon. So, we get [[Maybe IfaceTyCon]]. +-- match types data IfaceFamInst = IfaceFamInst { ifFamInstFam :: IfExtName -- Family name - , ifFamInstBranched :: Bool -- Is this branched? - , ifFamInstTys :: [[Maybe IfaceTyCon]] -- See above + , ifFamInstTys :: [Maybe IfaceTyCon] -- See above , ifFamInstAxiom :: IfExtName -- The axiom , ifFamInstOrph :: Maybe OccName -- Just like IfaceClsInst } @@ -497,15 +522,20 @@ pprIfaceDecl (IfaceForeign {ifName = tycon}) pprIfaceDecl (IfaceSyn {ifName = tycon, ifTyVars = tyvars, - ifSynRhs = SynonymTyCon mono_ty}) + ifSynRhs = IfaceSynonymTyCon mono_ty}) = hang (ptext (sLit "type") <+> pprIfaceDeclHead [] tycon tyvars) 4 (vcat [equals <+> ppr mono_ty]) pprIfaceDecl (IfaceSyn {ifName = tycon, ifTyVars = tyvars, - ifSynRhs = SynFamilyTyCon {}, ifSynKind = kind }) + ifSynRhs = IfaceOpenSynFamilyTyCon, ifSynKind = kind }) = hang (ptext (sLit "type family") <+> pprIfaceDeclHead [] tycon tyvars) 4 (dcolon <+> ppr kind) +pprIfaceDecl (IfaceSyn {ifName = tycon, ifTyVars = tyvars, + ifSynRhs = IfaceClosedSynFamilyTyCon {}, ifSynKind = kind }) + = hang (ptext (sLit "closed type family") <+> pprIfaceDeclHead [] tycon tyvars) + 4 (dcolon <+> ppr kind) + pprIfaceDecl (IfaceData {ifName = tycon, ifCType = cType, ifCtxt = context, ifTyVars = tyvars, ifCons = condecls, @@ -535,10 +565,7 @@ pprIfaceDecl (IfaceClass {ifCtxt = context, ifName = clas, ifTyVars = tyvars, pprIfaceDecl (IfaceAxiom {ifName = name, ifTyCon = tycon, ifAxBranches = branches }) = hang (ptext (sLit "axiom") <+> ppr name <> colon) - 2 (vcat $ map ppr_branch branches) - where - ppr_branch (IfaceAxBranch { ifaxbTyVars = tyvars, ifaxbLHS = lhs, ifaxbRHS = rhs }) - = pprIfaceTvBndrs tyvars <> dot <+> ppr (IfaceTyConApp tycon lhs) <+> text "~#" <+> ppr rhs + 2 (vcat $ map (pprAxBranch $ Just tycon) branches) pprCType :: Maybe CType -> SDoc pprCType Nothing = ptext (sLit "No C type associated") @@ -623,10 +650,10 @@ instance Outputable IfaceClsInst where 2 (equals <+> ppr dfun_id) instance Outputable IfaceFamInst where - ppr (IfaceFamInst {ifFamInstFam = fam, ifFamInstTys = mb_tcss, + ppr (IfaceFamInst {ifFamInstFam = fam, ifFamInstTys = mb_tcs, ifFamInstAxiom = tycon_ax}) = hang (ptext (sLit "family instance") <+> - ppr fam <+> pprWithCommas (brackets . pprWithCommas ppr_rough) mb_tcss) + ppr fam <+> pprWithCommas (brackets . ppr_rough) mb_tcs) 2 (equals <+> ppr tycon_ax) ppr_rough :: Maybe IfaceTyCon -> SDoc @@ -820,9 +847,10 @@ freeNamesIfIdDetails (IfRecSelId tc _) = freeNamesIfTc tc freeNamesIfIdDetails _ = emptyNameSet -- All other changes are handled via the version info on the tycon -freeNamesIfSynRhs :: SynTyConRhs IfaceType -> NameSet -freeNamesIfSynRhs (SynonymTyCon ty) = freeNamesIfType ty -freeNamesIfSynRhs _ = emptyNameSet +freeNamesIfSynRhs :: IfaceSynTyConRhs -> NameSet +freeNamesIfSynRhs (IfaceSynonymTyCon ty) = freeNamesIfType ty +freeNamesIfSynRhs IfaceOpenSynFamilyTyCon = emptyNameSet +freeNamesIfSynRhs (IfaceClosedSynFamilyTyCon ax) = unitNameSet ax freeNamesIfContext :: IfaceContext -> NameSet freeNamesIfContext = fnList freeNamesIfType diff --git a/compiler/iface/IfaceType.lhs b/compiler/iface/IfaceType.lhs index 103d336dbb..480eb7e0ba 100644 --- a/compiler/iface/IfaceType.lhs +++ b/compiler/iface/IfaceType.lhs @@ -90,7 +90,7 @@ newtype IfaceTyCon = IfaceTc { ifaceTyConName :: IfExtName } -- Coercion constructors data IfaceCoCon - = IfaceCoAx IfExtName Int -- Int is 0-indexed branch number + = IfaceCoAx IfExtName BranchIndex -- BranchIndex is 0-indexed branch number | IfaceReflCo | IfaceUnsafeCo | IfaceSymCo | IfaceTransCo | IfaceInstCo | IfaceNthCo Int | IfaceLRCo LeftOrRight diff --git a/compiler/iface/MkIface.lhs b/compiler/iface/MkIface.lhs index 13b64cdb25..d9bd6fc941 100644 --- a/compiler/iface/MkIface.lhs +++ b/compiler/iface/MkIface.lhs @@ -311,7 +311,6 @@ mkIface_ hsc_env maybe_old_fingerprint mi_warn_fn = mkIfaceWarnCache warns, mi_fix_fn = mkIfaceFixCache fixities } } - ; (new_iface, no_change_at_all) <- {-# SCC "versioninfo" #-} addFingerprints hsc_env maybe_old_fingerprint @@ -1445,16 +1444,33 @@ coAxiomToIfaceDecl :: CoAxiom br -> IfaceDecl coAxiomToIfaceDecl ax@(CoAxiom { co_ax_tc = tycon, co_ax_branches = branches }) = IfaceAxiom { ifName = name , ifTyCon = toIfaceTyCon tycon - , ifAxBranches = brListMap (coAxBranchToIfaceBranch emptyTidyEnv) branches } + , ifAxBranches = brListMap (coAxBranchToIfaceBranch + emptyTidyEnv + (brListMap coAxBranchLHS branches)) branches } where name = getOccName ax - -coAxBranchToIfaceBranch :: TidyEnv -> CoAxBranch -> IfaceAxBranch -coAxBranchToIfaceBranch env0 (CoAxBranch { cab_tvs = tvs, cab_lhs = lhs, cab_rhs = rhs }) +-- 2nd parameter is the list of branch LHSs, for conversion from incompatible branches +-- to incompatible indices +-- See [Storing compatibility] in CoAxiom +coAxBranchToIfaceBranch :: TidyEnv -> [[Type]] -> CoAxBranch -> IfaceAxBranch +coAxBranchToIfaceBranch env0 lhs_s + branch@(CoAxBranch { cab_incomps = incomps }) + = (coAxBranchToIfaceBranch' env0 branch) { ifaxbIncomps = iface_incomps } + where + iface_incomps = map (expectJust "iface_incomps" + . (flip findIndex lhs_s + . eqTypes) + . coAxBranchLHS) incomps + +-- use this one for standalone branches without incompatibles +coAxBranchToIfaceBranch' :: TidyEnv -> CoAxBranch -> IfaceAxBranch +coAxBranchToIfaceBranch' env0 + (CoAxBranch { cab_tvs = tvs, cab_lhs = lhs, cab_rhs = rhs }) = IfaceAxBranch { ifaxbTyVars = toIfaceTvBndrs tv_bndrs , ifaxbLHS = map (tidyToIfaceType env1) lhs - , ifaxbRHS = tidyToIfaceType env1 rhs } + , ifaxbRHS = tidyToIfaceType env1 rhs + , ifaxbIncomps = [] } where (env1, tv_bndrs) = tidyTyVarBndrs env0 tvs @@ -1491,8 +1507,9 @@ tyConToIfaceDecl env tycon where (env1, tyvars) = tidyTyClTyVarBndrs env (tyConTyVars tycon) - to_ifsyn_rhs (SynFamilyTyCon a b) = SynFamilyTyCon a b - to_ifsyn_rhs (SynonymTyCon ty) = SynonymTyCon (tidyToIfaceType env1 ty) + to_ifsyn_rhs OpenSynFamilyTyCon = IfaceOpenSynFamilyTyCon + to_ifsyn_rhs (ClosedSynFamilyTyCon ax) = IfaceClosedSynFamilyTyCon (coAxiomName ax) + to_ifsyn_rhs (SynonymTyCon ty) = IfaceSynonymTyCon (tidyToIfaceType env1 ty) ifaceConDecls (NewTyCon { data_con = con }) = IfNewTyCon (ifaceConDecl con) ifaceConDecls (DataTyCon { data_cons = cons }) = IfDataTyCon (map ifaceConDecl cons) @@ -1550,7 +1567,7 @@ classToIfaceDecl env clas toIfaceAT :: ClassATItem -> IfaceAT toIfaceAT (tc, defs) - = IfaceAT (tyConToIfaceDecl env1 tc) (map (coAxBranchToIfaceBranch env1) defs) + = IfaceAT (tyConToIfaceDecl env1 tc) (map (coAxBranchToIfaceBranch' env1) defs) toIfaceClassOp (sel_id, def_meth) = ASSERT(sel_tyvars == clas_tyvars) @@ -1638,19 +1655,15 @@ instanceToIfaceInst (ClsInst { is_dfun = dfun_id, is_flag = oflag (n : _) -> Just (nameOccName n) -------------------------- -famInstToIfaceFamInst :: FamInst br -> IfaceFamInst +famInstToIfaceFamInst :: FamInst -> IfaceFamInst famInstToIfaceFamInst (FamInst { fi_axiom = axiom, - fi_branched = branched, fi_fam = fam, - fi_branches = branches }) + fi_tcs = roughs }) = IfaceFamInst { ifFamInstAxiom = coAxiomName axiom , ifFamInstFam = fam - , ifFamInstBranched = branched - , ifFamInstTys = map (map do_rough) roughs + , ifFamInstTys = map do_rough roughs , ifFamInstOrph = orph } where - roughs = brListMap famInstBranchRoughMatch branches - do_rough Nothing = Nothing do_rough (Just n) = Just (toIfaceTyCon_name n) diff --git a/compiler/iface/TcIface.lhs b/compiler/iface/TcIface.lhs index 4c7435a554..af9d8f609c 100644 --- a/compiler/iface/TcIface.lhs +++ b/compiler/iface/TcIface.lhs @@ -490,9 +490,12 @@ tc_iface_decl parent _ (IfaceSyn {ifName = occ_name, ifTyVars = tv_bndrs, ; return (ATyCon tycon) } where mk_doc n = ptext (sLit "Type syonym") <+> ppr n - tc_syn_rhs (SynFamilyTyCon a b) = return (SynFamilyTyCon a b) - tc_syn_rhs (SynonymTyCon ty) = do { rhs_ty <- tcIfaceType ty - ; return (SynonymTyCon rhs_ty) } + tc_syn_rhs IfaceOpenSynFamilyTyCon = return OpenSynFamilyTyCon + tc_syn_rhs (IfaceClosedSynFamilyTyCon ax_name) + = do { ax <- tcIfaceCoAxiom ax_name + ; return (ClosedSynFamilyTyCon ax) } + tc_syn_rhs (IfaceSynonymTyCon ty) = do { rhs_ty <- tcIfaceType ty + ; return (SynonymTyCon rhs_ty) } tc_iface_decl _parent ignore_prags (IfaceClass {ifCtxt = rdr_ctxt, ifName = tc_occ, @@ -535,7 +538,7 @@ tc_iface_decl _parent ignore_prags tc_at cls (IfaceAT tc_decl defs_decls) = do ATyCon tc <- tc_iface_decl (AssocFamilyTyCon cls) ignore_prags tc_decl - defs <- mapM tc_ax_branch defs_decls + defs <- foldlM tc_ax_branches [] defs_decls return (tc, defs) mk_op_doc op_name op_ty = ptext (sLit "Class op") <+> sep [ppr op_name, ppr op_ty] @@ -552,23 +555,28 @@ tc_iface_decl _ _ (IfaceForeign {ifName = rdr_name, ifExtName = ext_name}) tc_iface_decl _ _ (IfaceAxiom {ifName = ax_occ, ifTyCon = tc, ifAxBranches = branches}) = do { tc_name <- lookupIfaceTop ax_occ ; tc_tycon <- tcIfaceTyCon tc - ; tc_branches <- mapM tc_ax_branch branches - ; let axiom = CoAxiom { co_ax_unique = nameUnique tc_name + ; tc_branches <- foldlM tc_ax_branches [] branches + ; let axiom = computeAxiomIncomps $ + CoAxiom { co_ax_unique = nameUnique tc_name , co_ax_name = tc_name , co_ax_tc = tc_tycon , co_ax_branches = toBranchList tc_branches , co_ax_implicit = False } ; return (ACoAxiom axiom) } -tc_ax_branch :: IfaceAxBranch -> IfL CoAxBranch -tc_ax_branch (IfaceAxBranch { ifaxbTyVars = tv_bndrs, ifaxbLHS = lhs, ifaxbRHS = rhs }) +tc_ax_branches :: [CoAxBranch] -> IfaceAxBranch -> IfL [CoAxBranch] +tc_ax_branches prev_branches + (IfaceAxBranch { ifaxbTyVars = tv_bndrs, ifaxbLHS = lhs, ifaxbRHS = rhs + , ifaxbIncomps = incomps }) = bindIfaceTyVars tv_bndrs $ \ tvs -> do -- Variables will all be fresh { tc_lhs <- mapM tcIfaceType lhs ; tc_rhs <- tcIfaceType rhs - ; return (CoAxBranch { cab_loc = noSrcSpan - , cab_tvs = tvs - , cab_lhs = tc_lhs - , cab_rhs = tc_rhs } ) } + ; let br = CoAxBranch { cab_loc = noSrcSpan + , cab_tvs = tvs + , cab_lhs = tc_lhs + , cab_rhs = tc_rhs + , cab_incomps = map (prev_branches !!) incomps } + ; return (prev_branches ++ [br]) } tcIfaceDataCons :: Name -> TyCon -> [TyVar] -> IfaceConDecls -> IfL AlgTyConRhs tcIfaceDataCons tycon_name tycon _ if_cons @@ -664,13 +672,15 @@ tcIfaceInst (IfaceClsInst { ifDFun = dfun_occ, ifOFlag = oflag ; let mb_tcs' = map (fmap ifaceTyConName) mb_tcs ; return (mkImportedInstance cls mb_tcs' dfun oflag) } -tcIfaceFamInst :: IfaceFamInst -> IfL (FamInst Branched) -tcIfaceFamInst (IfaceFamInst { ifFamInstFam = fam, ifFamInstTys = mb_tcss - , ifFamInstBranched = branched, ifFamInstAxiom = axiom_name } ) +tcIfaceFamInst :: IfaceFamInst -> IfL FamInst +tcIfaceFamInst (IfaceFamInst { ifFamInstFam = fam, ifFamInstTys = mb_tcs + , ifFamInstAxiom = axiom_name } ) = do { axiom' <- forkM (ptext (sLit "Axiom") <+> ppr axiom_name) $ tcIfaceCoAxiom axiom_name - ; let mb_tcss' = map (map (fmap ifaceTyConName)) mb_tcss - ; return (mkImportedFamInst fam branched mb_tcss' axiom') } + -- will panic if branched, but that's OK + ; let axiom'' = toUnbranchedAxiom axiom' + mb_tcs' = map (fmap ifaceTyConName) mb_tcs + ; return (mkImportedFamInst fam mb_tcs' axiom'') } \end{code} diff --git a/compiler/iface/TcIface.lhs-boot b/compiler/iface/TcIface.lhs-boot index 58df07cdc4..591419a251 100644 --- a/compiler/iface/TcIface.lhs-boot +++ b/compiler/iface/TcIface.lhs-boot @@ -5,7 +5,7 @@ import IfaceSyn ( IfaceDecl, IfaceClsInst, IfaceFamInst, IfaceRule, IfaceAnno import TypeRep ( TyThing ) import TcRnTypes ( IfL ) import InstEnv ( ClsInst ) -import FamInstEnv ( FamInst, Branched ) +import FamInstEnv ( FamInst ) import CoreSyn ( CoreRule ) import HscTypes ( TypeEnv, VectInfo, IfaceVectInfo ) import Module ( Module ) @@ -15,7 +15,7 @@ tcIfaceDecl :: Bool -> IfaceDecl -> IfL TyThing tcIfaceRules :: Bool -> [IfaceRule] -> IfL [CoreRule] tcIfaceVectInfo :: Module -> TypeEnv -> IfaceVectInfo -> IfL VectInfo tcIfaceInst :: IfaceClsInst -> IfL ClsInst -tcIfaceFamInst :: IfaceFamInst -> IfL (FamInst Branched) +tcIfaceFamInst :: IfaceFamInst -> IfL FamInst tcIfaceAnnotations :: [IfaceAnnotation] -> IfL [Annotation] \end{code} diff --git a/compiler/main/GHC.hs b/compiler/main/GHC.hs index a4aba138b9..39e1e0a453 100644 --- a/compiler/main/GHC.hs +++ b/compiler/main/GHC.hs @@ -157,7 +157,7 @@ module GHC ( TyCon, tyConTyVars, tyConDataCons, tyConArity, isClassTyCon, isSynTyCon, isNewTyCon, isPrimTyCon, isFunTyCon, - isFamilyTyCon, tyConClass_maybe, + isFamilyTyCon, isOpenFamilyTyCon, tyConClass_maybe, synTyConRhs_maybe, synTyConDefn_maybe, synTyConResKind, -- ** Type variables @@ -182,7 +182,7 @@ module GHC ( pprInstance, pprInstanceHdr, pprFamInst, - FamInst, Branched, + FamInst, -- ** Types and Kinds Type, splitForAllTys, funResultTy, @@ -1004,7 +1004,7 @@ getBindings = withSession $ \hsc_env -> return $ icInScopeTTs $ hsc_IC hsc_env -- | Return the instances for the current interactive session. -getInsts :: GhcMonad m => m ([ClsInst], [FamInst Branched]) +getInsts :: GhcMonad m => m ([ClsInst], [FamInst]) getInsts = withSession $ \hsc_env -> return $ ic_instances (hsc_IC hsc_env) diff --git a/compiler/main/HscMain.hs b/compiler/main/HscMain.hs index caa68d5ddf..d94fc7842f 100644 --- a/compiler/main/HscMain.hs +++ b/compiler/main/HscMain.hs @@ -303,7 +303,7 @@ hscTcRcLookupName hsc_env0 name = runInteractiveHsc hsc_env0 $ do -- "name not found", and the Maybe in the return type -- is used to indicate that. -hscTcRnGetInfo :: HscEnv -> Name -> IO (Maybe (TyThing, Fixity, [ClsInst], [FamInst Branched])) +hscTcRnGetInfo :: HscEnv -> Name -> IO (Maybe (TyThing, Fixity, [ClsInst], [FamInst])) hscTcRnGetInfo hsc_env0 name = runInteractiveHsc hsc_env0 $ do hsc_env <- getHscEnv ioMsgMaybe' $ tcRnGetInfo hsc_env name diff --git a/compiler/main/HscTypes.lhs b/compiler/main/HscTypes.lhs index 28134e1545..163af051e8 100644 --- a/compiler/main/HscTypes.lhs +++ b/compiler/main/HscTypes.lhs @@ -456,7 +456,7 @@ lookupIfaceByModule dflags hpt pit mod -- modules imported by this one, directly or indirectly, and are in the Home -- Package Table. This ensures that we don't see instances from modules @--make@ -- compiled before this one, but which are not below this one. -hptInstances :: HscEnv -> (ModuleName -> Bool) -> ([ClsInst], [FamInst Branched]) +hptInstances :: HscEnv -> (ModuleName -> Bool) -> ([ClsInst], [FamInst]) hptInstances hsc_env want_this_module = let (insts, famInsts) = unzip $ flip hptAllThings hsc_env $ \mod_info -> do guard (want_this_module (moduleName (mi_module (hm_iface mod_info)))) @@ -777,7 +777,7 @@ data ModDetails md_exports :: [AvailInfo], md_types :: !TypeEnv, -- ^ Local type environment for this particular module md_insts :: ![ClsInst], -- ^ 'DFunId's for the instances in this module - md_fam_insts :: ![FamInst Branched], + md_fam_insts :: ![FamInst], md_rules :: ![CoreRule], -- ^ Domain may include 'Id's from other modules md_anns :: ![Annotation], -- ^ Annotations present in this module: currently -- they only annotate things also declared in this module @@ -823,7 +823,7 @@ data ModGuts mg_tcs :: ![TyCon], -- ^ TyCons declared in this module -- (includes TyCons for classes) mg_insts :: ![ClsInst], -- ^ Class instances declared in this module - mg_fam_insts :: ![FamInst Branched], + mg_fam_insts :: ![FamInst], -- ^ Family instances declared in this module mg_rules :: ![CoreRule], -- ^ Before the core pipeline starts, contains -- See Note [Overall plumbing for rules] in Rules.lhs @@ -953,7 +953,7 @@ data InteractiveContext -- ^ Variables defined automatically by the system (e.g. -- record field selectors). See Notes [ic_sys_vars] - ic_instances :: ([ClsInst], [FamInst Branched]), + ic_instances :: ([ClsInst], [FamInst]), -- ^ All instances and family instances created during -- this session. These are grabbed en masse after each -- update to be sure that proper overlapping is retained. @@ -1280,10 +1280,12 @@ implicitTyConThings tc extras_plus :: TyThing -> [TyThing] extras_plus thing = thing : implicitTyThings thing --- For newtypes (only) add the implicit coercion tycon +-- For newtypes and closed type families (only) add the implicit coercion tycon implicitCoTyCon :: TyCon -> [TyThing] implicitCoTyCon tc | Just co <- newTyConCo_maybe tc = [ACoAxiom $ toBranchedAxiom co] + | Just co <- isClosedSynFamilyTyCon_maybe tc + = [ACoAxiom co] | otherwise = [] -- | Returns @True@ if there should be no interface-file declaration @@ -1379,12 +1381,12 @@ mkTypeEnvWithImplicits things = `plusNameEnv` mkTypeEnv (concatMap implicitTyThings things) -typeEnvFromEntities :: [Id] -> [TyCon] -> [FamInst Branched] -> TypeEnv +typeEnvFromEntities :: [Id] -> [TyCon] -> [FamInst] -> TypeEnv typeEnvFromEntities ids tcs famInsts = mkTypeEnv ( map AnId ids ++ map ATyCon all_tcs ++ concatMap implicitTyConThings all_tcs - ++ map (ACoAxiom . famInstAxiom) famInsts + ++ map (ACoAxiom . toBranchedAxiom . famInstAxiom) famInsts ) where all_tcs = tcs ++ famInstsRepTyCons famInsts diff --git a/compiler/main/InteractiveEval.hs b/compiler/main/InteractiveEval.hs index 391de5a42f..635c194a92 100644 --- a/compiler/main/InteractiveEval.hs +++ b/compiler/main/InteractiveEval.hs @@ -45,7 +45,7 @@ import HscMain import HsSyn import HscTypes import InstEnv -import FamInstEnv ( FamInst, Branched, orphNamesOfFamInst ) +import FamInstEnv ( FamInst, orphNamesOfFamInst ) import TyCon import Type hiding( typeKind ) import TcType hiding( typeKind ) @@ -890,7 +890,7 @@ moduleIsInterpreted modl = withSession $ \h -> -- are in scope (qualified or otherwise). Otherwise we list a whole lot too many! -- The exact choice of which ones to show, and which to hide, is a judgement call. -- (see Trac #1581) -getInfo :: GhcMonad m => Bool -> Name -> m (Maybe (TyThing,Fixity,[ClsInst],[FamInst Branched])) +getInfo :: GhcMonad m => Bool -> Name -> m (Maybe (TyThing,Fixity,[ClsInst],[FamInst])) getInfo allInfo name = withSession $ \hsc_env -> do mb_stuff <- liftIO $ hscTcRnGetInfo hsc_env name diff --git a/compiler/main/PprTyThing.hs b/compiler/main/PprTyThing.hs index 5145f56005..56d7afc4fa 100644 --- a/compiler/main/PprTyThing.hs +++ b/compiler/main/PprTyThing.hs @@ -29,7 +29,8 @@ import GHC ( TyThing(..) ) import DataCon import Id import TyCon -import Coercion( pprCoAxiom ) +import Coercion( pprCoAxiom, pprCoAxBranch ) +import CoAxiom( CoAxiom(..), brListMap ) import HscTypes( tyThingParent_maybe ) import Type( tidyTopType, tidyOpenType ) import TypeRep( pprTvBndrs ) @@ -175,10 +176,14 @@ pprTyCon :: PrintExplicitForalls -> ShowSub -> TyCon -> SDoc pprTyCon pefas ss tyCon | Just syn_rhs <- GHC.synTyConRhs_maybe tyCon = case syn_rhs of - SynFamilyTyCon {} -> pprTyConHdr pefas tyCon <+> dcolon <+> - pprTypeForUser pefas (GHC.synTyConResKind tyCon) + OpenSynFamilyTyCon -> pprTyConHdr pefas tyCon <+> dcolon <+> + pprTypeForUser pefas (GHC.synTyConResKind tyCon) + ClosedSynFamilyTyCon (CoAxiom { co_ax_branches = branches }) -> + hang (pprTyConHdr pefas tyCon <+> dcolon <+> + pprTypeForUser pefas (GHC.synTyConResKind tyCon) <+> ptext (sLit "where")) + 2 (vcat (brListMap (pprCoAxBranch tyCon) branches)) SynonymTyCon rhs_ty -> hang (pprTyConHdr pefas tyCon <+> equals) - 2 (ppr rhs_ty) -- Don't suppress foralls on RHS type! + 2 (ppr rhs_ty) -- Don't suppress foralls on RHS type! -- e.g. type T = forall a. a->a | Just cls <- GHC.tyConClass_maybe tyCon = pprClass pefas ss cls diff --git a/compiler/main/TidyPgm.lhs b/compiler/main/TidyPgm.lhs index 4608a21e8c..be4c683276 100644 --- a/compiler/main/TidyPgm.lhs +++ b/compiler/main/TidyPgm.lhs @@ -152,7 +152,7 @@ mkBootModDetailsTc hsc_env } where -mkBootTypeEnv :: NameSet -> [Id] -> [TyCon] -> [FamInst Branched] -> TypeEnv +mkBootTypeEnv :: NameSet -> [Id] -> [TyCon] -> [FamInst] -> TypeEnv mkBootTypeEnv exports ids tcs fam_insts = tidyTypeEnv True $ typeEnvFromEntities final_ids tcs fam_insts diff --git a/compiler/parser/Parser.y.pp b/compiler/parser/Parser.y.pp index 483ed87591..1545aa27f4 100644 --- a/compiler/parser/Parser.y.pp +++ b/compiler/parser/Parser.y.pp @@ -644,10 +644,10 @@ ty_decl :: { LTyClDecl RdrName } {% mkTySynonym (comb2 $1 $4) $2 $4 } -- type family declarations - | 'type' 'family' type opt_kind_sig + | 'type' 'family' type opt_kind_sig where_type_family -- Note the use of type for the head; this allows -- infix type constructors to be declared - {% do { L loc decl <- mkFamDecl (comb3 $1 $3 $4) TypeFamily $3 (unLoc $4) + {% do { L loc decl <- mkFamDecl (comb4 $1 $3 $4 $5) (unLoc $5) $3 (unLoc $4) ; return (L loc (FamDecl decl)) } } -- ordinary data type or newtype declaration @@ -684,9 +684,6 @@ inst_decl :: { LInstDecl RdrName } {% do { L loc tfi <- mkTyFamInst (comb2 $1 $3) $3 ; return (L loc (TyFamInstD { tfid_inst = tfi })) } } - | 'type' 'instance' 'where' ty_fam_inst_eqn_list - { LL (TyFamInstD { tfid_inst = mkTyFamInstGroup (unLoc $4) }) } - -- data/newtype instance declaration | data_or_newtype 'instance' tycl_hdr constrs deriving {% do { L loc d <- mkFamInstData (comb4 $1 $3 $4 $5) (unLoc $1) Nothing $3 @@ -701,14 +698,19 @@ inst_decl :: { LInstDecl RdrName } (unLoc $4) (unLoc $5) (unLoc $6) ; return (L loc (DataFamInstD { dfid_inst = d })) } } --- Type instance groups +-- Closed type families + +where_type_family :: { Located (FamilyInfo RdrName) } + : {- empty -} { noLoc OpenTypeFamily } + | 'where' ty_fam_inst_eqn_list + { LL (ClosedTypeFamily (reverse (unLoc $2))) } ty_fam_inst_eqn_list :: { Located [LTyFamInstEqn RdrName] } : '{' ty_fam_inst_eqns '}' { LL (unLoc $2) } | vocurly ty_fam_inst_eqns close { $2 } ty_fam_inst_eqns :: { Located [LTyFamInstEqn RdrName] } - : ty_fam_inst_eqn ';' ty_fam_inst_eqns { LL ($1 : unLoc $3) } + : ty_fam_inst_eqns ';' ty_fam_inst_eqn { LL ($3 : unLoc $1) } | ty_fam_inst_eqns ';' { LL (unLoc $1) } | ty_fam_inst_eqn { LL [$1] } @@ -716,7 +718,8 @@ ty_fam_inst_eqn :: { LTyFamInstEqn RdrName } : type '=' ctype -- Note the use of type for the head; this allows -- infix type constructors and type patterns - {% mkTyFamInstEqn (comb2 $1 $3) $1 $3 } + {% do { eqn <- mkTyFamInstEqn $1 $3 + ; return (LL eqn) } } -- Associated type family declarations -- @@ -732,7 +735,7 @@ at_decl_cls :: { LHsDecl RdrName } : 'type' type opt_kind_sig -- Note the use of type for the head; this allows -- infix type constructors to be declared. - {% do { L loc decl <- mkFamDecl (comb3 $1 $2 $3) TypeFamily $2 (unLoc $3) + {% do { L loc decl <- mkFamDecl (comb3 $1 $2 $3) OpenTypeFamily $2 (unLoc $3) ; return (L loc (TyClD (FamDecl decl))) } } | 'data' type opt_kind_sig diff --git a/compiler/parser/RdrHsSyn.lhs b/compiler/parser/RdrHsSyn.lhs index 3695daef58..e8c23cad52 100644 --- a/compiler/parser/RdrHsSyn.lhs +++ b/compiler/parser/RdrHsSyn.lhs @@ -10,7 +10,7 @@ module RdrHsSyn ( mkHsDo, mkHsSplice, mkTopSpliceDecl, mkClassDecl, mkTyData, mkFamInstData, - mkTySynonym, mkTyFamInstEqn, mkTyFamInstGroup, + mkTySynonym, mkTyFamInstEqn, mkTyFamInst, mkFamDecl, splitCon, mkInlinePragma, @@ -178,39 +178,31 @@ mkTySynonym loc lhs rhs ; return (L loc (SynDecl { tcdLName = tc, tcdTyVars = tyvars, tcdRhs = rhs, tcdFVs = placeHolderNames })) } -mkTyFamInstEqn :: SrcSpan +mkTyFamInstEqn :: LHsType RdrName -> LHsType RdrName - -> LHsType RdrName - -> P (LTyFamInstEqn RdrName) -mkTyFamInstEqn loc lhs rhs + -> P (TyFamInstEqn RdrName) +mkTyFamInstEqn lhs rhs = do { (tc, tparams) <- checkTyClHdr lhs - ; return (L loc (TyFamInstEqn { tfie_tycon = tc - , tfie_pats = mkHsWithBndrs tparams - , tfie_rhs = rhs })) } + ; return (TyFamInstEqn { tfie_tycon = tc + , tfie_pats = mkHsWithBndrs tparams + , tfie_rhs = rhs }) } mkTyFamInst :: SrcSpan -> LTyFamInstEqn RdrName -> P (LTyFamInstDecl RdrName) mkTyFamInst loc eqn - = return (L loc (TyFamInstDecl { tfid_eqns = [eqn] - , tfid_group = False - , tfid_fvs = placeHolderNames })) - -mkTyFamInstGroup :: [LTyFamInstEqn RdrName] - -> TyFamInstDecl RdrName -mkTyFamInstGroup eqns = TyFamInstDecl { tfid_eqns = eqns - , tfid_group = True - , tfid_fvs = placeHolderNames } + = return (L loc (TyFamInstDecl { tfid_eqn = eqn + , tfid_fvs = placeHolderNames })) mkFamDecl :: SrcSpan - -> FamilyFlavour + -> FamilyInfo RdrName -> LHsType RdrName -- LHS -> Maybe (LHsKind RdrName) -- Optional kind signature -> P (LFamilyDecl RdrName) -mkFamDecl loc flavour lhs ksig +mkFamDecl loc info lhs ksig = do { (tc, tparams) <- checkTyClHdr lhs ; tyvars <- checkTyVars lhs tparams - ; return (L loc (FamilyDecl flavour tc tyvars ksig)) } + ; return (L loc (FamilyDecl info tc tyvars ksig)) } mkTopSpliceDecl :: LHsExpr RdrName -> HsDecl RdrName -- If the user wrote diff --git a/compiler/prelude/TysPrim.lhs b/compiler/prelude/TysPrim.lhs index f702689e93..a10300a99c 100644 --- a/compiler/prelude/TysPrim.lhs +++ b/compiler/prelude/TysPrim.lhs @@ -731,6 +731,7 @@ anyTyCon = mkLiftedPrimTyCon anyTyConName kind 1 PtrRep where kind = ForAllTy kKiVar (mkTyVarTy kKiVar) {- Can't do this yet without messing up kind proxies +-- RAE: I think you can now. anyTyCon :: TyCon anyTyCon = mkSynTyCon anyTyConName kind [kKiVar] syn_rhs diff --git a/compiler/rename/RnSource.lhs b/compiler/rename/RnSource.lhs index cc410388df..e1236cac10 100644 --- a/compiler/rename/RnSource.lhs +++ b/compiler/rename/RnSource.lhs @@ -542,10 +542,9 @@ rnFamInstDecl doc mb_cls tycon pats payload rnPayload rnTyFamInstDecl :: Maybe (Name, [Name]) -> TyFamInstDecl RdrName -> RnM (TyFamInstDecl Name, FreeVars) -rnTyFamInstDecl mb_cls (TyFamInstDecl { tfid_eqns = eqns, tfid_group = group }) - = do { (eqns', fvs) <- rnList (rnTyFamInstEqn mb_cls) eqns - ; return (TyFamInstDecl { tfid_eqns = eqns' - , tfid_group = group +rnTyFamInstDecl mb_cls (TyFamInstDecl { tfid_eqn = L loc eqn }) + = do { (eqn', fvs) <- rnTyFamInstEqn mb_cls eqn + ; return (TyFamInstDecl { tfid_eqn = L loc eqn' , tfid_fvs = fvs }, fvs) } rnTyFamInstEqn :: Maybe (Name, [Name]) @@ -1044,16 +1043,27 @@ rnFamDecl :: Maybe Name -> FamilyDecl RdrName -> RnM (FamilyDecl Name, FreeVars) rnFamDecl mb_cls (FamilyDecl { fdLName = tycon, fdTyVars = tyvars - , fdFlavour = flav, fdKindSig = kind }) - = bindHsTyVars fmly_doc mb_cls kvs tyvars $ \tyvars' -> - do { tycon' <- lookupLocatedTopBndrRn tycon - ; (kind', fv_kind) <- rnLHsMaybeKind fmly_doc kind + , fdInfo = info, fdKindSig = kind }) + = do { ((tycon', tyvars', kind'), fv1) <- + bindHsTyVars fmly_doc mb_cls kvs tyvars $ \tyvars' -> + do { tycon' <- lookupLocatedTopBndrRn tycon + ; (kind', fv_kind) <- rnLHsMaybeKind fmly_doc kind + ; return ((tycon', tyvars', kind'), fv_kind) } + ; (info', fv2) <- rn_info info ; return (FamilyDecl { fdLName = tycon', fdTyVars = tyvars' - , fdFlavour = flav, fdKindSig = kind' } - , fv_kind ) } + , fdInfo = info', fdKindSig = kind' } + , fv1 `plusFV` fv2) } where fmly_doc = TyFamilyCtx tycon kvs = extractRdrKindSigVars kind + + rn_info (ClosedTypeFamily eqns) + = do { (eqns', fvs) <- rnList (rnTyFamInstEqn Nothing) eqns + -- no class context, + ; return (ClosedTypeFamily eqns', fvs) } + rn_info OpenTypeFamily = return (OpenTypeFamily, emptyFVs) + rn_info DataFamily = return (DataFamily, emptyFVs) + \end{code} Note [Stupid theta] diff --git a/compiler/typecheck/FamInst.lhs b/compiler/typecheck/FamInst.lhs index 44a0cefac5..3f220b1339 100644 --- a/compiler/typecheck/FamInst.lhs +++ b/compiler/typecheck/FamInst.lhs @@ -35,6 +35,7 @@ import Maybes import TcMType import TcType import Name +import VarSet -- RAE import Control.Monad import Data.Map (Map) import qualified Data.Map as Map @@ -53,34 +54,27 @@ import qualified Data.Map as Map -- creates the fresh variables and applies the necessary substitution -- It is defined here to avoid a dependency from FamInstEnv on the monad -- code. -newFamInst :: FamFlavor -> Bool -> CoAxiom br -> TcRnIf gbl lcl(FamInst br) + +newFamInst :: FamFlavor -> CoAxiom Unbranched -> TcRnIf gbl lcl FamInst -- Freshen the type variables of the FamInst branches -- Called from the vectoriser monad too, hence the rather general type -newFamInst flavor is_branched axiom@(CoAxiom { co_ax_tc = fam_tc - , co_ax_branches = ax_branches }) - = do { fam_branches <- go ax_branches - ; return (FamInst { fi_fam = tyConName fam_tc +newFamInst flavor axiom@(CoAxiom { co_ax_branches = FirstBranch branch + , co_ax_tc = fam_tc }) + = do { (subst, tvs') <- tcInstSkolTyVarsLoc loc tvs + ; return (FamInst { fi_fam = fam_tc_name , fi_flavor = flavor - , fi_branches = fam_branches - , fi_branched = is_branched + , fi_tcs = roughMatchTcs lhs + , fi_tvs = tvs' + , fi_tys = substTys subst lhs + , fi_rhs = substTy subst rhs , fi_axiom = axiom }) } where - go :: BranchList CoAxBranch br -> TcRnIf gbl lcl (BranchList FamInstBranch br) - go (FirstBranch br) = do { br' <- go_branch br - ; return (FirstBranch br') } - go (NextBranch br brs) = do { br' <- go_branch br - ; brs' <- go brs - ;return (NextBranch br' brs') } - go_branch :: CoAxBranch -> TcRnIf gbl lcl FamInstBranch - go_branch (CoAxBranch { cab_tvs = tvs1 - , cab_lhs = lhs - , cab_loc = loc - , cab_rhs = rhs }) - = do { (subst, tvs2) <- tcInstSkolTyVarsLoc loc tvs1 - ; return (FamInstBranch { fib_tvs = tvs2 - , fib_lhs = substTys subst lhs - , fib_rhs = substTy subst rhs - , fib_tcs = roughMatchTcs lhs }) } + fam_tc_name = tyConName fam_tc + CoAxBranch { cab_loc = loc + , cab_tvs = tvs + , cab_lhs = lhs + , cab_rhs = rhs } = branch + \end{code} @@ -218,14 +212,14 @@ which implies that :R42T was declared as 'data instance T [a]'. \begin{code} tcLookupFamInst :: TyCon -> [Type] -> TcM (Maybe FamInstMatch) tcLookupFamInst tycon tys - | not (isFamilyTyCon tycon) + | not (isOpenFamilyTyCon tycon) = return Nothing | otherwise = do { instEnv <- tcGetFamInstEnvs ; let mb_match = lookupFamInstEnv instEnv tycon tys --- ; traceTc "lookupFamInst" ((ppr tycon <+> ppr tys) $$ --- pprTvBndrs (varSetElems (tyVarsOfTypes tys)) $$ --- ppr mb_match $$ ppr instEnv) + ; traceTc "lookupFamInst" ((ppr tycon <+> ppr tys) $$ + pprTvBndrs (varSetElems (tyVarsOfTypes tys)) $$ + ppr mb_match $$ ppr instEnv) ; case mb_match of [] -> return Nothing (match:_) @@ -242,7 +236,7 @@ tcLookupFamInst tycon tys \begin{code} -- Add new locally-defined family instances -tcExtendLocalFamInstEnv :: [FamInst br] -> TcM a -> TcM a +tcExtendLocalFamInstEnv :: [FamInst] -> TcM a -> TcM a tcExtendLocalFamInstEnv fam_insts thing_inside = do { env <- getGblEnv ; (inst_env', fam_insts') <- foldlM addLocalFamInst @@ -257,7 +251,7 @@ tcExtendLocalFamInstEnv fam_insts thing_inside -- and then add it to the home inst env -- This must be lazy in the fam_inst arguments, see Note [Lazy axiom match] -- in FamInstEnv.lhs -addLocalFamInst :: (FamInstEnv,[FamInst Branched]) -> FamInst br -> TcM (FamInstEnv, [FamInst Branched]) +addLocalFamInst :: (FamInstEnv,[FamInst]) -> FamInst -> TcM (FamInstEnv, [FamInst]) addLocalFamInst (home_fie, my_fis) fam_inst -- home_fie includes home package and this module -- my_fies is just the ones from this module @@ -276,13 +270,12 @@ addLocalFamInst (home_fie, my_fis) fam_inst -- overlaps correctly ; eps <- getEps ; let inst_envs = (eps_fam_inst_env eps, home_fie') - fam_inst' = toBranchedFamInst fam_inst - home_fie'' = extendFamInstEnv home_fie fam_inst' + home_fie'' = extendFamInstEnv home_fie fam_inst -- Check for conflicting instance decls - ; no_conflict <- checkForConflicts inst_envs fam_inst' + ; no_conflict <- checkForConflicts inst_envs fam_inst ; if no_conflict then - return (home_fie'', fam_inst' : my_fis') + return (home_fie'', fam_inst : my_fis') else return (home_fie, my_fis) } @@ -298,39 +291,35 @@ Check whether a single family instance conflicts with those in two instance environments (one for the EPS and one for the HPT). \begin{code} -checkForConflicts :: FamInstEnvs -> FamInst Branched -> TcM Bool -checkForConflicts inst_envs fam_inst@(FamInst { fi_branches = branches - , fi_branched = branched }) - = do { let conflicts = brListMap (lookupFamInstEnvConflicts inst_envs branched fam_tc) branches - no_conflicts = all null conflicts - ; traceTc "checkForConflicts" (ppr conflicts $$ ppr fam_inst $$ ppr inst_envs) - ; unless no_conflicts $ - zipWithM_ (conflictInstErr fam_inst) (brListIndices branches) conflicts +checkForConflicts :: FamInstEnvs -> FamInst -> TcM Bool +checkForConflicts inst_envs fam_inst + = do { let conflicts = lookupFamInstEnvConflicts inst_envs fam_inst + no_conflicts = null conflicts + ; traceTc "checkForConflicts" (ppr (map fim_instance conflicts) $$ + ppr fam_inst $$ ppr inst_envs) + ; unless no_conflicts $ conflictInstErr fam_inst conflicts ; return no_conflicts } - where fam_tc = famInstTyCon fam_inst -conflictInstErr :: FamInst Branched -> BranchIndex -> [FamInstMatch] -> TcRn () -conflictInstErr fam_inst branch conflictingMatch - | (FamInstMatch { fim_instance = confInst - , fim_index = confIndex }) : _ <- conflictingMatch +conflictInstErr :: FamInst -> [FamInstMatch] -> TcRn () +conflictInstErr fam_inst conflictingMatch + | (FamInstMatch { fim_instance = confInst }) : _ <- conflictingMatch = addFamInstsErr (ptext (sLit "Conflicting family instance declarations:")) - [(fam_inst, branch), - (confInst, confIndex) ] - | otherwise -- no conflict on this branch; see Trac #7560 - = return () + [fam_inst, confInst] + | otherwise + = panic "conflictInstErr" -addFamInstsErr :: SDoc -> [(FamInst Branched, Int)] -> TcRn () +addFamInstsErr :: SDoc -> [FamInst] -> TcRn () addFamInstsErr herald insts = ASSERT( not (null insts) ) setSrcSpan srcSpan $ addErr $ hang herald - 2 (vcat [ pprCoAxBranchHdr (famInstAxiom fi) index - | (fi,index) <- sorted ]) + 2 (vcat [ pprCoAxBranchHdr (famInstAxiom fi) 0 + | fi <- sorted ]) where - getSpan = getSrcLoc . famInstAxiom . fst + getSpan = getSrcLoc . famInstAxiom sorted = sortWith getSpan insts - (fi1,ix1) = head sorted - srcSpan = coAxBranchSpan (coAxiomNthBranch (famInstAxiom fi1) ix1) + fi1 = head sorted + srcSpan = coAxBranchSpan (coAxiomSingleBranch (famInstAxiom fi1)) -- The sortWith just arranges that instances are dislayed in order -- of source location, which reduced wobbling in error messages, -- and is better for users diff --git a/compiler/typecheck/TcDeriv.lhs b/compiler/typecheck/TcDeriv.lhs index ac2d81072a..21e2bbb5b9 100644 --- a/compiler/typecheck/TcDeriv.lhs +++ b/compiler/typecheck/TcDeriv.lhs @@ -46,7 +46,6 @@ import RdrName import Name import NameSet import TyCon -import CoAxiom import TcType import Var import VarSet @@ -355,7 +354,7 @@ tcDeriving tycl_decls inst_decls deriv_decls where ddump_deriving :: Bag (InstInfo Name) -> HsValBinds Name -> Bag TyCon -- ^ Empty data constructors - -> Bag (FamInst Unbranched) -- ^ Rep type family instances + -> Bag (FamInst) -- ^ Rep type family instances -> SDoc ddump_deriving inst_infos extra_binds repMetaTys repFamInsts = hang (ptext (sLit "Derived instances:")) @@ -370,12 +369,11 @@ tcDeriving tycl_decls inst_decls deriv_decls hangP s x = text "" $$ hang (ptext (sLit s)) 2 x -- Prints the representable type family instance -pprRepTy :: FamInst Unbranched -> SDoc -pprRepTy fi@(FamInst { fi_branches = FirstBranch (FamInstBranch { fib_lhs = lhs - , fib_rhs = rhs }) }) +pprRepTy :: FamInst -> SDoc +pprRepTy fi@(FamInst { fi_tys = lhs }) = ptext (sLit "type") <+> ppr (mkTyConApp (famInstTyCon fi) lhs) <+> - equals <+> ppr rhs - + equals <+> ppr rhs + where rhs = famInstRHS fi -- As of 24 April 2012, this only shares MetaTyCons between derivations of -- Generic and Generic1; thus the types and logic are quite simple. @@ -552,8 +550,9 @@ deriveFamInst decl@(DataFamInstDecl { dfid_tycon = L _ tc_name, dfid_pats = pats , dfid_defn = HsDataDefn { dd_derivs = Just preds } }) = tcAddDataFamInstCtxt decl $ do { fam_tc <- tcLookupTyCon tc_name - ; tcFamTyPats fam_tc pats (\_ -> return ()) $ \ tvs' pats' _ -> - mapM (deriveTyData tvs' fam_tc pats') preds } + ; tcFamTyPats tc_name (tyConKind fam_tc) pats (\_ -> return ()) $ + \ tvs' pats' _ -> + mapM (deriveTyData tvs' fam_tc pats') preds } -- Tiresomely we must figure out the "lhs", which is awkward for type families -- E.g. data T a b = .. deriving( Eq ) -- Here, the lhs is (T a b) @@ -744,10 +743,8 @@ mkEqnHelp orig tvs cls cls_tys tc_app mtheta Nothing -> bale_out (ptext (sLit "No family instance for") <+> quotes (pprTypeApp tycon tys)) Just (FamInstMatch { fim_instance = famInst - , fim_index = index , fim_tys = tys }) - -> ASSERT( index == 0 ) - let tycon' = dataFamInstRepTyCon famInst + -> let tycon' = dataFamInstRepTyCon famInst in return (tycon', tys) } \end{code} diff --git a/compiler/typecheck/TcEnv.lhs b/compiler/typecheck/TcEnv.lhs index 528c06cbd5..058e84a22e 100644 --- a/compiler/typecheck/TcEnv.lhs +++ b/compiler/typecheck/TcEnv.lhs @@ -734,8 +734,9 @@ newGlobalBinder. newFamInstTyConName :: Located Name -> [Type] -> TcM Name newFamInstTyConName (L loc name) tys = mk_fam_inst_name id loc name [tys] -newFamInstAxiomName :: SrcSpan -> Name -> [[Type]] -> TcM Name -newFamInstAxiomName = mk_fam_inst_name mkInstTyCoOcc +newFamInstAxiomName :: SrcSpan -> Name -> [CoAxBranch] -> TcM Name +newFamInstAxiomName loc name branches + = mk_fam_inst_name mkInstTyCoOcc loc name (map coAxBranchLHS branches) mk_fam_inst_name :: (OccName -> OccName) -> SrcSpan -> Name -> [[Type]] -> TcM Name mk_fam_inst_name adaptOcc loc tc_name tyss diff --git a/compiler/typecheck/TcExpr.lhs b/compiler/typecheck/TcExpr.lhs index f58c466566..8615293a17 100644 --- a/compiler/typecheck/TcExpr.lhs +++ b/compiler/typecheck/TcExpr.lhs @@ -1238,9 +1238,8 @@ tcTagToEnum loc fun_name arg res_ty ; case mb_fam of Nothing -> failWithTc (tagToEnumError ty doc3) Just (FamInstMatch { fim_instance = rep_fam - , fim_index = index , fim_tys = rep_args }) - -> return ( mkTcSymCo (mkTcAxInstCo co_tc index rep_args) + -> return ( mkTcSymCo (mkTcUnbranchedAxInstCo co_tc rep_args) , rep_tc, rep_args ) where co_tc = famInstAxiom rep_fam diff --git a/compiler/typecheck/TcGenDeriv.lhs b/compiler/typecheck/TcGenDeriv.lhs index 564756269e..77bda8274b 100644 --- a/compiler/typecheck/TcGenDeriv.lhs +++ b/compiler/typecheck/TcGenDeriv.lhs @@ -51,7 +51,6 @@ import PrelNames hiding (error_RDR) import PrimOp import SrcLoc import TyCon -import CoAxiom import TcType import TysPrim import TysWiredIn @@ -87,7 +86,7 @@ data DerivStuff -- Please add this auxiliary stuff -- Generics | DerivTyCon TyCon -- New data types - | DerivFamInst (FamInst Unbranched) -- New type family instances + | DerivFamInst (FamInst) -- New type family instances -- New top-level auxiliary bindings | DerivHsBind (LHsBind RdrName, LSig RdrName) -- Also used for SYB @@ -1916,7 +1915,7 @@ type SeparateBagsDerivStuff = -- AuxBinds and SYB bindings ( Bag (LHsBind RdrName, LSig RdrName) -- Extra bindings (used by Generic only) , Bag TyCon -- Extra top-level datatypes - , Bag (FamInst Unbranched) -- Extra family instances + , Bag (FamInst) -- Extra family instances , Bag (InstInfo RdrName)) -- Extra instances genAuxBinds :: SrcSpan -> BagDerivStuff -> SeparateBagsDerivStuff diff --git a/compiler/typecheck/TcGenGenerics.lhs b/compiler/typecheck/TcGenGenerics.lhs index cd233751ff..f4765e9425 100644 --- a/compiler/typecheck/TcGenGenerics.lhs +++ b/compiler/typecheck/TcGenGenerics.lhs @@ -27,9 +27,7 @@ import TcType import TcGenDeriv import DataCon import TyCon -import CoAxiom -import Coercion ( mkSingleCoAxiom ) -import FamInstEnv ( FamInst, FamFlavor(..) ) +import FamInstEnv ( FamInst, FamFlavor(..), mkSingleCoAxiom ) import FamInst import Module ( Module, moduleName, moduleNameString ) import IfaceEnv ( newGlobalBinder ) @@ -72,7 +70,7 @@ For the generic representation we need to generate: \begin{code} gen_Generic_binds :: GenericKind -> TyCon -> MetaTyCons -> Module - -> TcM (LHsBinds RdrName, FamInst Unbranched) + -> TcM (LHsBinds RdrName, FamInst) gen_Generic_binds gk tc metaTyCons mod = do repTyInsts <- tc_mkRepFamInsts gk tc metaTyCons mod return (mkBindsRep gk tc, repTyInsts) @@ -404,7 +402,7 @@ tc_mkRepFamInsts :: GenericKind -- Gen0 or Gen1 -> TyCon -- The type to generate representation for -> MetaTyCons -- Metadata datatypes to refer to -> Module -- Used as the location of the new RepTy - -> TcM (FamInst Unbranched) -- Generated representation0 coercion + -> TcM (FamInst) -- Generated representation0 coercion tc_mkRepFamInsts gk tycon metaDts mod = -- Consider the example input tycon `D`, where data D a b = D_ a -- Also consider `R:DInt`, where { data family D x y :: * -> * @@ -445,7 +443,7 @@ tc_mkRepFamInsts gk tycon metaDts mod = (nameSrcSpan (tyConName tycon)) ; let axiom = mkSingleCoAxiom rep_name tyvars fam_tc appT repTy - ; newFamInst SynFamilyInst False axiom } + ; newFamInst SynFamilyInst axiom } -------------------------------------------------------------------------------- -- Type representation diff --git a/compiler/typecheck/TcHsType.lhs b/compiler/typecheck/TcHsType.lhs index d810b0a2f8..c7d65a6b57 100644 --- a/compiler/typecheck/TcHsType.lhs +++ b/compiler/typecheck/TcHsType.lhs @@ -18,7 +18,7 @@ module TcHsType ( UserTypeCtxt(..), -- Type checking type and class decls - kcTyClTyVars, tcTyClTyVars, + kcLookupKind, kcTyClTyVars, tcTyClTyVars, tcHsConArgType, tcDataKindSig, tcClassSigType, diff --git a/compiler/typecheck/TcInstDcls.lhs b/compiler/typecheck/TcInstDcls.lhs index 753bc327be..2156bba9db 100644 --- a/compiler/typecheck/TcInstDcls.lhs +++ b/compiler/typecheck/TcInstDcls.lhs @@ -31,7 +31,6 @@ import TcRnMonad import TcValidity import TcMType import TcType -import Coercion( mkSingleCoAxiom, mkBranchedCoAxiom, pprCoAxBranch ) import BuildTyCl import Inst import InstEnv @@ -455,7 +454,7 @@ addClsInsts :: [InstInfo Name] -> TcM a -> TcM a addClsInsts infos thing_inside = tcExtendLocalInstEnv (map iSpec infos) thing_inside -addFamInsts :: [FamInst Branched] -> TcM a -> TcM a +addFamInsts :: [FamInst] -> TcM a -> TcM a -- Extend (a) the family instance envt -- (b) the type envt with stuff from data type decls addFamInsts fam_insts thing_inside @@ -465,7 +464,7 @@ addFamInsts fam_insts thing_inside ; tcg_env <- tcAddImplicits things ; setGblEnv tcg_env thing_inside } where - axioms = map famInstAxiom fam_insts + axioms = map (toBranchedAxiom . famInstAxiom) fam_insts tycons = famInstsRepTyCons fam_insts things = map ATyCon tycons ++ map ACoAxiom axioms \end{code} @@ -489,7 +488,7 @@ the brutal solution will do. \begin{code} tcLocalInstDecl :: LInstDecl Name - -> TcM ([InstInfo Name], [FamInst Branched]) + -> TcM ([InstInfo Name], [FamInst]) -- A source-file instance declaration -- Type-check all the stuff before the "where" -- @@ -500,13 +499,13 @@ tcLocalInstDecl (L loc (TyFamInstD { tfid_inst = decl })) tcLocalInstDecl (L loc (DataFamInstD { dfid_inst = decl })) = do { fam_inst <- tcDataFamInstDecl Nothing (L loc decl) - ; return ([], [toBranchedFamInst fam_inst]) } + ; return ([], [fam_inst]) } tcLocalInstDecl (L loc (ClsInstD { cid_inst = decl })) = do { (insts, fam_insts) <- tcClsInstDecl (L loc decl) - ; return (insts, map toBranchedFamInst fam_insts) } + ; return (insts, fam_insts) } -tcClsInstDecl :: LClsInstDecl Name -> TcM ([InstInfo Name], [FamInst Unbranched]) +tcClsInstDecl :: LClsInstDecl Name -> TcM ([InstInfo Name], [FamInst]) tcClsInstDecl (L loc (ClsInstDecl { cid_poly_ty = poly_ty, cid_binds = binds , cid_sigs = uprags, cid_tyfam_insts = ats , cid_datafam_insts = adts })) @@ -533,7 +532,7 @@ tcClsInstDecl (L loc (ClsInstDecl { cid_poly_ty = poly_ty, cid_binds = binds ; let defined_ats = mkNameSet $ map (tyFamInstDeclName . unLoc) ats defined_adts = mkNameSet $ map (unLoc . dfid_tycon . unLoc) adts - mk_deflt_at_instances :: ClassATItem -> TcM [FamInst Unbranched] + mk_deflt_at_instances :: ClassATItem -> TcM [FamInst] mk_deflt_at_instances (fam_tc, defs) -- User supplied instances ==> everything is OK | tyConName fam_tc `elemNameSet` defined_ats @@ -558,7 +557,7 @@ tcClsInstDecl (L loc (ClsInstDecl { cid_poly_ty = poly_ty, cid_binds = binds ; rep_tc_name <- newFamInstTyConName (noLoc (tyConName fam_tc)) pat_tys' ; let axiom = mkSingleCoAxiom rep_tc_name tvs' fam_tc pat_tys' rhs' ; ASSERT( tyVarsOfType rhs' `subVarSet` tv_set' ) - newFamInst SynFamilyInst False {- group -} axiom } + newFamInst SynFamilyInst axiom } ; tyfam_insts1 <- mapM mk_deflt_at_instances (classATItems clas) @@ -581,10 +580,10 @@ tcClsInstDecl (L loc (ClsInstDecl { cid_poly_ty = poly_ty, cid_binds = binds tcAssocTyDecl :: Class -- Class of associated type -> VarEnv Type -- Instantiation of class TyVars -> LTyFamInstDecl Name - -> TcM (FamInst Unbranched) + -> TcM (FamInst) tcAssocTyDecl clas mini_env ldecl = do { fam_inst <- tcTyFamInstDecl (Just (clas, mini_env)) ldecl - ; return $ toUnbranchedFamInst fam_inst } + ; return fam_inst } \end{code} %************************************************************************ @@ -620,14 +619,12 @@ tcFamInstDeclCombined mb_clsinfo fam_tc_lname ; return fam_tc } tcTyFamInstDecl :: Maybe (Class, VarEnv Type) -- the class & mini_env if applicable - -> LTyFamInstDecl Name -> TcM (FamInst Branched) + -> LTyFamInstDecl Name -> TcM FamInst -- "type instance" -tcTyFamInstDecl mb_clsinfo (L loc decl@(TyFamInstDecl { tfid_group = group - , tfid_eqns = eqns })) +tcTyFamInstDecl mb_clsinfo (L loc decl@(TyFamInstDecl { tfid_eqn = eqn })) = setSrcSpan loc $ tcAddTyFamInstCtxt decl $ - do { let (eqn1:_) = eqns - fam_lname = tfie_tycon (unLoc eqn1) + do { let fam_lname = tfie_tycon (unLoc eqn) ; fam_tc <- tcFamInstDeclCombined mb_clsinfo fam_lname -- (0) Check it's an open type family @@ -637,36 +634,20 @@ tcTyFamInstDecl mb_clsinfo (L loc decl@(TyFamInstDecl { tfid_group = group (notOpenFamily fam_tc) -- (1) do the work of verifying the synonym group - ; co_ax_branches <- tcSynFamInstDecl fam_tc decl + ; co_ax_branch <- tcSynFamInstDecl fam_tc decl - -- (2) check for validity and inaccessibility - ; foldlM_ (check_valid_branch fam_tc) [] co_ax_branches + -- (2) check for validity + ; checkValidTyFamInst mb_clsinfo fam_tc co_ax_branch -- (3) construct coercion axiom ; rep_tc_name <- newFamInstAxiomName loc (tyFamInstDeclName decl) - (map cab_lhs co_ax_branches) - ; let axiom = mkBranchedCoAxiom rep_tc_name fam_tc co_ax_branches - ; newFamInst SynFamilyInst group axiom } - where - check_valid_branch :: TyCon - -> [CoAxBranch] -- previous - -> CoAxBranch -- current - -> TcM [CoAxBranch] -- current : previous - check_valid_branch fam_tc prev_branches cur_branch - = do { -- Check the well-formedness of the instance - checkValidTyFamInst mb_clsinfo fam_tc cur_branch - - -- Check whether the branch is dominated by earlier - -- ones and hence is inaccessible - ; when (cur_branch `isDominatedBy` prev_branches) $ - setSrcSpan (coAxBranchSpan cur_branch) $ - addErrTc $ inaccessibleCoAxBranch fam_tc cur_branch - - ; return $ cur_branch : prev_branches } + [co_ax_branch] + ; let axiom = mkUnbranchedCoAxiom rep_tc_name fam_tc co_ax_branch + ; newFamInst SynFamilyInst axiom } tcDataFamInstDecl :: Maybe (Class, VarEnv Type) - -> LDataFamInstDecl Name -> TcM (FamInst Unbranched) + -> LDataFamInstDecl Name -> TcM FamInst -- "newtype instance" and "data instance" tcDataFamInstDecl mb_clsinfo (L loc decl@(DataFamInstDecl @@ -683,7 +664,7 @@ tcDataFamInstDecl mb_clsinfo ; checkTc (isAlgTyCon fam_tc) (wrongKindOfFamily fam_tc) -- Kind check type patterns - ; tcFamTyPats fam_tc pats (kcDataDefn defn) $ + ; tcFamTyPats (unLoc fam_tc_name) (tyConKind fam_tc) pats (kcDataDefn defn) $ \tvs' pats' res_kind -> do { -- Check that left-hand side contains no type family applications @@ -725,7 +706,7 @@ tcDataFamInstDecl mb_clsinfo -- further instance might not introduce a new recursive -- dependency. (2) They are always valid loop breakers as -- they involve a coercion. - ; fam_inst <- newFamInst (DataFamilyInst rep_tc) False axiom + ; fam_inst <- newFamInst (DataFamilyInst rep_tc) axiom ; return (rep_tc, fam_inst) } -- Remember to check validity; no recursion to worry about here @@ -765,6 +746,8 @@ Solution: eta-reduce both axioms, thus: Now d' = d |> Monad (sym (ax2 ; ax1)) +This eta reduction happens both for data instances and newtype instances. + See Note [Newtype eta] in TyCon. @@ -1576,11 +1559,6 @@ badFamInstDecl tc_name quotes (ppr tc_name) , nest 2 (parens $ ptext (sLit "Use -XTypeFamilies to allow indexed type families")) ] -inaccessibleCoAxBranch :: TyCon -> CoAxBranch -> SDoc -inaccessibleCoAxBranch tc fi - = ptext (sLit "Inaccessible family instance equation:") $$ - (pprCoAxBranch tc fi) - notOpenFamily :: TyCon -> SDoc notOpenFamily tc = ptext (sLit "Illegal instance for closed family") <+> quotes (ppr tc) diff --git a/compiler/typecheck/TcInteract.lhs b/compiler/typecheck/TcInteract.lhs index 42238a8769..27cf52e85e 100644 --- a/compiler/typecheck/TcInteract.lhs +++ b/compiler/typecheck/TcInteract.lhs @@ -20,7 +20,6 @@ import VarSet import Type import Unify import FamInstEnv -import Coercion( mkAxInstRHS ) import Var import TcType @@ -1431,17 +1430,13 @@ doTopReactFunEq _ct fl fun_tc args xi loc do { match_res <- matchFam fun_tc args -- See Note [MATCHING-SYNONYMS] ; case match_res of { Nothing -> return NoTopInt ; - Just (FamInstMatch { fim_instance = famInst - , fim_index = index - , fim_tys = rep_tys }) -> + Just (co, ty) -> -- Found a top-level instance do { -- Add it to the solved goals unless (isDerived fl) (addSolvedFunEq fam_ty fl xi) - ; let coe_ax = famInstAxiom famInst - ; succeed_with "Fun/Top" (mkTcAxInstCo coe_ax index rep_tys) - (mkAxInstRHS coe_ax index rep_tys) } } } } } + ; succeed_with "Fun/Top" co ty } } } } } where fam_ty = mkTyConApp fun_tc args @@ -1709,17 +1704,17 @@ matchClassInst _ clas [ k, ty ] _ case unwrapNewTyCon_maybe (classTyCon clas) of Just (_,dictRep, axDict) | Just tcSing <- tyConAppTyCon_maybe dictRep -> - do mbInst <- matchFam tcSing [k,ty] + do mbInst <- matchOpenFam tcSing [k,ty] case mbInst of Just FamInstMatch { fim_instance = FamInst { fi_axiom = axDataFam , fi_flavor = DataFamilyInst tcon } - , fim_index = ix, fim_tys = tys + , fim_tys = tys } | Just (_,_,axSing) <- unwrapNewTyCon_maybe tcon -> do let co1 = mkTcSymCo $ mkTcUnbranchedAxInstCo axSing tys - co2 = mkTcSymCo $ mkTcAxInstCo axDataFam ix tys + co2 = mkTcSymCo $ mkTcUnbranchedAxInstCo axDataFam tys co3 = mkTcSymCo $ mkTcUnbranchedAxInstCo axDict [k,ty] return $ GenInst [] $ EvCast (EvLit evLit) $ mkTcTransCo co1 $ mkTcTransCo co2 co3 diff --git a/compiler/typecheck/TcRnDriver.lhs b/compiler/typecheck/TcRnDriver.lhs index 08590203a3..56cdf60afc 100644 --- a/compiler/typecheck/TcRnDriver.lhs +++ b/compiler/typecheck/TcRnDriver.lhs @@ -460,6 +460,7 @@ tcRnSrcDecls boot_iface decls tcg_fords = fords' } } ; setGlobalTypeEnv tcg_env' final_type_env + } } tc_rn_src_decls :: ModDetails @@ -487,7 +488,7 @@ tc_rn_src_decls boot_details ds case group_tail of { Nothing -> do { tcg_env <- checkMain ; -- Check for `main' traceTc "returning from tc_rn_src_decls: " $ - ppr $ nameEnvElts $ tcg_type_env tcg_env ; -- RAE + ppr $ nameEnvElts $ tcg_type_env tcg_env ; return (tcg_env, tcl_env) } ; @@ -769,8 +770,9 @@ checkBootTyCon tc1 tc2 , Just syn_rhs2 <- synTyConRhs_maybe tc2 , Just env <- eqTyVarBndrs emptyRnEnv2 (tyConTyVars tc1) (tyConTyVars tc2) = ASSERT(tc1 == tc2) - let eqSynRhs (SynFamilyTyCon o1 i1) (SynFamilyTyCon o2 i2) - = o1==o2 && i1==i2 + let eqSynRhs OpenSynFamilyTyCon OpenSynFamilyTyCon = True + eqSynRhs (ClosedSynFamilyTyCon ax1) (ClosedSynFamilyTyCon ax2) + = ax1 == ax2 eqSynRhs (SynonymTyCon t1) (SynonymTyCon t2) = eqTypeX env t1 t2 eqSynRhs _ _ = False @@ -956,7 +958,6 @@ tcTopSrcDecls boot_details -- tcg_dus: see Note [Newtype constructor usage in foreign declarations] addUsedRdrNames fo_rdr_names ; - traceTc "Tc8: type_env: " (ppr $ nameEnvElts $ tcg_type_env tcg_env') ; -- RAE return (tcg_env', tcl_env) }}}}}} where @@ -1654,13 +1655,8 @@ tcRnDeclsi hsc_env ictxt local_decls = tcg_vects = vects', tcg_fords = fords' } - tcg_env'' <- setGlobalTypeEnv tcg_env' final_type_env - - traceTc "returning from tcRnDeclsi: " $ ppr $ nameEnvElts $ tcg_type_env tcg_env'' -- RAE - - return tcg_env'' - - + setGlobalTypeEnv tcg_env' final_type_env + #endif /* GHCi */ \end{code} @@ -1738,7 +1734,7 @@ tcRnLookupName' name = do tcRnGetInfo :: HscEnv -> Name - -> IO (Messages, Maybe (TyThing, Fixity, [ClsInst], [FamInst Branched])) + -> IO (Messages, Maybe (TyThing, Fixity, [ClsInst], [FamInst])) -- Used to implement :info in GHCi -- @@ -1763,13 +1759,13 @@ tcRnGetInfo hsc_env name (cls_insts, fam_insts) <- lookupInsts thing return (thing, fixity, cls_insts, fam_insts) -lookupInsts :: TyThing -> TcM ([ClsInst],[FamInst Branched]) +lookupInsts :: TyThing -> TcM ([ClsInst],[FamInst]) lookupInsts (ATyCon tc) | Just cls <- tyConClass_maybe tc = do { inst_envs <- tcGetInstEnvs ; return (classInstances inst_envs cls, []) } - | isFamilyTyCon tc || isTyConAssoc tc + | isOpenFamilyTyCon tc || isTyConAssoc tc = do { inst_envs <- tcGetFamInstEnvs ; return ([], familyInstances inst_envs tc) } @@ -1901,7 +1897,7 @@ ppr_types insts type_env -- that the type checker has invented. Top-level user-defined things -- have External names. -ppr_tycons :: [FamInst br] -> TypeEnv -> SDoc +ppr_tycons :: [FamInst] -> TypeEnv -> SDoc ppr_tycons fam_insts type_env = vcat [ text "TYPE CONSTRUCTORS" , nest 2 (ppr_tydecls tycons) @@ -1919,7 +1915,7 @@ ppr_insts :: [ClsInst] -> SDoc ppr_insts [] = empty ppr_insts ispecs = text "INSTANCES" $$ nest 2 (pprInstances ispecs) -ppr_fam_insts :: [FamInst br] -> SDoc +ppr_fam_insts :: [FamInst] -> SDoc ppr_fam_insts [] = empty ppr_fam_insts fam_insts = text "FAMILY INSTANCES" $$ nest 2 (pprFamInsts fam_insts) diff --git a/compiler/typecheck/TcRnTypes.lhs b/compiler/typecheck/TcRnTypes.lhs index b53c40d358..43b4f36aa2 100644 --- a/compiler/typecheck/TcRnTypes.lhs +++ b/compiler/typecheck/TcRnTypes.lhs @@ -298,7 +298,7 @@ data TcGblEnv tcg_anns :: [Annotation], -- ...Annotations tcg_tcs :: [TyCon], -- ...TyCons and Classes tcg_insts :: [ClsInst], -- ...Instances - tcg_fam_insts :: [FamInst Branched],-- ...Family instances + tcg_fam_insts :: [FamInst], -- ...Family instances tcg_rules :: [LRuleDecl Id], -- ...Rules tcg_fords :: [LForeignDecl Id], -- ...Foreign import & exports tcg_vects :: [LVectDecl Id], -- ...Vectorisation declarations diff --git a/compiler/typecheck/TcSMonad.lhs b/compiler/typecheck/TcSMonad.lhs index 930444a1ba..9a7049fcca 100644 --- a/compiler/typecheck/TcSMonad.lhs +++ b/compiler/typecheck/TcSMonad.lhs @@ -86,7 +86,7 @@ module TcSMonad ( getDefaultInfo, getDynFlags, - matchClass, matchFam, MatchInstResult (..), + matchClass, matchFam, matchOpenFam, MatchInstResult (..), checkWellStagedDFun, pprEq -- Smaller utils, re-exported from TcM -- TODO (DV): these are only really used in the @@ -132,6 +132,7 @@ import TcRnTypes import Unique import UniqFM import Maybes ( orElse, catMaybes, firstJust ) +import Pair ( pSnd ) import Control.Monad( unless, when, zipWithM ) import Data.IORef @@ -1674,8 +1675,30 @@ matchClass clas tys } } -matchFam :: TyCon -> [Type] -> TcS (Maybe FamInstMatch) -matchFam tycon args = wrapTcS $ tcLookupFamInst tycon args +matchOpenFam :: TyCon -> [Type] -> TcS (Maybe FamInstMatch) +matchOpenFam tycon args = wrapTcS $ tcLookupFamInst tycon args + +matchFam :: TyCon -> [Type] -> TcS (Maybe (TcCoercion, TcType)) +matchFam tycon args + | isOpenSynFamilyTyCon tycon + = do { maybe_match <- matchOpenFam tycon args + ; case maybe_match of + Nothing -> return Nothing + Just (FamInstMatch { fim_instance = famInst + , fim_tys = inst_tys }) + -> let co = mkTcUnbranchedAxInstCo (famInstAxiom famInst) inst_tys + ty = pSnd $ tcCoercionKind co + in return $ Just (co, ty) } + + | Just ax <- isClosedSynFamilyTyCon_maybe tycon + , Just (ind, inst_tys) <- chooseBranch ax args + = let co = mkTcAxInstCo ax ind inst_tys + ty = pSnd (tcCoercionKind co) + in return $ Just (co, ty) + + | otherwise + = return Nothing + \end{code} \begin{code} diff --git a/compiler/typecheck/TcSplice.lhs b/compiler/typecheck/TcSplice.lhs index 2561bd967c..59b06d4a8e 100644 --- a/compiler/typecheck/TcSplice.lhs +++ b/compiler/typecheck/TcSplice.lhs @@ -1027,7 +1027,7 @@ reifyInstances th_nm th_tys -> do { inst_envs <- tcGetInstEnvs ; let (matches, unifies, _) = lookupInstEnv inst_envs cls tys ; mapM reifyClassInstance (map fst matches ++ unifies) } - | isFamilyTyCon tc + | isOpenFamilyTyCon tc -> do { inst_envs <- tcGetFamInstEnvs ; let matches = lookupFamInstEnv inst_envs tc tys ; mapM (reifyFamilyInstance . fim_instance) matches } @@ -1169,7 +1169,6 @@ reifyThing (AGlobal (AnId id)) } reifyThing (AGlobal (ATyCon tc)) = reifyTyCon tc -reifyThing (AGlobal (ACoAxiom ax)) = reifyAxiom ax reifyThing (AGlobal (ADataCon dc)) = do { let name = dataConName dc ; ty <- reifyType (idType (dataConWrapId dc)) @@ -1192,12 +1191,7 @@ reifyThing (ATyVar tv tv1) reifyThing thing = pprPanic "reifyThing" (pprTcTyThingCategory thing) ------------------------------- -reifyAxiom :: CoAxiom br -> TcM TH.Info -reifyAxiom (CoAxiom { co_ax_tc = tc, co_ax_branches = branches }) - = do { eqns <- sequence $ brListMap reifyAxBranch branches - ; return (TH.TyConI (TH.TySynInstD (reifyName tc) eqns)) } - +------------------------------------------- reifyAxBranch :: CoAxBranch -> TcM TH.TySynEqn reifyAxBranch (CoAxBranch { cab_lhs = args, cab_rhs = rhs }) = do { args' <- mapM reifyType args @@ -1216,18 +1210,24 @@ reifyTyCon tc = return (TH.PrimTyConI (reifyName tc) (tyConArity tc) (isUnLiftedTyCon tc)) | isFamilyTyCon tc - = do { let flavour = reifyFamFlavour tc - tvs = tyConTyVars tc + = do { let tvs = tyConTyVars tc kind = tyConKind tc ; kind' <- if isLiftedTypeKind kind then return Nothing else fmap Just (reifyKind kind) - ; fam_envs <- tcGetFamInstEnvs - ; instances <- mapM reifyFamilyInstance (familyInstances fam_envs tc) ; tvs' <- reifyTyVars tvs - ; return (TH.FamilyI - (TH.FamilyD flavour (reifyName tc) tvs' kind') - instances) } + ; flav' <- reifyFamFlavour tc + ; case flav' of + { Left flav -> -- open type/data family + do { fam_envs <- tcGetFamInstEnvs + ; instances <- mapM reifyFamilyInstance (familyInstances fam_envs tc) + ; return (TH.FamilyI + (TH.FamilyD flav (reifyName tc) tvs' kind') + instances) } + ; Right eqns -> -- closed type family + return (TH.FamilyI + (TH.ClosedTypeFamilyD (reifyName tc) tvs' kind' eqns) + []) } } | Just (tvs, rhs) <- synTyConDefn_maybe tc -- Vanilla type synonym = do { rhs' <- reifyType rhs @@ -1308,31 +1308,26 @@ reifyClassInstance i n_silent = dfunNSilent dfun ------------------------------ -reifyFamilyInstance :: FamInst br -> TcM TH.Dec -reifyFamilyInstance fi@(FamInst { fi_flavor = flavor - , fi_branches = branches - , fi_fam = fam }) +reifyFamilyInstance :: FamInst -> TcM TH.Dec +reifyFamilyInstance (FamInst { fi_flavor = flavor + , fi_fam = fam + , fi_tys = lhs + , fi_rhs = rhs }) = case flavor of SynFamilyInst -> - do { th_eqns <- sequence $ brListMap reifyFamInstBranch branches - ; return (TH.TySynInstD (reifyName fam) th_eqns) } + do { th_lhs <- reifyTypes lhs + ; th_rhs <- reifyType rhs + ; return (TH.TySynInstD (reifyName fam) (TH.TySynEqn th_lhs th_rhs)) } DataFamilyInst rep_tc -> do { let tvs = tyConTyVars rep_tc fam' = reifyName fam - lhs = famInstBranchLHS $ famInstSingleBranch (toUnbranchedFamInst fi) ; cons <- mapM (reifyDataCon (mkTyVarTys tvs)) (tyConDataCons rep_tc) ; th_tys <- reifyTypes lhs ; return (if isNewTyCon rep_tc then TH.NewtypeInstD [] fam' th_tys (head cons) [] else TH.DataInstD [] fam' th_tys cons []) } -reifyFamInstBranch :: FamInstBranch -> TcM TH.TySynEqn -reifyFamInstBranch (FamInstBranch { fib_lhs = lhs, fib_rhs = rhs }) - = do { th_lhs <- reifyTypes lhs - ; th_rhs <- reifyType rhs - ; return (TH.TySynEqn th_lhs th_rhs) } - ------------------------------ reifyType :: TypeRep.Type -> TcM TH.Type -- Monadic only because of failure @@ -1394,11 +1389,17 @@ reifyCxt = mapM reifyPred reifyFunDep :: ([TyVar], [TyVar]) -> TH.FunDep reifyFunDep (xs, ys) = TH.FunDep (map reifyName xs) (map reifyName ys) -reifyFamFlavour :: TyCon -> TH.FamFlavour -reifyFamFlavour tc | isSynFamilyTyCon tc = TH.TypeFam - | isFamilyTyCon tc = TH.DataFam - | otherwise - = panic "TcSplice.reifyFamFlavour: not a type family" +reifyFamFlavour :: TyCon -> TcM (Either TH.FamFlavour [TH.TySynEqn]) +reifyFamFlavour tc + | isOpenSynFamilyTyCon tc = return $ Left TH.TypeFam + | isDataFamilyTyCon tc = return $ Left TH.DataFam + + | Just ax <- isClosedSynFamilyTyCon_maybe tc + = do { eqns <- brListMapM reifyAxBranch $ coAxiomBranches ax + ; return $ Right eqns } + + | otherwise + = panic "TcSplice.reifyFamFlavour: not a type family" reifyTyVars :: [TyVar] -> TcM [TH.TyVarBndr] reifyTyVars = mapM reifyTyVar . filter isTypeVar diff --git a/compiler/typecheck/TcTyClsDecls.lhs b/compiler/typecheck/TcTyClsDecls.lhs index 41cbeae349..044086d937 100644 --- a/compiler/typecheck/TcTyClsDecls.lhs +++ b/compiler/typecheck/TcTyClsDecls.lhs @@ -37,11 +37,12 @@ import TcMType import TcType import TysWiredIn( unitTy ) import FamInst -import Coercion( mkCoAxBranch ) +import FamInstEnv( isDominatedBy, mkCoAxBranch, mkBranchedCoAxiom ) +import Coercion( pprCoAxBranch ) import Type import Kind import Class -import CoAxiom( CoAxBranch(..) ) +import CoAxiom import TyCon import DataCon import Id @@ -648,16 +649,53 @@ tcTyClDecl1 _ _ \begin{code} tcFamDecl1 :: TyConParent -> FamilyDecl Name -> TcM [TyThing] tcFamDecl1 parent - (FamilyDecl {fdFlavour = TypeFamily, fdLName = L _ tc_name, fdTyVars = tvs}) + (FamilyDecl {fdInfo = OpenTypeFamily, fdLName = L _ tc_name, fdTyVars = tvs}) = tcTyClTyVars tc_name tvs $ \ tvs' kind -> do - { traceTc "type family:" (ppr tc_name) + { traceTc "open type family:" (ppr tc_name) ; checkFamFlag tc_name - ; let syn_rhs = SynFamilyTyCon { synf_open = True, synf_injective = False } - ; tycon <- buildSynTyCon tc_name tvs' syn_rhs kind parent + ; tycon <- buildSynTyCon tc_name tvs' OpenSynFamilyTyCon kind parent ; return [ATyCon tycon] } tcFamDecl1 parent - (FamilyDecl {fdFlavour = DataFamily, fdLName = L _ tc_name, fdTyVars = tvs}) + (FamilyDecl { fdInfo = ClosedTypeFamily eqns + , fdLName = lname@(L _ tc_name), fdTyVars = tvs }) +-- Closed type families are a little tricky, because they contain the definition +-- of both the type family and the equations for a CoAxiom. + = do { traceTc "closed type family:" (ppr tc_name) + -- the variables in the header have no scope: + ; (tvs', kind) <- tcTyClTyVars tc_name tvs $ \ tvs' kind -> + return (tvs', kind) + + ; checkFamFlag tc_name -- make sure we have -XTypeFamilies + + -- check to make sure all the names used in the equations are + -- consistent + ; let names = map (tfie_tycon . unLoc) eqns + ; tcSynFamInstNames lname names + + -- process the equations, creating CoAxBranches + ; tycon_kind <- kcLookupKind tc_name + ; branches <- mapM (tcTyFamInstEqn tc_name tycon_kind) eqns + + -- we need the tycon that we will be creating, but it's in scope. + -- just look it up. + ; fam_tc <- tcLookupLocatedTyCon lname + + -- create a CoAxiom, with the correct src location + ; loc <- getSrcSpanM + ; co_ax_name <- newFamInstAxiomName loc tc_name branches + ; let co_ax = mkBranchedCoAxiom co_ax_name fam_tc branches + + -- now, finally, build the TyCon + ; let syn_rhs = ClosedSynFamilyTyCon co_ax + ; tycon <- buildSynTyCon tc_name tvs' syn_rhs kind parent + + ; return [ATyCon tycon, ACoAxiom co_ax] } +-- We check for instance validity later, when doing validity checking for +-- the tycon + +tcFamDecl1 parent + (FamilyDecl {fdInfo = DataFamily, fdLName = L _ tc_name, fdTyVars = tvs}) = tcTyClTyVars tc_name tvs $ \ tvs' kind -> do { traceTc "data family:" (ppr tc_name) ; checkFamFlag tc_name @@ -770,13 +808,13 @@ tcClassATs class_name parent ats at_defs tc_at at = do { [ATyCon fam_tc] <- addLocM (tcFamDecl1 parent) at ; let at_defs = lookupNameEnv at_defs_map (unLoc $ fdLName $ unLoc at) `orElse` [] - ; atd <- concatMapM (tcDefaultAssocDecl fam_tc) at_defs + ; atd <- mapM (tcDefaultAssocDecl fam_tc) at_defs ; return (fam_tc, atd) } ------------------------- tcDefaultAssocDecl :: TyCon -- ^ Family TyCon -> LTyFamInstDecl Name -- ^ RHS - -> TcM [CoAxBranch] -- ^ Type checked RHS and free TyVars + -> TcM CoAxBranch -- ^ Type checked RHS and free TyVars tcDefaultAssocDecl fam_tc (L loc decl) = setSrcSpan loc $ tcAddTyFamInstCtxt decl $ @@ -785,17 +823,12 @@ tcDefaultAssocDecl fam_tc (L loc decl) -- We check for well-formedness and validity later, in checkValidClass ------------------------- -tcSynFamInstDecl :: TyCon -> TyFamInstDecl Name -> TcM [CoAxBranch] +tcSynFamInstDecl :: TyCon -> TyFamInstDecl Name -> TcM CoAxBranch -- Placed here because type family instances appear as -- default decls in class declarations -tcSynFamInstDecl fam_tc (TyFamInstDecl { tfid_eqns = eqns }) - -- we know the first equation matches the fam_tc because of the lookup logic - -- now, just check that all other names match the first - = do { let names = map (tfie_tycon . unLoc) eqns - first = head names - ; tcSynFamInstNames first names - ; checkTc (isSynTyCon fam_tc) (wrongKindOfFamily fam_tc) - ; mapM (tcTyFamInstEqn fam_tc) eqns } +tcSynFamInstDecl fam_tc (TyFamInstDecl { tfid_eqn = eqn }) + = do { checkTc (isSynTyCon fam_tc) (wrongKindOfFamily fam_tc) + ; tcTyFamInstEqn (tyConName fam_tc) (tyConKind fam_tc) eqn } -- Checks to make sure that all the names in an instance group are the same tcSynFamInstNames :: Located Name -> [Located Name] -> TcM () @@ -808,15 +841,15 @@ tcSynFamInstNames (L _ first) names = setSrcSpan loc $ failWithTc (msg_fun name) -tcTyFamInstEqn :: TyCon -> LTyFamInstEqn Name -> TcM CoAxBranch -tcTyFamInstEqn fam_tc +tcTyFamInstEqn :: Name -> Kind -> LTyFamInstEqn Name -> TcM CoAxBranch +tcTyFamInstEqn fam_tc_name kind (L loc (TyFamInstEqn { tfie_pats = pats, tfie_rhs = hs_ty })) = setSrcSpan loc $ - tcFamTyPats fam_tc pats (discardResult . (tcCheckLHsType hs_ty)) $ + tcFamTyPats fam_tc_name kind pats (discardResult . (tcCheckLHsType hs_ty)) $ \tvs' pats' res_kind -> do { rhs_ty <- tcCheckLHsType hs_ty res_kind ; rhs_ty <- zonkTcTypeToType emptyZonkEnv rhs_ty - ; traceTc "tcSynFamInstEqn" (ppr fam_tc <+> (ppr tvs' $$ ppr pats' $$ ppr rhs_ty)) + ; traceTc "tcSynFamInstEqn" (ppr fam_tc_name <+> (ppr tvs' $$ ppr pats' $$ ppr rhs_ty)) ; return (mkCoAxBranch tvs' pats' rhs_ty loc) } kcDataDefn :: HsDataDefn Name -> TcKind -> TcM () @@ -846,7 +879,11 @@ kcResultKind (Just k) res_k -- check is only required for type synonym instances. ----------------- -tcFamTyPats :: TyCon +-- Note that we can't use the family TyCon, because this is sometimes called +-- from within a type-checking knot. So, we ask our callers to do a little more +-- work. +tcFamTyPats :: Name -- of the family TyCon + -> Kind -- of the family TyCon -> HsWithBndrs [LHsType Name] -- Patterns -> (TcKind -> TcM ()) -- Kind checker for RHS -- result is ignored @@ -863,23 +900,27 @@ tcFamTyPats :: TyCon -- In that case, the type variable 'a' will *already be in scope* -- (and, if C is poly-kinded, so will its kind parameter). -tcFamTyPats fam_tc (HsWB { hswb_cts = arg_pats, hswb_kvs = kvars, hswb_tvs = tvars }) +tcFamTyPats fam_tc_name kind + (HsWB { hswb_cts = arg_pats, hswb_kvs = kvars, hswb_tvs = tvars }) kind_checker thing_inside - = do { -- A family instance must have exactly the same number of type - -- parameters as the family declaration. You can't write - -- type family F a :: * -> * - -- type instance F Int y = y - -- because then the type (F Int) would be like (\y.y) - ; let (fam_kvs, fam_body) = splitForAllTys (tyConKind fam_tc) - fam_arity = tyConArity fam_tc - length fam_kvs - ; checkTc (length arg_pats == fam_arity) $ - wrongNumberOfParmsErr fam_arity + = do { let (fam_kvs, fam_body) = splitForAllTys kind + + -- We wish to check that the pattern has the right number of arguments + -- in checkValidFamPats (in TcValidity), so we can do the check *after* + -- we're done with the knot. But, the splitKindFunTysN below will panic + -- if there are *too many* patterns. So, we do a preliminary check here. + -- Note that we don't have enough information at hand to do a full check, + -- as that requires the full declared arity of the family, which isn't + -- nearby. + ; let max_args = length (fst $ splitKindFunTys fam_body) + ; checkTc (length arg_pats <= max_args) $ + wrongNumberOfParmsErrTooMany max_args -- Instantiate with meta kind vars ; fam_arg_kinds <- mapM (const newMetaKindVar) fam_kvs ; loc <- getSrcSpanM ; let (arg_kinds, res_kind) - = splitKindFunTysN fam_arity $ + = splitKindFunTysN (length arg_pats) $ substKiWith fam_kvs fam_arg_kinds fam_body hs_tvs = HsQTvs { hsq_kvs = kvars , hsq_tvs = userHsTyVarBndrs loc tvars } @@ -888,7 +929,7 @@ tcFamTyPats fam_tc (HsWB { hswb_cts = arg_pats, hswb_kvs = kvars, hswb_tvs = tva -- See Note [Quantifying over family patterns] ; typats <- tcHsTyVarBndrs hs_tvs $ \ _ -> do { kind_checker res_kind - ; tcHsArgTys (quotes (ppr fam_tc)) arg_pats arg_kinds } + ; tcHsArgTys (quotes (ppr fam_tc_name)) arg_pats arg_kinds } ; let all_args = fam_arg_kinds ++ typats -- Find free variables (after zonking) and turn @@ -1214,7 +1255,7 @@ checkValidTyCl decl _ -> return () } checkValidFamDecl :: FamilyDecl Name -> TcM () -checkValidFamDecl (FamilyDecl { fdLName = lname, fdFlavour = flav }) +checkValidFamDecl (FamilyDecl { fdLName = lname, fdInfo = flav }) = checkValidDecl (hsep [ptext (sLit "In the"), ppr flav, ptext (sLit "declaration for"), quotes (ppr lname)]) lname @@ -1241,8 +1282,9 @@ checkValidTyCon tc | Just syn_rhs <- synTyConRhs_maybe tc = case syn_rhs of - SynFamilyTyCon {} -> return () - SynonymTyCon ty -> checkValidType syn_ctxt ty + ClosedSynFamilyTyCon ax -> checkValidClosedCoAxiom ax + OpenSynFamilyTyCon -> return () + SynonymTyCon ty -> checkValidType syn_ctxt ty | otherwise = do { -- Check the context on the data decl @@ -1306,6 +1348,23 @@ checkValidTyCon tc fty2 = dataConFieldType con2 label check_fields [] = panic "checkValidTyCon/check_fields []" +checkValidClosedCoAxiom :: CoAxiom Branched -> TcM () +checkValidClosedCoAxiom (CoAxiom { co_ax_branches = branches, co_ax_tc = tc }) + = tcAddClosedTypeFamilyDeclCtxt tc $ + do { brListFoldlM_ check_accessibility [] branches + ; void $ brListMapM (checkValidTyFamInst Nothing tc) branches } + where + check_accessibility :: [CoAxBranch] -- prev branches (in reverse order) + -> CoAxBranch -- cur branch + -> TcM [CoAxBranch] -- cur : prev + -- Check whether the branch is dominated by earlier + -- ones and hence is inaccessible + check_accessibility prev_branches cur_branch + = do { when (cur_branch `isDominatedBy` prev_branches) $ + setSrcSpan (coAxBranchSpan cur_branch) $ + addErrTc $ inaccessibleCoAxBranch tc cur_branch + ; return (cur_branch : prev_branches) } + checkFieldCompat :: Name -> DataCon -> DataCon -> TyVarSet -> Type -> Type -> Type -> Type -> TcM () checkFieldCompat fld con1 con2 tvs1 res1 res2 fty1 fty2 @@ -1705,10 +1764,7 @@ tcAddDefaultAssocDeclCtxt name thing_inside tcAddTyFamInstCtxt :: TyFamInstDecl Name -> TcM a -> TcM a tcAddTyFamInstCtxt decl - | [_] <- tfid_eqns decl = tcAddFamInstCtxt (ptext (sLit "type instance")) (tyFamInstDeclName decl) - | otherwise - = tcAddFamInstCtxt (ptext (sLit "type instance group")) (tyFamInstDeclName decl) tcAddDataFamInstCtxt :: DataFamInstDecl Name -> TcM a -> TcM a tcAddDataFamInstCtxt decl @@ -1723,6 +1779,13 @@ tcAddFamInstCtxt flavour tycon thing_inside <+> ptext (sLit "declaration for"), quotes (ppr tycon)] +tcAddClosedTypeFamilyDeclCtxt :: TyCon -> TcM a -> TcM a +tcAddClosedTypeFamilyDeclCtxt tc + = addErrCtxt ctxt + where + ctxt = ptext (sLit "In the equations for closed type family") <+> + quotes (ppr tc) + resultTypeMisMatch :: Name -> DataCon -> DataCon -> SDoc resultTypeMisMatch field_name con1 con2 = vcat [sep [ptext (sLit "Constructors") <+> ppr con1 <+> ptext (sLit "and") <+> ppr con2, @@ -1830,11 +1893,6 @@ emptyConDeclsErr tycon = sep [quotes (ppr tycon) <+> ptext (sLit "has no constructors"), nest 2 $ ptext (sLit "(-XEmptyDataDecls permits this)")] -wrongNumberOfParmsErr :: Arity -> SDoc -wrongNumberOfParmsErr exp_arity - = ptext (sLit "Number of parameters must match family declaration; expected") - <+> ppr exp_arity - wrongKindOfFamily :: TyCon -> SDoc wrongKindOfFamily family = ptext (sLit "Wrong category of family instance; declaration was for a") @@ -1844,10 +1902,20 @@ wrongKindOfFamily family | isAlgTyCon family = ptext (sLit "data type") | otherwise = pprPanic "wrongKindOfFamily" (ppr family) +wrongNumberOfParmsErrTooMany :: Arity -> SDoc +wrongNumberOfParmsErrTooMany max_args + = ptext (sLit "Number of parameters must match family declaration; expected no more than") + <+> ppr max_args + wrongNamesInInstGroup :: Name -> Name -> SDoc wrongNamesInInstGroup first cur - = ptext (sLit "Mismatched family names in instance group.") $$ + = ptext (sLit "Mismatched type names in closed type family declaration.") $$ ptext (sLit "First name was") <+> (ppr first) <> (ptext (sLit "; this one is")) <+> (ppr cur) +inaccessibleCoAxBranch :: TyCon -> CoAxBranch -> SDoc +inaccessibleCoAxBranch tc fi + = ptext (sLit "Inaccessible family instance equation:") $$ + (pprCoAxBranch tc fi) + \end{code} diff --git a/compiler/typecheck/TcValidity.lhs b/compiler/typecheck/TcValidity.lhs index 54377192f4..968d8695cc 100644 --- a/compiler/typecheck/TcValidity.lhs +++ b/compiler/typecheck/TcValidity.lhs @@ -45,6 +45,7 @@ import ListSetOps import SrcLoc import Outputable import FastString +import BasicTypes ( Arity ) import Control.Monad import Data.List ( (\\) ) @@ -1135,10 +1136,25 @@ checkValidFamPats :: TyCon -> [TyVar] -> [Type] -> TcM () -- e.g. we disallow (Trac #7536) -- type T a = Int -- type instance F (T a) = a +-- c) Have the right number of patterns checkValidFamPats fam_tc tvs ty_pats - = do { mapM_ checkTyFamFreeness ty_pats + = do { -- A family instance must have exactly the same number of type + -- parameters as the family declaration. You can't write + -- type family F a :: * -> * + -- type instance F Int y = y + -- because then the type (F Int) would be like (\y.y) + checkTc (length ty_pats == fam_arity) $ + wrongNumberOfParmsErr (fam_arity - length fam_kvs) -- report only types + ; mapM_ checkTyFamFreeness ty_pats ; let unbound_tvs = filterOut (`elemVarSet` exactTyVarsOfTypes ty_pats) tvs ; checkTc (null unbound_tvs) (famPatErr fam_tc unbound_tvs ty_pats) } + where fam_arity = tyConArity fam_tc + (fam_kvs, _) = splitForAllTys (tyConKind fam_tc) + +wrongNumberOfParmsErr :: Arity -> SDoc +wrongNumberOfParmsErr exp_arity + = ptext (sLit "Number of parameters must match family declaration; expected") + <+> ppr exp_arity -- Ensure that no type family instances occur in a type. -- diff --git a/compiler/types/CoAxiom.lhs b/compiler/types/CoAxiom.lhs index 365c65369f..7781d56356 100644 --- a/compiler/types/CoAxiom.lhs +++ b/compiler/types/CoAxiom.lhs @@ -4,7 +4,7 @@ \begin{code} -{-# LANGUAGE GADTs #-} +{-# LANGUAGE GADTs, ScopedTypeVariables #-} -- | Module for coercion axioms, used to represent type family instances -- and newtypes @@ -13,17 +13,18 @@ module CoAxiom ( Branched, Unbranched, BranchIndex, BranchList(..), toBranchList, fromBranchList, toBranchedList, toUnbranchedList, - brListLength, brListNth, brListMap, brListFoldr, - brListZipWith, brListIndices, + brListLength, brListNth, brListMap, brListFoldr, brListMapM, + brListFoldlM_, brListZipWith, CoAxiom(..), CoAxBranch(..), toBranchedAxiom, toUnbranchedAxiom, coAxiomName, coAxiomArity, coAxiomBranches, - coAxiomTyCon, isImplicitCoAxiom, + coAxiomTyCon, isImplicitCoAxiom, coAxiomNumPats, coAxiomNthBranch, coAxiomSingleBranch_maybe, coAxiomSingleBranch, coAxBranchTyVars, coAxBranchLHS, - coAxBranchRHS, coAxBranchSpan + coAxBranchRHS, coAxBranchSpan, coAxBranchIncomps, + placeHolderIncomps ) where import {-# SOURCE #-} TypeRep ( Type ) @@ -99,10 +100,10 @@ that code to deal with branched axioms, especially when the code can be sure of the fact that an axiom is indeed a singleton. At the same time, it seems dangerous to assume singlehood in various places through GHC. -The solution to this is to label a CoAxiom (and FamInst) with a phantom -type variable declaring whether it is known to be a singleton or not. The -list of branches is stored using a special form of list, declared below, -that ensures that the type variable is accurate. +The solution to this is to label a CoAxiom with a phantom type variable +declaring whether it is known to be a singleton or not. The list of branches +is stored using a special form of list, declared below, that ensures that the +type variable is accurate. As of this writing (Dec 2012), it would not be appropriate to use a promoted type as the phantom type, so we use empty datatypes. We wish to have GHC @@ -154,14 +155,6 @@ brListLength :: BranchList a br -> Int brListLength (FirstBranch _) = 1 brListLength (NextBranch _ t) = 1 + brListLength t --- Indices -brListIndices :: BranchList a br -> [BranchIndex] -brListIndices bs = go 0 bs - where - go :: BranchIndex -> BranchList a br -> [BranchIndex] - go n (NextBranch _ t) = n : go (n+1) t - go n (FirstBranch {}) = [n] - -- lookup brListNth :: BranchList a br -> BranchIndex -> a brListNth (FirstBranch b) 0 = b @@ -178,6 +171,21 @@ brListFoldr :: (a -> b -> b) -> b -> BranchList a br -> b brListFoldr f x (FirstBranch b) = f b x brListFoldr f x (NextBranch h t) = f h (brListFoldr f x t) +brListMapM :: Monad m => (a -> m b) -> BranchList a br -> m [b] +brListMapM f (FirstBranch b) = f b >>= \fb -> return [fb] +brListMapM f (NextBranch h t) = do { fh <- f h + ; ft <- brListMapM f t + ; return (fh : ft) } + +brListFoldlM_ :: forall a b m br. Monad m + => (a -> b -> m a) -> a -> BranchList b br -> m () +brListFoldlM_ f z brs = do { _ <- go z brs + ; return () } + where go :: forall br'. Monad m => a -> BranchList b br' -> m a + go acc (FirstBranch b) = f acc b + go acc (NextBranch h t) = do { fh <- f acc h + ; go fh t } + -- zipWith brListZipWith :: (a -> b -> c) -> BranchList a br1 -> BranchList b br2 -> [c] brListZipWith f (FirstBranch a) (FirstBranch b) = [f a b] @@ -197,6 +205,25 @@ instance Outputable a => Outputable (BranchList a br) where %* * %************************************************************************ +Note [Storing compatibility] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +During axiom application, we need to be aware of which branches are compatible +with which others. The full explanation is in Note [Compatibility] in +FamInstEnv. (The code is placed there to avoid a dependency from CoAxiom on +the unification algorithm.) Although we could theoretically compute +compatibility on the fly, this is silly, so we store it in a CoAxiom. + +Specifically, each branch refers to all other branches with which it is +incompatible. This list might well be empty, and it will always be for the +first branch of any axiom. + +CoAxBranches that do not (yet) belong to a CoAxiom should have a panic thunk +stored in cab_incomps. The incompatibilities are properly a property of the +axiom as a whole, and they are computed only when the final axiom is built. + +During serialization, the list is converted into a list of the indices +of the branches. + \begin{code} -- | A 'CoAxiom' is a \"coercion constructor\", i.e. a named equality axiom. @@ -217,12 +244,14 @@ data CoAxiom br data CoAxBranch = CoAxBranch - { cab_loc :: SrcSpan -- Location of the defining equation - -- See Note [CoAxiom locations] - , cab_tvs :: [TyVar] -- Bound type variables; not necessarily fresh - -- See Note [CoAxBranch type variables] - , cab_lhs :: [Type] -- Type patterns to match against - , cab_rhs :: Type -- Right-hand side of the equality + { cab_loc :: SrcSpan -- Location of the defining equation + -- See Note [CoAxiom locations] + , cab_tvs :: [TyVar] -- Bound type variables; not necessarily fresh + -- See Note [CoAxBranch type variables] + , cab_lhs :: [Type] -- Type patterns to match against + , cab_rhs :: Type -- Right-hand side of the equality + , cab_incomps :: [CoAxBranch] -- The previous incompatible branches + -- See Note [Storing compatibility] } deriving Typeable @@ -234,6 +263,9 @@ toUnbranchedAxiom :: CoAxiom br -> CoAxiom Unbranched toUnbranchedAxiom (CoAxiom unique name tc branches implicit) = CoAxiom unique name tc (toUnbranchedList branches) implicit +coAxiomNumPats :: CoAxiom br -> Int +coAxiomNumPats = length . coAxBranchLHS . (flip coAxiomNthBranch 0) + coAxiomNthBranch :: CoAxiom br -> BranchIndex -> CoAxBranch coAxiomNthBranch (CoAxiom { co_ax_branches = bs }) index = brListNth bs index @@ -276,6 +308,12 @@ coAxBranchSpan = cab_loc isImplicitCoAxiom :: CoAxiom br -> Bool isImplicitCoAxiom = co_ax_implicit +coAxBranchIncomps :: CoAxBranch -> [CoAxBranch] +coAxBranchIncomps = cab_incomps + +placeHolderIncomps :: [CoAxBranch] +placeHolderIncomps = panic "placeHolderIncomps" + \end{code} Note [CoAxBranch type variables] diff --git a/compiler/types/Coercion.lhs b/compiler/types/Coercion.lhs index f30f11dce3..e1dec49380 100644 --- a/compiler/types/Coercion.lhs +++ b/compiler/types/Coercion.lhs @@ -15,9 +15,6 @@ -- more on System FC and how coercions fit into it. -- module Coercion ( - -- * CoAxioms - mkCoAxBranch, mkBranchedCoAxiom, mkSingleCoAxiom, - -- * Main data type Coercion(..), Var, CoVar, LeftOrRight(..), pickLR, @@ -112,58 +109,6 @@ import FastString import qualified Data.Data as Data hiding ( TyCon ) \end{code} - -%************************************************************************ -%* * - Constructing axioms - These functions are here because tidyType etc - are not available in CoAxiom -%* * -%************************************************************************ - -Note [Tidy axioms when we build them] -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -We print out axioms and don't want to print stuff like - F k k a b = ... -Instead we must tidy those kind variables. See Trac #7524. - - -\begin{code} -mkCoAxBranch :: [TyVar] -- original, possibly stale, tyvars - -> [Type] -- LHS patterns - -> Type -- RHS - -> SrcSpan - -> CoAxBranch -mkCoAxBranch tvs lhs rhs loc - = CoAxBranch { cab_tvs = tvs1 - , cab_lhs = tidyTypes env lhs - , cab_rhs = tidyType env rhs - , cab_loc = loc } - where - (env, tvs1) = tidyTyVarBndrs emptyTidyEnv tvs - -- See Note [Tidy axioms when we build them] - - -mkBranchedCoAxiom :: Name -> TyCon -> [CoAxBranch] -> CoAxiom Branched -mkBranchedCoAxiom ax_name fam_tc branches - = CoAxiom { co_ax_unique = nameUnique ax_name - , co_ax_name = ax_name - , co_ax_tc = fam_tc - , co_ax_implicit = False - , co_ax_branches = toBranchList branches } - -mkSingleCoAxiom :: Name -> [TyVar] -> TyCon -> [Type] -> Type -> CoAxiom Unbranched -mkSingleCoAxiom ax_name tvs fam_tc lhs_tys rhs_ty - = CoAxiom { co_ax_unique = nameUnique ax_name - , co_ax_name = ax_name - , co_ax_tc = fam_tc - , co_ax_implicit = False - , co_ax_branches = FirstBranch branch } - where - branch = mkCoAxBranch tvs lhs_tys rhs_ty (getSrcSpan ax_name) -\end{code} - - %************************************************************************ %* * Coercions @@ -673,7 +618,7 @@ mkCoVarCo cv mkReflCo :: Type -> Coercion mkReflCo = Refl -mkAxInstCo :: CoAxiom br -> Int -> [Type] -> Coercion +mkAxInstCo :: CoAxiom br -> BranchIndex -> [Type] -> Coercion -- mkAxInstCo can legitimately be called over-staturated; -- i.e. with more type arguments than the coercion requires mkAxInstCo ax index tys @@ -823,7 +768,8 @@ mkNewTypeCo name tycon tvs rhs_ty where branch = CoAxBranch { cab_loc = getSrcSpan name , cab_tvs = tvs , cab_lhs = mkTyVarTys tvs - , cab_rhs = rhs_ty } + , cab_rhs = rhs_ty + , cab_incomps = [] } mkPiCos :: [Var] -> Coercion -> Coercion mkPiCos vs co = foldr mkPiCo co vs diff --git a/compiler/types/FamInstEnv.lhs b/compiler/types/FamInstEnv.lhs index cc51568a33..85ad7f4e19 100644 --- a/compiler/types/FamInstEnv.lhs +++ b/compiler/types/FamInstEnv.lhs @@ -5,59 +5,58 @@ FamInstEnv: Type checked family instance declarations \begin{code} -module FamInstEnv ( - Branched, Unbranched, - FamInst(..), FamFlavor(..), FamInstBranch(..), +{-# LANGUAGE GADTs #-} + +module FamInstEnv ( + FamInst(..), FamFlavor(..), famInstAxiom, famInstTyCon, famInstRHS, + famInstsRepTyCons, famInstRepTyCon_maybe, dataFamInstRepTyCon, + pprFamInst, pprFamInstHdr, pprFamInsts, + mkImportedFamInst, - famInstAxiom, famInstBranchRoughMatch, - famInstsRepTyCons, famInstNthBranch, famInstSingleBranch, - famInstBranchLHS, famInstBranches, - toBranchedFamInst, toUnbranchedFamInst, - famInstTyCon, famInstRepTyCon_maybe, dataFamInstRepTyCon, - pprFamInst, pprFamInsts, - pprFamFlavor, - mkImportedFamInst, + FamInstEnvs, FamInstEnv, emptyFamInstEnv, emptyFamInstEnvs, + extendFamInstEnv, deleteFromFamInstEnv, extendFamInstEnvList, + identicalFamInst, famInstEnvElts, familyInstances, orphNamesOfFamInst, - FamInstEnv, FamInstEnvs, - emptyFamInstEnvs, emptyFamInstEnv, famInstEnvElts, familyInstances, - extendFamInstEnvList, extendFamInstEnv, deleteFromFamInstEnv, - identicalFamInst, orphNamesOfFamInst, + -- * CoAxioms + mkCoAxBranch, mkBranchedCoAxiom, mkUnbranchedCoAxiom, mkSingleCoAxiom, + computeAxiomIncomps, FamInstMatch(..), - lookupFamInstEnv, lookupFamInstEnvConflicts, lookupFamInstEnvConflicts', - - isDominatedBy, + lookupFamInstEnv, lookupFamInstEnvConflicts, + isDominatedBy, + -- Normalisation - topNormaliseType, normaliseType, normaliseTcApp + chooseBranch, topNormaliseType, normaliseType, normaliseTcApp ) where #include "HsVersions.h" -import TcType ( orphNamesOfTypes ) import InstEnv import Unify import Type -import Coercion hiding ( substTy ) +import TcType ( orphNamesOfTypes ) import TypeRep import TyCon +import Coercion import CoAxiom import VarSet import VarEnv import Name -import NameSet import UniqFM import Outputable import Maybes import Util +import Pair +import SrcLoc +import NameSet import FastString \end{code} - %************************************************************************ %* * - Type checked family instance heads + Type checked family instance heads %* * %************************************************************************ @@ -69,80 +68,40 @@ Note [FamInsts and CoAxioms] * A CoAxiom is a System-FC thing: it can relate any two types * A FamInst is a Haskell source-language thing, corresponding - to a type/data family instance declaration. + to a type/data family instance declaration. - The FamInst contains a CoAxiom, which is the evidence for the instance - - The LHSs of the CoAxiom branches are always of form - F ty1 .. tyn where F is a type family - -* A FamInstBranch corresponds to a CoAxBranch -- it represents - one alternative in a branched family instance. We could theoretically - not have FamInstBranches and just use the CoAxBranches within - the CoAxiom stored in the FamInst, but for one problem: we want to - cache the "rough match" top-level tycon names for quick matching. - This data is not stored in a CoAxBranch, so we use FamInstBranches - instead. - -Note [fi_branched field] -~~~~~~~~~~~~~~~~~~~~~~~~ -A FamInst stores whether or not it was declared with "type instance where" -for two reasons: - 1. for accurate pretty-printing; and - 2. because confluent overlap is disallowed between branches - declared in groups. -Note that this "branched-ness" is properly associated with the FamInst, -which thinks about overlap, and not in the CoAxiom, which blindly -assumes that it is part of a consistent axiom set. - -A "branched" instance with fi_branched=True can have just one branch, however. - -Note [Why we need fib_rhs] -~~~~~~~~~~~~~~~~~~~~~~~~~~ -It may at first seem unnecessary to store the right-hand side of an equation -in a FamInstBranch. After all, FamInstBranches are used only for matching a -family application; the underlying CoAxiom is used to perform the actual -simplification. - -However, we do need to know the rhs field during conflict checking to support -confluent overlap. When two unbranched instances have overlapping left-hand -sides, we check if the right-hand sides are coincident in the region of overlap. -This check requires fib_rhs. See lookupFamInstEnvConflicts. + - The LHS of the CoAxiom is always of form F ty1 .. tyn + where F is a type family \begin{code} -data FamInst br -- See Note [FamInsts and CoAxioms], Note [Branched axioms] in CoAxiom - = FamInst { fi_axiom :: CoAxiom br -- The new coercion axiom introduced - -- by this family instance - , fi_flavor :: FamFlavor - , fi_branched :: Bool -- True <=> declared with "type instance where" - -- See Note [fi_branched field] - - -- Everything below here is a redundant, - -- cached version of the two things above, - -- except that the TyVars are freshened in the FamInstBranches - , fi_branches :: BranchList FamInstBranch br - -- Haskell-source-language view of - -- a CoAxBranch - , fi_fam :: Name -- Family name - -- INVARIANT: fi_fam = name of fi_axiom.co_ax_tc - } - -data FamInstBranch - = FamInstBranch - { fib_tvs :: [TyVar] -- Bound type variables +data FamInst -- See Note [FamInsts and CoAxioms] + = FamInst { fi_axiom :: CoAxiom Unbranched -- The new coercion axiom introduced + -- by this family instance + , fi_flavor :: FamFlavor + + -- Everything below here is a redundant, + -- cached version of the two things above + -- except that the TyVars are freshened + , fi_fam :: Name -- Family name + + -- Used for "rough matching"; same idea as for class instances + -- See Note [Rough-match field] in InstEnv + , fi_tcs :: [Maybe Name] -- Top of type args + -- INVARIANT: fi_tcs = roughMatchTcs fi_tys + + -- Used for "proper matching"; ditto + , fi_tvs :: [TyVar] -- Template tyvars for full match -- Like ClsInsts, these variables are always -- fresh. See Note [Template tyvars are fresh] -- in InstEnv - , fib_lhs :: [Type] -- Type patterns - - , fib_rhs :: Type -- RHS of family instance - -- See Note [Why we need fib_rhs] + , fi_tys :: [Type] -- and its arg types + -- INVARIANT: fi_tvs = coAxiomTyVars fi_axiom - , fib_tcs :: [Maybe Name] -- Used for "rough matching" during typechecking - -- In 1-1 correspondence with fib_lhs - -- see Note [Rough-match field] in InstEnv - } + , fi_rhs :: Type -- the RHS, with its freshened vars + } data FamFlavor = SynFamilyInst -- A synonym family @@ -152,50 +111,35 @@ data FamFlavor \begin{code} -- Obtain the axiom of a family instance -famInstAxiom :: FamInst br -> CoAxiom br +famInstAxiom :: FamInst -> CoAxiom Unbranched famInstAxiom = fi_axiom -famInstTyCon :: FamInst br -> TyCon -famInstTyCon = co_ax_tc . fi_axiom - -famInstNthBranch :: FamInst br -> Int -> FamInstBranch -famInstNthBranch (FamInst { fi_branches = branches }) index - = ASSERT( 0 <= index && index < (length $ fromBranchList branches) ) - brListNth branches index +-- Split the left-hand side of the FamInst +famInstSplitLHS :: FamInst -> (TyCon, [Type]) +famInstSplitLHS (FamInst { fi_axiom = axiom, fi_tys = lhs }) + = (coAxiomTyCon axiom, lhs) -famInstSingleBranch :: FamInst Unbranched -> FamInstBranch -famInstSingleBranch (FamInst { fi_branches = FirstBranch branch }) = branch +-- Get the RHS of the FamInst +famInstRHS :: FamInst -> Type +famInstRHS = fi_rhs -toBranchedFamInst :: FamInst br -> FamInst Branched -toBranchedFamInst (FamInst ax flav grp branches fam) - = FamInst (toBranchedAxiom ax) flav grp (toBranchedList branches) fam - -toUnbranchedFamInst :: FamInst br -> FamInst Unbranched -toUnbranchedFamInst (FamInst ax flav grp branches fam) - = FamInst (toUnbranchedAxiom ax) flav grp (toUnbranchedList branches) fam - -famInstBranches :: FamInst br -> BranchList FamInstBranch br -famInstBranches = fi_branches - -famInstBranchLHS :: FamInstBranch -> [Type] -famInstBranchLHS = fib_lhs - -famInstBranchRoughMatch :: FamInstBranch -> [Maybe Name] -famInstBranchRoughMatch = fib_tcs +-- Get the family TyCon of the FamInst +famInstTyCon :: FamInst -> TyCon +famInstTyCon = coAxiomTyCon . famInstAxiom -- Return the representation TyCons introduced by data family instances, if any -famInstsRepTyCons :: [FamInst br] -> [TyCon] +famInstsRepTyCons :: [FamInst] -> [TyCon] famInstsRepTyCons fis = [tc | FamInst { fi_flavor = DataFamilyInst tc } <- fis] -- Extracts the TyCon for this *data* (or newtype) instance -famInstRepTyCon_maybe :: FamInst br -> Maybe TyCon -famInstRepTyCon_maybe fi +famInstRepTyCon_maybe :: FamInst -> Maybe TyCon +famInstRepTyCon_maybe fi = case fi_flavor fi of DataFamilyInst tycon -> Just tycon SynFamilyInst -> Nothing -dataFamInstRepTyCon :: FamInst br -> TyCon -dataFamInstRepTyCon fi +dataFamInstRepTyCon :: FamInst -> TyCon +dataFamInstRepTyCon fi = case fi_flavor fi of DataFamilyInst tycon -> tycon SynFamilyInst -> pprPanic "dataFamInstRepTyCon" (ppr fi) @@ -208,44 +152,46 @@ dataFamInstRepTyCon fi %************************************************************************ \begin{code} -instance NamedThing (FamInst br) where +instance NamedThing FamInst where getName = coAxiomName . fi_axiom -instance Outputable (FamInst br) where +instance Outputable FamInst where ppr = pprFamInst -- Prints the FamInst as a family instance declaration -pprFamInst :: FamInst br -> SDoc -pprFamInst (FamInst { fi_branches = brs, fi_flavor = SynFamilyInst - , fi_branched = True, fi_axiom = axiom }) - = hang (ptext (sLit "type instance where")) - 2 (vcat [pprCoAxBranchHdr axiom i | i <- brListIndices brs]) - -pprFamInst fi@(FamInst { fi_flavor = flavor - , fi_branched = False, fi_axiom = ax }) - = pprFamFlavor flavor <+> pp_instance - <+> pprCoAxBranchHdr ax 0 +pprFamInst :: FamInst -> SDoc +pprFamInst famInst + = hang (pprFamInstHdr famInst) + 2 (vcat [ ifPprDebug (ptext (sLit "Coercion axiom:") <+> ppr ax) + , ifPprDebug (ptext (sLit "RHS:") <+> ppr (famInstRHS famInst)) + , ptext (sLit "--") <+> pprDefinedAt (getName famInst)]) where + ax = fi_axiom famInst + +pprFamInstHdr :: FamInst -> SDoc +pprFamInstHdr fi@(FamInst {fi_flavor = flavor}) + = pprTyConSort <+> pp_instance <+> pprHead + where + (fam_tc, tys) = famInstSplitLHS fi + -- For *associated* types, say "type T Int = blah" -- For *top level* type instances, say "type instance T Int = blah" pp_instance - | isTyConAssoc (famInstTyCon fi) = empty - | otherwise = ptext (sLit "instance") - -pprFamInst _ = panic "pprFamInst" - -pprFamFlavor :: FamFlavor -> SDoc -pprFamFlavor flavor - = case flavor of - SynFamilyInst -> ptext (sLit "type") - DataFamilyInst tycon - | isDataTyCon tycon -> ptext (sLit "data") - | isNewTyCon tycon -> ptext (sLit "newtype") - | isAbstractTyCon tycon -> ptext (sLit "data") - | otherwise -> ptext (sLit "WEIRD") <+> ppr tycon - -pprFamInsts :: [FamInst br] -> SDoc + | isTyConAssoc fam_tc = empty + | otherwise = ptext (sLit "instance") + + pprHead = pprTypeApp fam_tc tys + pprTyConSort = case flavor of + SynFamilyInst -> ptext (sLit "type") + DataFamilyInst tycon + | isDataTyCon tycon -> ptext (sLit "data") + | isNewTyCon tycon -> ptext (sLit "newtype") + | isAbstractTyCon tycon -> ptext (sLit "data") + | otherwise -> ptext (sLit "WEIRD") <+> ppr tycon + +pprFamInsts :: [FamInst] -> SDoc pprFamInsts finsts = vcat (map pprFamInst finsts) + \end{code} Note [Lazy axiom match] @@ -264,55 +210,39 @@ not in the parameter list) and we assert the consistency of names there also. \begin{code} - -- Make a family instance representation from the information found in an -- interface file. In particular, we get the rough match info from the iface -- (instead of computing it here). mkImportedFamInst :: Name -- Name of the family - -> Bool -- is this a branched instance? - -> [[Maybe Name]] -- Rough match info, per branch - -> CoAxiom Branched -- Axiom introduced - -> FamInst Branched -- Resulting family instance -mkImportedFamInst fam branched roughs axiom + -> [Maybe Name] -- Rough match info + -> CoAxiom Unbranched -- Axiom introduced + -> FamInst -- Resulting family instance +mkImportedFamInst fam mb_tcs axiom = FamInst { - fi_fam = fam, - fi_axiom = axiom, - fi_flavor = flavor, - fi_branched = branched, - fi_branches = branches } - where - -- Lazy match (See note [Lazy axiom match]) - CoAxiom { co_ax_branches = axBranches } - = ASSERT( fam == tyConName (coAxiomTyCon axiom) ) - axiom - - branches = toBranchList $ map mk_imp_fam_inst_branch $ - (roughs `zipLazy` fromBranchList axBranches) - -- Lazy zip (See note [Lazy axiom match]) - - mk_imp_fam_inst_branch (mb_tcs, ~(CoAxBranch { cab_tvs = tvs - , cab_lhs = lhs - , cab_rhs = rhs })) - -- Lazy match (See note [Lazy axiom match]) - = FamInstBranch { fib_tvs = tvs - , fib_lhs = lhs - , fib_rhs = rhs - , fib_tcs = mb_tcs } + fi_fam = fam, + fi_tcs = mb_tcs, + fi_tvs = tvs, + fi_tys = tys, + fi_rhs = rhs, + fi_axiom = axiom, + fi_flavor = flavor } + where + -- See Note [Lazy axiom match] + ~(CoAxiom { co_ax_branches = + ~(FirstBranch ~(CoAxBranch { cab_lhs = tys + , cab_tvs = tvs + , cab_rhs = rhs })) }) = axiom -- Derive the flavor for an imported FamInst rather disgustingly -- Maybe we should store it in the IfaceFamInst? - flavor - | FirstBranch (CoAxBranch { cab_rhs = rhs }) <- axBranches - , Just (tc, _) <- splitTyConApp_maybe rhs - , Just ax' <- tyConFamilyCoercion_maybe tc - , (toBranchedAxiom ax') == axiom - = DataFamilyInst tc - - | otherwise - = SynFamilyInst + flavor = case splitTyConApp_maybe rhs of + Just (tc, _) + | Just ax' <- tyConFamilyCoercion_maybe tc + , ax' == axiom + -> DataFamilyInst tc + _ -> SynFamilyInst \end{code} - %************************************************************************ %* * FamInstEnv @@ -335,7 +265,7 @@ Neverthless it is still useful to have data families in the FamInstEnv: - For finding the representation type...see FamInstEnv.topNormaliseType and its call site in Simplify - - In standalone deriving instance Eq (T [Int]) we need to find the + - In standalone deriving instance Eq (T [Int]) we need to find the representation type for T [Int] Note [Varying number of patterns for data family axioms] @@ -365,7 +295,7 @@ type FamInstEnvs = (FamInstEnv, FamInstEnv) -- External package inst-env, Home-package inst-env newtype FamilyInstEnv - = FamIE [FamInst Branched] -- The instances for a particular family, in any order + = FamIE [FamInst] -- The instances for a particular family, in any order instance Outputable FamilyInstEnv where ppr (FamIE fs) = ptext (sLit "FamIE") <+> vcat (map ppr fs) @@ -380,16 +310,16 @@ emptyFamInstEnvs = (emptyFamInstEnv, emptyFamInstEnv) emptyFamInstEnv :: FamInstEnv emptyFamInstEnv = emptyUFM -famInstEnvElts :: FamInstEnv -> [FamInst Branched] +famInstEnvElts :: FamInstEnv -> [FamInst] famInstEnvElts fi = [elt | FamIE elts <- eltsUFM fi, elt <- elts] -familyInstances :: (FamInstEnv, FamInstEnv) -> TyCon -> [FamInst Branched] +familyInstances :: (FamInstEnv, FamInstEnv) -> TyCon -> [FamInst] familyInstances (pkg_fie, home_fie) fam = get home_fie ++ get pkg_fie where get env = case lookupUFM env fam of Just (FamIE insts) -> insts - Nothing -> [] + Nothing -> [] -- | Collects the names of the concrete types and type constructors that -- make up the LHS of a type family instance. For instance, @@ -398,28 +328,28 @@ familyInstances (pkg_fie, home_fie) fam -- `type instance Foo (F (G (H a))) b = ...` would yield [F,G,H] -- -- Used in the implementation of ":info" in GHCi. -orphNamesOfFamInst :: FamInst Branched -> NameSet +orphNamesOfFamInst :: FamInst -> NameSet orphNamesOfFamInst = orphNamesOfTypes . concat . brListMap cab_lhs . coAxiomBranches . fi_axiom -extendFamInstEnvList :: FamInstEnv -> [FamInst br] -> FamInstEnv +extendFamInstEnvList :: FamInstEnv -> [FamInst] -> FamInstEnv extendFamInstEnvList inst_env fis = foldl extendFamInstEnv inst_env fis -extendFamInstEnv :: FamInstEnv -> FamInst br -> FamInstEnv +extendFamInstEnv :: FamInstEnv -> FamInst -> FamInstEnv extendFamInstEnv inst_env ins_item@(FamInst {fi_fam = cls_nm}) - = addToUFM_C add inst_env cls_nm (FamIE [ins_item_br]) + = addToUFM_C add inst_env cls_nm (FamIE [ins_item]) where - ins_item_br = toBranchedFamInst ins_item - add (FamIE items) _ = FamIE (ins_item_br:items) + add (FamIE items) _ = FamIE (ins_item:items) -deleteFromFamInstEnv :: FamInstEnv -> FamInst br -> FamInstEnv +deleteFromFamInstEnv :: FamInstEnv -> FamInst -> FamInstEnv deleteFromFamInstEnv inst_env fam_inst@(FamInst {fi_fam = fam_nm}) = adjustUFM adjust inst_env fam_nm where adjust :: FamilyInstEnv -> FamilyInstEnv - adjust (FamIE items) = FamIE (filterOut (identicalFamInst fam_inst) items) + adjust (FamIE items) + = FamIE (filterOut (identicalFamInst fam_inst) items) -identicalFamInst :: FamInst br1 -> FamInst br2 -> Bool +identicalFamInst :: FamInst -> FamInst -> Bool -- Same LHS, *and* the instance is defined in the same module -- Used for overriding in GHCi identicalFamInst (FamInst { fi_axiom = ax1 }) (FamInst { fi_axiom = ax2 }) @@ -439,38 +369,26 @@ identicalFamInst (FamInst { fi_axiom = ax1 }) (FamInst { fi_axiom = ax2 }) lhs1 = coAxBranchLHS br1 lhs2 = coAxBranchLHS br2 rn_env = rnBndrs2 (mkRnEnv2 emptyInScopeSet) tvs1 tvs2 - + \end{code} %************************************************************************ %* * - Looking up a family instance + Compatibility %* * %************************************************************************ -@lookupFamInstEnv@ looks up in a @FamInstEnv@, using a one-way match. -Multiple matches are only possible in case of type families (not data -families), and then, it doesn't matter which match we choose (as the -instances are guaranteed confluent). +Note [Compatibility] +~~~~~~~~~~~~~~~~~~~~ +Two patterns are /compatible/ if either of the following conditions hold: +1) The patterns are apart. +2) The patterns unify with a substitution S, and their right hand sides +equal under that substitution. -We return the matching family instances and the type instance at which it -matches. For example, if we lookup 'T [Int]' and have a family instance - - data instance T [a] = .. - -desugared to - - data :R42T a = .. - coe :Co:R42T a :: T [a] ~ :R42T a - -we return the matching instance '(FamInst{.., fi_tycon = :R42T}, Int)'. - -Note [Branched instance checking] -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +For open type families, only compatible instances are allowed. For closed +type families, the story is slightly more complicated. Consider the following: -Consider the following: - -type instance where +type family F a where F Int = Bool F a = Int @@ -481,8 +399,8 @@ Should that type-check? No. We need to allow for the possibility that 'a' might be Int and therefore 'F a' should be Bool. We can simplify 'F a' to Int only when we can be sure that 'a' is not Int. -To achieve this, after finding a possible match within an instance, we have to -go back to all previous FamInstBranchess and check that, under the +To achieve this, after finding a possible match within the equations, we have to +go back to all previous equations and check that, under the substitution induced by the match, other branches are surely apart. (See [Apartness] in types/Unify.lhs.) This is similar to what happens with class instance selection, when we need to guarantee that there is only a match and @@ -502,70 +420,148 @@ type family H y Now, we want to simplify (G (H Char)). We can't, because (H Char) might later simplify to be Int. So, (G (H Char)) is stuck, for now. -ALTERNATE APPROACH: As we are processing the branches, we could check if a -branch is not surely apart from an application but does not match that -application. If this happens, there is no possible match and we can fail right -away. This might be more efficient. +While everything above is quite sound, it isn't as expressive as we'd like. +Consider this: -Note [Early failure optimisation for branched instances] -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -As we're searching through the instances for a match, it is possible that we -find a branch within an instance that matches, but a previous branch is not -surely apart from the target application. In this case, we can abort the -search, because any other instance that matches will necessarily overlap with -the instance we're currently searching. Because overlap among branched -instances is disallowed, we know that that no such other instance exists. - -Note [Confluence checking within branched instances] -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -GHC allows type family instances to have overlapping patterns as long as the -right-hand sides are coincident in the region of overlap. Can we extend this -notion of confluent overlap to branched instances? Not in any obvious way. +type family J a where + J Int = Int + J a = a -Consider this: +Can we simplify (J b) to b? Sure we can. Yes, the first equation matches if +b is instantiated with Int, but the RHSs coincide there, so it's all OK. -type instance where - F Int = Int - F a = a - -Without confluence checking (in other words, as implemented), we cannot now -simplify an application of (F b) -- b might unify with Int later on, so this -application is stuck. However, it would seem easy to just check that, in the -region of overlap, (i.e. b |-> Int), the right-hand sides coincide, so we're -OK. The problem happens when we are simplifying an application (F (G a)), -where (G a) is stuck. What, now, is the region of overlap? We can't soundly -simplify (F (G a)) without knowing that the right-hand sides are confluent -in the region of overlap, but we also can't in any obvious way identify the -region of overlap. We don't want to do analysis on the instances of G, because -that is not sound in a world with open type families. (If G were known to be -closed, there might be a way forward here.) To find the region of overlap, -it is conceivable that we might convert (G a) to some fresh type variable and -then unify, but we must be careful to convert every (G a) to the same fresh -type variable. And then, what if there is an (H a) lying around? It all seems -rather subtle, error-prone, confusing, and probably won't help anyone. So, -we're not doing it. - -So, why is this not a problem with non-branched confluent overlap? Because -we don't need to verify that an application is apart from anything. The -non-branched confluent overlap check happens when we add the instance to the -environment -- we're unifying among patterns, which cannot contain type family -applications. So, we're safe there and can continue supporting that feature. +So, the rule is this: when looking up a branch in a closed type family, we +find a branch that matches the target, but then we make sure that the target +is apart from every previous *incompatible* branch. We don't check the +branches that are compatible with the matching branch, because they are eithe +irrelevant (clause 1 of compatible) or benign (clause 2 of compatible). + +\begin{code} + +compatibleBranches :: CoAxBranch -> CoAxBranch -> Bool +compatibleBranches (CoAxBranch { cab_lhs = lhs1, cab_rhs = rhs1 }) + (CoAxBranch { cab_lhs = lhs2, cab_rhs = rhs2 }) + = case tcApartTys instanceBindFun lhs1 lhs2 of + SurelyApart -> True + Unifiable subst + | Type.substTy subst rhs1 `eqType` Type.substTy subst rhs2 + -> True + _ -> False + +-- takes a CoAxiom with unknown branch incompatibilities and computes +-- the compatibilities +computeAxiomIncomps :: CoAxiom br -> CoAxiom br +computeAxiomIncomps ax@(CoAxiom { co_ax_branches = branches }) + = ax { co_ax_branches = go [] branches } + where + go :: [CoAxBranch] -> BranchList CoAxBranch br -> BranchList CoAxBranch br + go prev_branches (FirstBranch br) + = FirstBranch (br { cab_incomps = mk_incomps br prev_branches }) + go prev_branches (NextBranch br tail) + = let br' = br { cab_incomps = mk_incomps br prev_branches } in + NextBranch br' (go (br' : prev_branches) tail) + + mk_incomps :: CoAxBranch -> [CoAxBranch] -> [CoAxBranch] + mk_incomps br = filter (not . compatibleBranches br) + +\end{code} + +%************************************************************************ +%* * + Constructing axioms + These functions are here because tidyType / tcApartTys + are not available in CoAxiom +%* * +%************************************************************************ + +Note [Tidy axioms when we build them] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +We print out axioms and don't want to print stuff like + F k k a b = ... +Instead we must tidy those kind variables. See Trac #7524. + +\begin{code} +mkCoAxBranch :: [TyVar] -- original, possibly stale, tyvars + -> [Type] -- LHS patterns + -> Type -- RHS + -> SrcSpan + -> CoAxBranch +mkCoAxBranch tvs lhs rhs loc + = CoAxBranch { cab_tvs = tvs1 + , cab_lhs = tidyTypes env lhs + , cab_rhs = tidyType env rhs + , cab_loc = loc + , cab_incomps = placeHolderIncomps } + where + (env, tvs1) = tidyTyVarBndrs emptyTidyEnv tvs + -- See Note [Tidy axioms when we build them] + +-- all of the following code is here to avoid mutual dependencies with +-- Coercion +mkBranchedCoAxiom :: Name -> TyCon -> [CoAxBranch] -> CoAxiom Branched +mkBranchedCoAxiom ax_name fam_tc branches + = computeAxiomIncomps $ + CoAxiom { co_ax_unique = nameUnique ax_name + , co_ax_name = ax_name + , co_ax_tc = fam_tc + , co_ax_implicit = False + , co_ax_branches = toBranchList branches } + +mkUnbranchedCoAxiom :: Name -> TyCon -> CoAxBranch -> CoAxiom Unbranched +mkUnbranchedCoAxiom ax_name fam_tc branch + = CoAxiom { co_ax_unique = nameUnique ax_name + , co_ax_name = ax_name + , co_ax_tc = fam_tc + , co_ax_implicit = False + , co_ax_branches = FirstBranch (branch { cab_incomps = [] }) } + +mkSingleCoAxiom :: Name -> [TyVar] -> TyCon -> [Type] -> Type -> CoAxiom Unbranched +mkSingleCoAxiom ax_name tvs fam_tc lhs_tys rhs_ty + = CoAxiom { co_ax_unique = nameUnique ax_name + , co_ax_name = ax_name + , co_ax_tc = fam_tc + , co_ax_implicit = False + , co_ax_branches = FirstBranch (branch { cab_incomps = [] }) } + where + branch = mkCoAxBranch tvs lhs_tys rhs_ty (getSrcSpan ax_name) +\end{code} + +%************************************************************************ +%* * + Looking up a family instance +%* * +%************************************************************************ + +@lookupFamInstEnv@ looks up in a @FamInstEnv@, using a one-way match. +Multiple matches are only possible in case of type families (not data +families), and then, it doesn't matter which match we choose (as the +instances are guaranteed confluent). + +We return the matching family instances and the type instance at which it +matches. For example, if we lookup 'T [Int]' and have a family instance + + data instance T [a] = .. + +desugared to + + data :R42T a = .. + coe :Co:R42T a :: T [a] ~ :R42T a + +we return the matching instance '(FamInst{.., fi_tycon = :R42T}, Int)'. \begin{code} + -- when matching a type family application, we get a FamInst, --- a 0-based index of the branch that matched, and the list of types --- the axiom should be applied to -data FamInstMatch = FamInstMatch { fim_instance :: FamInst Branched - , fim_index :: BranchIndex +-- and the list of types the axiom should be applied to +data FamInstMatch = FamInstMatch { fim_instance :: FamInst , fim_tys :: [Type] } + -- See Note [Over-saturated matches] instance Outputable FamInstMatch where ppr (FamInstMatch { fim_instance = inst - , fim_index = ind , fim_tys = tys }) - = ptext (sLit "match with") <+> parens (ppr inst) - <> brackets (ppr ind) <+> ppr tys + = ptext (sLit "match with") <+> parens (ppr inst) <+> ppr tys lookupFamInstEnv :: FamInstEnvs @@ -574,48 +570,14 @@ lookupFamInstEnv -- Precondition: the tycon is saturated (or over-saturated) lookupFamInstEnv - = lookup_fam_inst_env match True - where - match :: MatchFun - match seen (FamInstBranch { fib_tvs = tpl_tvs - , fib_lhs = tpl_tys }) - _ match_tys - = ASSERT( tyVarsOfTypes match_tys `disjointVarSet` tpl_tv_set ) - -- Unification will break badly if the variables overlap - -- They shouldn't because we allocate separate uniques for them - case tcMatchTys tpl_tv_set tpl_tys match_tys of - -- success - Just subst - | checkConflict seen match_tys - -> (Nothing, StopSearching) -- we found an incoherence, so stop searching - -- see Note [Early failure optimisation for branched instances] - - | otherwise - -> (Just subst, KeepSearching) - - -- failure; instance not relevant - Nothing -> (Nothing, KeepSearching) - where - tpl_tv_set = mkVarSet tpl_tvs - - -- see Note [Branched instance checking] - checkConflict :: [FamInstBranch] -- the previous branches in the instance that matched - -> [Type] -- the types in the tyfam application we are matching - -> Bool -- is there a conflict? - checkConflict [] _ = False - checkConflict ((FamInstBranch { fib_lhs = tpl_tys }) : rest) match_tys - -- see Note [Confluence checking within branched instances] - | SurelyApart <- tcApartTys instanceBindFun tpl_tys match_tys - = checkConflict rest match_tys - | otherwise - = True + = lookup_fam_inst_env match + where + match _ tpl_tvs tpl_tys tys = tcMatchTys tpl_tvs tpl_tys tys lookupFamInstEnvConflicts :: FamInstEnvs - -> Bool -- True <=> we are checking part of a group with other branches - -> TyCon -- The TyCon of the family - -> FamInstBranch -- the putative new instance branch - -> [FamInstMatch] -- Conflicting branches + -> FamInst -- Putative new instance + -> [FamInstMatch] -- Conflicting matches (don't look at the fim_tys field) -- E.g. when we are about to add -- f : type instance F [a] = a->a -- we do (lookupFamInstConflicts f [b]) @@ -623,67 +585,26 @@ lookupFamInstEnvConflicts -- -- Precondition: the tycon is saturated (or over-saturated) -lookupFamInstEnvConflicts envs grp tc - (FamInstBranch { fib_lhs = tys, fib_rhs = rhs }) - = lookup_fam_inst_env my_unify False envs tc tys +lookupFamInstEnvConflicts envs fam_inst@(FamInst { fi_axiom = new_axiom }) + = lookup_fam_inst_env my_unify envs fam tys where - my_unify :: MatchFun - my_unify _ (FamInstBranch { fib_tvs = tpl_tvs, fib_lhs = tpl_tys - , fib_rhs = tpl_rhs }) old_grp match_tys - = ASSERT( tyVarsOfTypes tys `disjointVarSet` mkVarSet tpl_tvs ) + (fam, tys) = famInstSplitLHS fam_inst + -- In example above, fam tys' = F [b] + + my_unify (FamInst { fi_axiom = old_axiom }) tpl_tvs tpl_tys _ + = ASSERT2( tyVarsOfTypes tys `disjointVarSet` tpl_tvs, + (ppr fam <+> ppr tys) $$ + (ppr tpl_tvs <+> ppr tpl_tys) ) -- Unification will break badly if the variables overlap -- They shouldn't because we allocate separate uniques for them - case tcUnifyTys instanceBindFun tpl_tys match_tys of - Just subst - | isDataFamilyTyCon tc - || grp - || old_grp - || rhs_conflict tpl_rhs rhs subst - -> (Just subst, KeepSearching) - | otherwise -- confluent overlap - -> (Nothing, KeepSearching) - -- irrelevant instance - Nothing -> (Nothing, KeepSearching) - - -- checks whether two RHSs are distinct, under a unifying substitution - -- Note [Family instance overlap conflicts] - rhs_conflict :: Type -> Type -> TvSubst -> Bool - rhs_conflict rhs1 rhs2 subst - = not (rhs1' `eqType` rhs2') - where - rhs1' = substTy subst rhs1 - rhs2' = substTy subst rhs2 - --- This variant is called when we want to check if the conflict is only in the --- home environment (see FamInst.addLocalFamInst) -lookupFamInstEnvConflicts' :: FamInstEnv -> Bool -> TyCon - -> FamInstBranch -> [FamInstMatch] -lookupFamInstEnvConflicts' env - = lookupFamInstEnvConflicts (emptyFamInstEnv, env) -\end{code} + if compatibleBranches (coAxiomSingleBranch old_axiom) (new_branch) + then Nothing + else Just noSubst + -- Note [Family instance overlap conflicts] -Note [lookup_fam_inst_env' implementation] -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -To reduce code duplication, both lookups during simplification and conflict -checking are routed through lookup_fam_inst_env', which looks for a -matching/unifying branch compared to some target. In the simplification -case, the search is for a match for a target application; in the conflict- -checking case, the search is for a unifier for a putative new instance branch. - -The two uses are differentiated by different MatchFuns, which look at a given -branch to see if it is relevant and whether the search should continue. The -the branch is relevant (i.e. matches or unifies), Just subst is -returned; if the instance is not relevant, Nothing is returned. The MatchFun -also indicates what the search algorithm should do next: it could -KeepSearching or StopSearching. - -When to StopSearching? See Note [Early failure optimisation for branched instances] - -For class instances, these two variants of lookup are combined into one -function (cf, @InstEnv@). We don't do that for family instances as the -results of matching and unification are used in two different contexts. -Moreover, matching is the wildly more frequently used operation in the case of -indexed synonyms and we don't want to slow that down by needless unification. + noSubst = panic "lookupFamInstEnvConflicts noSubst" + new_branch = coAxiomSingleBranch new_axiom +\end{code} Note [Family instance overlap conflicts] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ @@ -691,86 +612,83 @@ Note [Family instance overlap conflicts] conflict (as these instances imply injective type mappings). - In the case of type family instances, overlap is admitted as long as - the neither instance declares an instance group and the right-hand - sides of the overlapping rules coincide under the overlap substitution. - For example: + the right-hand sides of the overlapping rules coincide under the + overlap substitution. eg type instance F a Int = a type instance F Int b = b - These two overlap on (F Int Int) but then both RHSs are Int, + These two overlap on (F Int Int) but then both RHSs are Int, so all is well. We require that they are syntactically equal; anything else would be difficult to test for at this stage. \begin{code} ------------------------------------------------------------ -data ContSearch = KeepSearching - | StopSearching - -- Might be a one-way match or a unifier -type MatchFun = [FamInstBranch] -- the previous branches in the instance - -> FamInstBranch -- the individual branch to check - -> Bool -- is this branch a part of a branched instance? - -> [Type] -- the types to match against - -> (Maybe TvSubst, ContSearch) - -type OneSidedMatch = Bool -- Are optimisations that are only valid for - -- one sided matches allowed? +type MatchFun = FamInst -- The FamInst template + -> TyVarSet -> [Type] -- fi_tvs, fi_tys of that FamInst + -> [Type] -- Target to match against + -> Maybe TvSubst lookup_fam_inst_env' -- The worker, local to this module :: MatchFun - -> OneSidedMatch -> FamInstEnv -> TyCon -> [Type] -- What we are looking for -> [FamInstMatch] -lookup_fam_inst_env' match_fun _one_sided ie fam tys - | isFamilyTyCon fam +lookup_fam_inst_env' match_fun ie fam match_tys + | isOpenFamilyTyCon fam , Just (FamIE insts) <- lookupUFM ie fam - = find match_fun tys insts -- The common case + = find insts -- The common case | otherwise = [] - -find :: MatchFun -> [Type] -> [FamInst Branched] -> [FamInstMatch] -find _ _ [] = [] -find match_fun match_tys (inst@(FamInst { fi_branches = branches, fi_branched = is_branched }) : rest) - = case findBranch [] (fromBranchList branches) 0 of - (Just match, StopSearching) -> [match] - (Just match, KeepSearching) -> match : find match_fun match_tys rest - (Nothing, StopSearching) -> [] - (Nothing, KeepSearching) -> find match_fun match_tys rest where - rough_tcs = roughMatchTcs match_tys - - findBranch :: [FamInstBranch] -- the branches that have already been checked - -> [FamInstBranch] -- still looking through these - -> BranchIndex -- index of teh first of the "still looking" list - -> (Maybe FamInstMatch, ContSearch) - findBranch _ [] _ = (Nothing, KeepSearching) - findBranch seen (branch@(FamInstBranch { fib_tvs = tvs, fib_tcs = mb_tcs }) : rest) ind + + find [] = [] + find (item@(FamInst { fi_tcs = mb_tcs, fi_tvs = tpl_tvs, + fi_tys = tpl_tys }) : rest) + -- Fast check for no match, uses the "rough match" fields | instanceCantMatch rough_tcs mb_tcs - = findBranch seen rest (ind+1) -- branch won't unify later; no need to add to 'seen' + = find rest + + -- Proper check + | Just subst <- match_fun item (mkVarSet tpl_tvs) tpl_tys match_tys1 + = (FamInstMatch { fim_instance = item + , fim_tys = substTyVars subst tpl_tvs `chkAppend` match_tys2 }) + : find rest + + -- No match => try next | otherwise - = case match_fun seen branch is_branched match_tys1 of - (Nothing, KeepSearching) -> findBranch (branch : seen) rest (ind+1) - (Nothing, StopSearching) -> (Nothing, StopSearching) - (Just subst, cont) -> (Just match, cont) - where - match = FamInstMatch { fim_instance = inst - , fim_index = ind - , fim_tys = substTyVars subst tvs `chkAppend` match_tys2} + = find rest + where - -- Deal with over-saturation - -- See Note [Over-saturated matches] - (match_tys1, match_tys2) = splitAtList mb_tcs match_tys + (rough_tcs, match_tys1, match_tys2) = split_tys tpl_tys + + -- Precondition: the tycon is saturated (or over-saturated) + + -- Deal with over-saturation + -- See Note [Over-saturated matches] + split_tys tpl_tys + | isSynFamilyTyCon fam + = pre_rough_split_tys + + | otherwise + = let (match_tys1, match_tys2) = splitAtList tpl_tys match_tys + rough_tcs = roughMatchTcs match_tys1 + in (rough_tcs, match_tys1, match_tys2) + + (pre_match_tys1, pre_match_tys2) = splitAt (tyConArity fam) match_tys + pre_rough_split_tys + = (roughMatchTcs pre_match_tys1, pre_match_tys1, pre_match_tys2) lookup_fam_inst_env -- The worker, local to this module :: MatchFun - -> OneSidedMatch -> FamInstEnvs -> TyCon -> [Type] -- What we are looking for - -> [FamInstMatch] -- What was found + -> [FamInstMatch] -- Successful matches -- Precondition: the tycon is saturated (or over-saturated) -lookup_fam_inst_env match_fun one_sided (pkg_ie, home_ie) fam tys = - lookup_fam_inst_env' match_fun one_sided home_ie fam tys ++ - lookup_fam_inst_env' match_fun one_sided pkg_ie fam tys + +lookup_fam_inst_env match_fun (pkg_ie, home_ie) fam tys = + lookup_fam_inst_env' match_fun home_ie fam tys ++ + lookup_fam_inst_env' match_fun pkg_ie fam tys + \end{code} Note [Over-saturated matches] @@ -783,11 +701,19 @@ The type instance gives rise to a newtype TyCon (at a higher kind which you can't do in Haskell!): newtype FPair a b = FP (Either (a->b)) -Then looking up (F (Int,Bool) Char) will return a FamInstMatch +Then looking up (F (Int,Bool) Char) will return a FamInstMatch (FPair, [Int,Bool,Char]) The "extra" type argument [Char] just stays on the end. +Because of eta-reduction of data family instances (see +Note [Eta reduction for data family axioms] in TcInstDecls), we must +handle data families and type families separately here. All instances +of a type family must have the same arity, so we can precompute the split +between the match_tys and the overflow tys. This is done in pre_rough_split_tys. +For data instances, though, we need to re-split for each instance, because +the breakdown might be different. + \begin{code} -- checks if one LHS is dominated by a list of other branches @@ -808,6 +734,72 @@ isDominatedBy branch branches = isJust $ tcMatchTys (mkVarSet tvs) tys lhs \end{code} +%************************************************************************ +%* * + Choosing an axiom application +%* * +%************************************************************************ + +The lookupFamInstEnv function does a nice job for *open* type families, +but we also need to handle closed ones when normalising a type: + +\begin{code} + +-- The TyCon can be oversaturated. This works on both open and closed families +chooseAxiom :: FamInstEnvs -> TyCon -> [Type] -> Maybe (Coercion, Type) +chooseAxiom envs tc tys + | isOpenFamilyTyCon tc + , [FamInstMatch { fim_instance = fam_inst + , fim_tys = inst_tys }] <- lookupFamInstEnv envs tc tys + = let co = mkUnbranchedAxInstCo (famInstAxiom fam_inst) inst_tys + ty = pSnd (coercionKind co) + in Just (co, ty) + + | Just ax <- isClosedSynFamilyTyCon_maybe tc + , Just (ind, inst_tys) <- chooseBranch ax tys + = let co = mkAxInstCo ax ind inst_tys + ty = pSnd (coercionKind co) + in Just (co, ty) + + | otherwise + = Nothing + +-- The axiom can be oversaturated. (Closed families only.) +chooseBranch :: CoAxiom Branched -> [Type] -> Maybe (BranchIndex, [Type]) +chooseBranch axiom tys + = do { let num_pats = coAxiomNumPats axiom + (target_tys, extra_tys) = splitAt num_pats tys + branches = coAxiomBranches axiom + ; (ind, inst_tys) <- findBranch (fromBranchList branches) 0 target_tys + ; return (ind, inst_tys ++ extra_tys) } + +-- The axiom must *not* be oversaturated +findBranch :: [CoAxBranch] -- branches to check + -> BranchIndex -- index of current branch + -> [Type] -- target types + -> Maybe (BranchIndex, [Type]) +findBranch (CoAxBranch { cab_tvs = tpl_tvs, cab_lhs = tpl_lhs, cab_incomps = incomps } + : rest) ind target_tys + = case tcMatchTys (mkVarSet tpl_tvs) tpl_lhs target_tys of + Just subst -- matching worked. now, check for apartness. + | all (isSurelyApart + . tcApartTys instanceBindFun target_tys + . coAxBranchLHS) $ -- RAE: This is horribly inefficient + incomps + -> -- matching worked & we're apart from all incompatible branches. success + Just (ind, substTyVars subst tpl_tvs) + + -- failure. keep looking + _ -> findBranch rest (ind+1) target_tys + + where isSurelyApart SurelyApart = True + isSurelyApart _ = False + +-- fail if no branches left +findBranch [] _ _ = Nothing + +\end{code} + %************************************************************************ %* * @@ -820,8 +812,8 @@ topNormaliseType :: FamInstEnvs -> Type -> Maybe (Coercion, Type) --- Get rid of *outermost* (or toplevel) --- * type functions +-- Get rid of *outermost* (or toplevel) +-- * type functions -- * newtypes -- using appropriate coercions. -- By "outer" we mean that toplevelNormaliseType guarantees to return @@ -843,7 +835,7 @@ topNormaliseType env ty = add_co nt_co rec_nts' nt_rhs go rec_nts (TyConApp tc tys) - | isFamilyTyCon tc -- Expand open tycons + | isFamilyTyCon tc -- Expand family tycons , (co, ty) <- normaliseTcApp env tc tys -- Note that normaliseType fully normalises 'tys', -- wrt type functions but *not* newtypes @@ -855,23 +847,18 @@ topNormaliseType env ty go _ _ = Nothing - add_co co rec_nts ty + add_co co rec_nts ty = case go rec_nts ty of Nothing -> Just (co, ty) Just (co', ty') -> Just (mkTransCo co co', ty') - + --------------- normaliseTcApp :: FamInstEnvs -> TyCon -> [Type] -> (Coercion, Type) normaliseTcApp env tc tys | isFamilyTyCon tc - , [FamInstMatch { fim_instance = fam_inst - , fim_index = fam_ind - , fim_tys = inst_tys }] <- lookupFamInstEnv env tc ntys - = let -- A matching family instance exists - ax = famInstAxiom fam_inst - co = mkAxInstCo ax fam_ind inst_tys - rhs = mkAxInstRHS ax fam_ind inst_tys + , Just (co, rhs) <- chooseAxiom env tc ntys + = let -- A reduction is possible first_coi = mkTransCo tycon_coi co (rest_coi,nty) = normaliseType env rhs fix_coi = mkTransCo first_coi rest_coi @@ -879,26 +866,25 @@ normaliseTcApp env tc tys (fix_coi, nty) | otherwise -- No unique matching family instance exists; - -- we do not do anything (including for newtypes) + -- we do not do anything = (tycon_coi, TyConApp tc ntys) where - -- Normalise the arg types so that they'll match + -- Normalise the arg types so that they'll match -- when we lookup in in the instance envt (cois, ntys) = mapAndUnzip (normaliseType env) tys tycon_coi = mkTyConAppCo tc cois --------------- normaliseType :: FamInstEnvs -- environment with family instances - -> Type -- old type + -> Type -- old type -> (Coercion, Type) -- (coercion,new type), where -- co :: old-type ~ new_type -- Normalise the input type, by eliminating *all* type-function redexes -- Returns with Refl if nothing happens --- Does nothing to newtypes -normaliseType env ty - | Just ty' <- coreView ty = normaliseType env ty' +normaliseType env ty + | Just ty' <- coreView ty = normaliseType env ty' normaliseType env (TyConApp tc tys) = normaliseTcApp env tc tys normaliseType _env ty@(LitTy {}) = (Refl ty, ty) diff --git a/compiler/types/OptCoercion.lhs b/compiler/types/OptCoercion.lhs index 7eaab5c8a1..d3dd2a4697 100644 --- a/compiler/types/OptCoercion.lhs +++ b/compiler/types/OptCoercion.lhs @@ -381,27 +381,28 @@ Note [Branched instance checking] in types/FamInstEnv.lhs. \begin{code} -- | Check to make sure that an AxInstCo is internally consistent. --- Returns the number of the conflicting branch, if it exists +-- Returns the conflicting branch, if it exists -- See Note [Conflict checking with AxiomInstCo] -checkAxInstCo :: Coercion -> Maybe Int +checkAxInstCo :: Coercion -> Maybe CoAxBranch -- defined here to avoid dependencies in Coercion +-- If you edit this function, you may need to update the GHC formalism +-- See Note [GHC Formalism] in CoreLint checkAxInstCo (AxiomInstCo ax ind cos) = let branch = coAxiomNthBranch ax ind tvs = coAxBranchTyVars branch + incomps = coAxBranchIncomps branch tys = map (pFst . coercionKind) cos subst = zipOpenTvSubst tvs tys lhs' = Type.substTys subst (coAxBranchLHS branch) in - check_no_conflict lhs' (ind-1) + check_no_conflict lhs' incomps where - check_no_conflict :: [Type] -> Int -> Maybe Int - check_no_conflict _ (-1) = Nothing - check_no_conflict lhs' j - | SurelyApart <- tcApartTys instanceBindFun lhs' lhsj - = check_no_conflict lhs' (j-1) + check_no_conflict :: [Type] -> [CoAxBranch] -> Maybe CoAxBranch + check_no_conflict _ [] = Nothing + check_no_conflict lhs' (b@CoAxBranch { cab_lhs = lhs_incomp } : rest) + | SurelyApart <- tcApartTys instanceBindFun lhs' lhs_incomp + = check_no_conflict lhs' rest | otherwise - = Just j - where - (CoAxBranch { cab_lhs = lhsj }) = coAxiomNthBranch ax j + = Just b checkAxInstCo _ = Nothing ----------- diff --git a/compiler/types/TyCon.lhs b/compiler/types/TyCon.lhs index bb95b795f1..fb078ec979 100644 --- a/compiler/types/TyCon.lhs +++ b/compiler/types/TyCon.lhs @@ -34,7 +34,7 @@ module TyCon( isFunTyCon, isPrimTyCon, isTupleTyCon, isUnboxedTupleTyCon, isBoxedTupleTyCon, - isSynTyCon, isOpenSynFamilyTyCon, + isSynTyCon, isDecomposableTyCon, isForeignTyCon, isPromotedDataCon, isPromotedTyCon, @@ -45,7 +45,9 @@ module TyCon( isDataTyCon, isProductTyCon, isDataProductTyCon_maybe, isEnumerationTyCon, isNewTyCon, isAbstractTyCon, - isFamilyTyCon, isSynFamilyTyCon, isDataFamilyTyCon, + isFamilyTyCon, isOpenFamilyTyCon, + isSynFamilyTyCon, isDataFamilyTyCon, + isOpenSynFamilyTyCon, isClosedSynFamilyTyCon_maybe, isUnLiftedTyCon, isGadtSyntaxTyCon, isDistinctTyCon, isDistinctAlgRhs, isTyConAssoc, tyConAssoc_maybe, @@ -137,17 +139,19 @@ Note [Type synonym families] * Translation of type family decl: type family F a :: * translates to - a SynTyCon 'F', whose SynTyConRhs is SynFamilyTyCon + a SynTyCon 'F', whose SynTyConRhs is OpenSynFamilyTyCon -* Translation of type family decl: - type family F a :: * + type family G a :: * where + G Int = Bool + G Bool = Char + G a = () translates to - a SynTyCon 'F', whose SynTyConRhs is SynFamilyTyCon + a SynTyCon 'G', whose SynTyConRhs is ClosedSynFamilyTyCon, with the + appropriate CoAxiom representing the equations * In the future we might want to support - * closed type families (esp when we have proper kinds) * injective type families (allow decomposition) - but we don't at the moment [2010] + but we don't at the moment [2013] Note [Data type families] ~~~~~~~~~~~~~~~~~~~~~~~~~ @@ -369,7 +373,7 @@ data TyCon tyConTyVars :: [TyVar], -- Bound tyvars - synTcRhs :: SynTyConRhs Type, -- ^ Contains information about the + synTcRhs :: SynTyConRhs, -- ^ Contains information about the -- expansion of the synonym synTcParent :: TyConParent -- ^ Gives the family declaration 'TyCon' @@ -577,18 +581,19 @@ isNoParent _ = False -------------------- -- | Information pertaining to the expansion of a type synonym (@type@) -data SynTyConRhs ty +data SynTyConRhs = -- | An ordinary type synonyn. SynonymTyCon - ty -- This 'Type' is the rhs, and may mention from 'tyConTyVars'. + Type -- This 'Type' is the rhs, and may mention from 'tyConTyVars'. -- It acts as a template for the expansion when the 'TyCon' -- is applied to some types. - -- | A type synonym family e.g. @type family F x y :: * -> *@ - | SynFamilyTyCon { - synf_open :: Bool, -- See Note [Closed type families] - synf_injective :: Bool - } + -- | An open type synonym family e.g. @type family F x y :: * -> *@ + | OpenSynFamilyTyCon + + -- | A closed type synonym family e.g. @type family F x where { F Int = Bool }@ + | ClosedSynFamilyTyCon + (CoAxiom Branched) -- The one axiom for this family \end{code} Note [Closed type families] @@ -596,8 +601,9 @@ Note [Closed type families] * In an open type family you can add new instances later. This is the usual case. -* In a closed type family you can only put instnaces where the family - is defined. GHC doesn't support syntax for this yet. +* In a closed type family you can only put equations where the family + is defined. + Note [Promoted data constructors] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ @@ -970,7 +976,7 @@ mkPrimTyCon' name kind arity rep is_unlifted } -- | Create a type synonym 'TyCon' -mkSynTyCon :: Name -> Kind -> [TyVar] -> SynTyConRhs Type -> TyConParent -> TyCon +mkSynTyCon :: Name -> Kind -> [TyVar] -> SynTyConRhs -> TyConParent -> TyCon mkSynTyCon name kind tyvars rhs parent = SynTyCon { tyConName = name, @@ -1153,21 +1159,35 @@ isEnumerationTyCon (AlgTyCon {algTcRhs = DataTyCon { is_enum = res }}) = res isEnumerationTyCon (TupleTyCon {tyConArity = arity}) = arity == 0 isEnumerationTyCon _ = False --- | Is this a 'TyCon', synonym or otherwise, that may have further instances appear? +-- | Is this a 'TyCon', synonym or otherwise, that defines a family? isFamilyTyCon :: TyCon -> Bool -isFamilyTyCon (SynTyCon {synTcRhs = SynFamilyTyCon {}}) = True -isFamilyTyCon (AlgTyCon {algTcRhs = DataFamilyTyCon {}}) = True +isFamilyTyCon (SynTyCon {synTcRhs = OpenSynFamilyTyCon }) = True +isFamilyTyCon (SynTyCon {synTcRhs = ClosedSynFamilyTyCon {} }) = True +isFamilyTyCon (AlgTyCon {algTcRhs = DataFamilyTyCon {}}) = True isFamilyTyCon _ = False +-- | Is this a 'TyCon', synonym or otherwise, that defines an family with +-- instances? +isOpenFamilyTyCon :: TyCon -> Bool +isOpenFamilyTyCon (SynTyCon {synTcRhs = OpenSynFamilyTyCon }) = True +isOpenFamilyTyCon (AlgTyCon {algTcRhs = DataFamilyTyCon }) = True +isOpenFamilyTyCon _ = False + -- | Is this a synonym 'TyCon' that can have may have further instances appear? isSynFamilyTyCon :: TyCon -> Bool -isSynFamilyTyCon (SynTyCon {synTcRhs = SynFamilyTyCon {}}) = True +isSynFamilyTyCon (SynTyCon {synTcRhs = OpenSynFamilyTyCon {}}) = True +isSynFamilyTyCon (SynTyCon {synTcRhs = ClosedSynFamilyTyCon {}}) = True isSynFamilyTyCon _ = False isOpenSynFamilyTyCon :: TyCon -> Bool -isOpenSynFamilyTyCon (SynTyCon {synTcRhs = SynFamilyTyCon { synf_open = is_open } }) = is_open +isOpenSynFamilyTyCon (SynTyCon {synTcRhs = OpenSynFamilyTyCon }) = True isOpenSynFamilyTyCon _ = False +isClosedSynFamilyTyCon_maybe :: TyCon -> Maybe (CoAxiom Branched) +isClosedSynFamilyTyCon_maybe + (SynTyCon {synTcRhs = ClosedSynFamilyTyCon ax}) = Just ax +isClosedSynFamilyTyCon_maybe _ = Nothing + -- | Is this a synonym 'TyCon' that can have may have further instances appear? isDataFamilyTyCon :: TyCon -> Bool isDataFamilyTyCon (AlgTyCon {algTcRhs = DataFamilyTyCon {}}) = True @@ -1427,7 +1447,7 @@ synTyConDefn_maybe (SynTyCon {tyConTyVars = tyvars, synTcRhs = SynonymTyCon ty}) synTyConDefn_maybe _ = Nothing -- | Extract the information pertaining to the right hand side of a type synonym (@type@) declaration. -synTyConRhs_maybe :: TyCon -> Maybe (SynTyConRhs Type) +synTyConRhs_maybe :: TyCon -> Maybe SynTyConRhs synTyConRhs_maybe (SynTyCon {synTcRhs = rhs}) = Just rhs synTyConRhs_maybe _ = Nothing \end{code} @@ -1604,4 +1624,4 @@ checkRecTc (RC rec_nts) tc | otherwise = Just (RC (addOneToNameSet rec_nts tc_name)) where tc_name = tyConName tc -\end{code}
\ No newline at end of file +\end{code} diff --git a/compiler/types/Unify.lhs b/compiler/types/Unify.lhs index 67e748e777..34bc4b5ec4 100644 --- a/compiler/types/Unify.lhs +++ b/compiler/types/Unify.lhs @@ -25,7 +25,7 @@ module Unify ( tcUnifyTys, BindFlag(..), niFixTvSubst, niSubstTvSet, - ApartResult(..), tcApartTys + UnifyResultM(..), UnifyResult, tcApartTys ) where @@ -377,10 +377,10 @@ The workhorse function behind unification actually is testing for apartness, not unification. (See [Apartness], above.) There are three possibilities here: - - two types might be NotApart, which means a substitution can be found between + - two types might be Unifiable, which means a substitution can be found between them, - Example: (Either a Int) and (Either Bool b) are NotApart, with + Example: (Either a Int) and (Either Bool b) are Unifiable, with [a |-> Bool, b |-> Int] - they might be MaybeApart, which means that we're not sure, but a substitution @@ -393,7 +393,7 @@ possibilities here: Example: (Either Int a) and (Either Bool b) are SurelyApart -In the NotApart case, the apartness finding function also returns a +In the Unifiable case, the apartness finding function also returns a substitution, which we can then use to unify the types. It is necessary for the unification algorithm to depend on the apartness algorithm, because apartness is finer-grained than unification. @@ -433,6 +433,41 @@ substituted, we can't properly unify the types. But, that skolem variable may later be instantiated with a unifyable type. So, we return maybeApart in these cases. +Note [Apartness and the occurs check] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +Are the types (x, x) and ([y], y) apart? The answer is "maybe". They clearly +don't unify, but they also don't have a direct conflict. This is somewhere +between unifiable and surely apart, so we use maybeApart. + +It turns out that this whole area is rather delicate, as regards soundness of +type families. Specifically, we need to disallow the two instances + + F x x = Int + F [y] y = Bool + +because if we have + + Looper = [Looper] + +then the instances potentially overlap. A simple unification doesn't eliminate +the overlap, so we use an apartness check with this special handling of the +occurs check. + +Note [The substitution in MaybeApart] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +The constructor MaybeApart carries data with it, typically a TvSubstEnv. Why? +Because consider unifying these: + +(a, a, a) ~ (Int, F Bool, Bool) + +If we go left-to-right, we start with [a |-> Int]. Then, on the middle terms, +we apply the subst we have so far and discover that Int is maybeApart from +F Bool. But, we can't stop there! Because if we continue, we discover that +Int is SurelyApart from Bool, and therefore the types are apart. This has +practical consequences for the ability for closed type family applications +to reduce. See test case indexed-types/should_compile/Overlap14. + + \begin{code} -- See Note [Unification and apartness] tcUnifyTys :: (TyVar -> BindFlag) @@ -442,18 +477,23 @@ tcUnifyTys :: (TyVar -> BindFlag) -- second call to tcUnifyTys in FunDeps.checkClsFD -- tcUnifyTys bind_fn tys1 tys2 - | NotApart subst <- tcApartTys bind_fn tys1 tys2 + | Unifiable subst <- tcApartTys bind_fn tys1 tys2 = Just subst | otherwise = Nothing -data ApartResult = NotApart TvSubst -- the subst that unifies the types - | MaybeApart - | SurelyApart +-- This type does double-duty. It is used in the UM (unifier monad) and to +-- return the final result. +type UnifyResult = UnifyResultM TvSubst +data UnifyResultM a = Unifiable a -- the subst that unifies the types + | MaybeApart a -- the subst has as much as we know + -- it must be part of an most general unifier + -- See Note [The substitution in MaybeApart] + | SurelyApart tcApartTys :: (TyVar -> BindFlag) -> [Type] -> [Type] - -> ApartResult + -> UnifyResult tcApartTys bind_fn tys1 tys2 = initUM bind_fn $ do { subst <- unifyList emptyTvSubstEnv tys1 tys2 @@ -527,13 +567,13 @@ unify subst ty1 ty2 | Just ty2' <- tcView ty2 = unify subst ty1 ty2' unify subst (TyConApp tyc1 tys1) (TyConApp tyc2 tys2) | tyc1 == tyc2 = unify_tys subst tys1 tys2 - | isSynFamilyTyCon tyc1 || isSynFamilyTyCon tyc2 = maybeApart + | isSynFamilyTyCon tyc1 || isSynFamilyTyCon tyc2 = maybeApart subst -- See Note [Unifying with type families] -unify _ (TyConApp tyc _) _ - | isSynFamilyTyCon tyc = maybeApart -unify _ _ (TyConApp tyc _) - | isSynFamilyTyCon tyc = maybeApart +unify subst (TyConApp tyc _) _ + | isSynFamilyTyCon tyc = maybeApart subst +unify subst _ (TyConApp tyc _) + | isSynFamilyTyCon tyc = maybeApart subst unify subst (FunTy ty1a ty1b) (FunTy ty2a ty2b) = do { subst' <- unify subst ty1a ty2a @@ -621,13 +661,14 @@ uUnrefined subst tv1 ty2 (TyVarTy tv2) ; b2 <- tvBindFlag tv2 ; let ty1 = TyVarTy tv1 ; case (b1, b2) of - (Skolem, Skolem) -> maybeApart -- See Note [Apartness with skolems] + (Skolem, Skolem) -> maybeApart subst' -- See Note [Apartness with skolems] (BindMe, _) -> return (extendVarEnv subst' tv1 ty2) (_, BindMe) -> return (extendVarEnv subst' tv2 ty1) } uUnrefined subst tv1 ty2 ty2' -- ty2 is not a type variable | tv1 `elemVarSet` niSubstTvSet subst (tyVarsOfType ty2') - = surelyApart -- Occurs check + = maybeApart subst -- Occurs check + -- See Note [Apartness and the occurs check] | otherwise = do { subst' <- unify subst k1 k2 ; bindTv subst' tv1 ty2 } -- Bind tyvar to the synonym if poss @@ -639,7 +680,7 @@ bindTv :: TvSubstEnv -> TyVar -> Type -> UM TvSubstEnv bindTv subst tv ty -- ty is not a type variable = do { b <- tvBindFlag tv ; case b of - Skolem -> maybeApart -- See Note [Apartness with skolems] + Skolem -> maybeApart subst -- See Note [Apartness with skolems] BindMe -> return $ extendVarEnv subst tv ty } \end{code} @@ -666,33 +707,30 @@ data BindFlag %************************************************************************ \begin{code} -data UnifFailure = UFMaybeApart - | UFSurelyApart - newtype UM a = UM { unUM :: (TyVar -> BindFlag) - -> Either UnifFailure a } + -> UnifyResultM a } instance Monad UM where - return a = UM (\_tvs -> Right a) - fail _ = UM (\_tvs -> Left UFSurelyApart) -- failed pattern match + return a = UM (\_tvs -> Unifiable a) + fail _ = UM (\_tvs -> SurelyApart) -- failed pattern match m >>= k = UM (\tvs -> case unUM m tvs of - Right v -> unUM (k v) tvs - Left f -> Left f) - -initUM :: (TyVar -> BindFlag) -> UM TvSubst -> ApartResult -initUM badtvs um - = case unUM um badtvs of - Right subst -> NotApart subst - Left UFMaybeApart -> MaybeApart - Left UFSurelyApart -> SurelyApart + Unifiable v -> unUM (k v) tvs + MaybeApart v -> + case unUM (k v) tvs of + Unifiable v' -> MaybeApart v' + other -> other + SurelyApart -> SurelyApart) + +initUM :: (TyVar -> BindFlag) -> UM TvSubst -> UnifyResult +initUM badtvs um = unUM um badtvs tvBindFlag :: TyVar -> UM BindFlag -tvBindFlag tv = UM (\tv_fn -> Right (tv_fn tv)) +tvBindFlag tv = UM (\tv_fn -> Unifiable (tv_fn tv)) -maybeApart :: UM a -maybeApart = UM (\_tv_fn -> Left UFMaybeApart) +maybeApart :: TvSubstEnv -> UM TvSubstEnv +maybeApart subst = UM (\_tv_fn -> MaybeApart subst) surelyApart :: UM a -surelyApart = UM (\_tv_fn -> Left UFSurelyApart) +surelyApart = UM (\_tv_fn -> SurelyApart) \end{code} diff --git a/compiler/vectorise/Vectorise.hs b/compiler/vectorise/Vectorise.hs index b939f4beb6..012ae37039 100644 --- a/compiler/vectorise/Vectorise.hs +++ b/compiler/vectorise/Vectorise.hs @@ -27,7 +27,6 @@ import DynFlags import Outputable import Util ( zipLazy ) import MonadUtils -import FamInstEnv ( toBranchedFamInst ) import Control.Monad @@ -93,7 +92,7 @@ vectModule guts@(ModGuts { mg_tcs = tycons -- and dfuns , mg_binds = Rec tc_binds : (binds_top ++ binds_imp) , mg_fam_inst_env = fam_inst_env - , mg_fam_insts = fam_insts ++ (map toBranchedFamInst new_fam_insts) + , mg_fam_insts = fam_insts ++ new_fam_insts } } diff --git a/compiler/vectorise/Vectorise/Env.hs b/compiler/vectorise/Vectorise/Env.hs index 2d415aab36..3358ceafab 100644 --- a/compiler/vectorise/Vectorise/Env.hs +++ b/compiler/vectorise/Vectorise/Env.hs @@ -174,7 +174,7 @@ extendImportedVarsEnv ps genv -- |Extend the list of type family instances. -- -extendFamEnv :: [FamInst Unbranched] -> GlobalEnv -> GlobalEnv +extendFamEnv :: [FamInst] -> GlobalEnv -> GlobalEnv extendFamEnv new genv = genv { global_fam_inst_env = (g_fam_inst, extendFamInstEnvList l_fam_inst new) } where (g_fam_inst, l_fam_inst) = global_fam_inst_env genv diff --git a/compiler/vectorise/Vectorise/Generic/PAMethods.hs b/compiler/vectorise/Vectorise/Generic/PAMethods.hs index af815c9294..9390696fc7 100644 --- a/compiler/vectorise/Vectorise/Generic/PAMethods.hs +++ b/compiler/vectorise/Vectorise/Generic/PAMethods.hs @@ -32,13 +32,13 @@ import Control.Monad import Outputable -buildPReprTyCon :: TyCon -> TyCon -> SumRepr -> VM (FamInst Unbranched) +buildPReprTyCon :: TyCon -> TyCon -> SumRepr -> VM FamInst buildPReprTyCon orig_tc vect_tc repr = do name <- mkLocalisedName mkPReprTyConOcc (tyConName orig_tc) rhs_ty <- sumReprType repr prepr_tc <- builtin preprTyCon let axiom = mkSingleCoAxiom name tyvars prepr_tc instTys rhs_ty - liftDs $ newFamInst SynFamilyInst False axiom + liftDs $ newFamInst SynFamilyInst axiom where tyvars = tyConTyVars vect_tc instTys = [mkTyConApp vect_tc . mkTyVarTys $ tyConTyVars vect_tc] diff --git a/compiler/vectorise/Vectorise/Generic/PData.hs b/compiler/vectorise/Vectorise/Generic/PData.hs index 893f1559be..6b06996ec8 100644 --- a/compiler/vectorise/Vectorise/Generic/PData.hs +++ b/compiler/vectorise/Vectorise/Generic/PData.hs @@ -14,7 +14,6 @@ import Vectorise.Generic.Description import Vectorise.Utils import Vectorise.Env( GlobalEnv( global_fam_inst_env ) ) -import Coercion( mkSingleCoAxiom ) import BasicTypes import BuildTyCl import DataCon @@ -31,7 +30,7 @@ import Control.Monad -- buildPDataTyCon ------------------------------------------------------------ -- | Build the PData instance tycon for a given type constructor. -buildPDataTyCon :: TyCon -> TyCon -> SumRepr -> VM (FamInst Unbranched) +buildPDataTyCon :: TyCon -> TyCon -> SumRepr -> VM FamInst buildPDataTyCon orig_tc vect_tc repr = fixV $ \fam_inst -> do let repr_tc = dataFamInstRepTyCon fam_inst @@ -42,7 +41,7 @@ buildPDataTyCon orig_tc vect_tc repr where orig_name = tyConName orig_tc -buildDataFamInst :: Name -> TyCon -> TyCon -> AlgTyConRhs -> VM (FamInst Unbranched) +buildDataFamInst :: Name -> TyCon -> TyCon -> AlgTyConRhs -> VM FamInst buildDataFamInst name' fam_tc vect_tc rhs = do { axiom_name <- mkDerivedName mkInstTyCoOcc name' @@ -60,7 +59,7 @@ buildDataFamInst name' fam_tc vect_tc rhs False -- Not promotable False -- not GADT syntax (FamInstTyCon ax fam_tc pat_tys) - ; liftDs $ newFamInst (DataFamilyInst rep_tc) False ax } + ; liftDs $ newFamInst (DataFamilyInst rep_tc) ax } where tyvars = tyConTyVars vect_tc rec_flag = boolToRecFlag (isRecursiveTyCon vect_tc) @@ -92,7 +91,7 @@ buildPDataDataCon orig_name vect_tc repr_tc repr -- buildPDatasTyCon ----------------------------------------------------------- -- | Build the PDatas instance tycon for a given type constructor. -buildPDatasTyCon :: TyCon -> TyCon -> SumRepr -> VM (FamInst Unbranched) +buildPDatasTyCon :: TyCon -> TyCon -> SumRepr -> VM FamInst buildPDatasTyCon orig_tc vect_tc repr = fixV $ \fam_inst -> do let repr_tc = dataFamInstRepTyCon fam_inst diff --git a/compiler/vectorise/Vectorise/Monad/InstEnv.hs b/compiler/vectorise/Vectorise/Monad/InstEnv.hs index ceb62eef80..84b29ceb61 100644 --- a/compiler/vectorise/Vectorise/Monad/InstEnv.hs +++ b/compiler/vectorise/Vectorise/Monad/InstEnv.hs @@ -67,7 +67,7 @@ lookupInst cls tys -- lookupFamInst :: TyCon -> [Type] -> VM FamInstMatch lookupFamInst tycon tys - = ASSERT( isFamilyTyCon tycon ) + = ASSERT( isOpenFamilyTyCon tycon ) do { instEnv <- readGEnv global_fam_inst_env ; case lookupFamInstEnv instEnv tycon tys of [match] -> return match diff --git a/compiler/vectorise/Vectorise/Type/Env.hs b/compiler/vectorise/Vectorise/Type/Env.hs index 0ae0f936b3..66db6185da 100644 --- a/compiler/vectorise/Vectorise/Type/Env.hs +++ b/compiler/vectorise/Vectorise/Type/Env.hs @@ -162,7 +162,7 @@ vectTypeEnv :: [TyCon] -- Type constructors defined in this mo -> [CoreVect] -- All 'VECTORISE [SCALAR] type' declarations in this module -> [CoreVect] -- All 'VECTORISE class' declarations in this module -> VM ( [TyCon] -- old TyCons ++ new TyCons - , [FamInst Unbranched] -- New type family instances. + , [FamInst] -- New type family instances. , [(Var, CoreExpr)]) -- New top level bindings. vectTypeEnv tycons vectTypeDecls vectClassDecls = do { traceVt "** vectTypeEnv" $ ppr tycons diff --git a/compiler/vectorise/Vectorise/Utils/Base.hs b/compiler/vectorise/Vectorise/Utils/Base.hs index d088f45355..0bd54f4408 100644 --- a/compiler/vectorise/Vectorise/Utils/Base.hs +++ b/compiler/vectorise/Vectorise/Utils/Base.hs @@ -39,8 +39,6 @@ import DataCon import MkId import DynFlags import FastString -import Util -import Panic #include "HsVersions.h" @@ -211,10 +209,8 @@ pdataReprTyCon :: Type -> VM (TyCon, [Type]) pdataReprTyCon ty = do { FamInstMatch { fim_instance = famInst - , fim_index = index , fim_tys = tys } <- builtin pdataTyCon >>= (`lookupFamInst` [ty]) - ; ASSERT( index == 0 ) - return (dataFamInstRepTyCon famInst, tys) + ; return (dataFamInstRepTyCon famInst, tys) } -- |Get the representation tycon of the 'PData' data family for a given type constructor. diff --git a/compiler/vectorise/Vectorise/Utils/PADict.hs b/compiler/vectorise/Vectorise/Utils/PADict.hs index 8029dfb466..84a6ff37d9 100644 --- a/compiler/vectorise/Vectorise/Utils/PADict.hs +++ b/compiler/vectorise/Vectorise/Utils/PADict.hs @@ -119,7 +119,7 @@ prDictOfPReprInst :: Type -> VM CoreExpr prDictOfPReprInst ty = do { (FamInstMatch { fim_instance = prepr_fam, fim_tys = prepr_args }) <- preprSynTyCon ty - ; prDictOfPReprInstTyCon ty (famInstAxiom (toUnbranchedFamInst prepr_fam)) prepr_args + ; prDictOfPReprInstTyCon ty (famInstAxiom prepr_fam) prepr_args } -- |Given a type @ty@, its PRepr synonym tycon and its type arguments, diff --git a/docs/core-spec/CoreLint.ott b/docs/core-spec/CoreLint.ott index beaf52a7d9..c452877ad5 100644 --- a/docs/core-spec/CoreLint.ott +++ b/docs/core-spec/CoreLint.ott @@ -229,7 +229,7 @@ forall </ ni // i />. (</ s1j // j /> ~> t1) = (</ axBranchkk // kk />)[ind] </ substi @ // i /> = inits(</ [ ni |-> s'i ] // i />) </ ni = zi_ki // i /> </ k'i <: substi(ki) // i /> -no_conflict(C, </ s2j // j />, ind-1) +no_conflict(C, </ s2j // j />, ind, ind-1) </ s2j = s1j </ [ni |-> s'i] // i/> // j /> t2 = t1 </ [ni |-> t'i] // i /> G |-ty t2 : k @@ -403,16 +403,32 @@ Constraint <: * ------------------ :: LiftedConstraint * <: Constraint -defn no_conflict ( C , </ sj // j /> , ind ) :: :: check_no_conflict :: 'NoConflict_' - {{ com Branched axiom conflict checking, \coderef{coreSyn/CoreLint.lhs}{lintCoercion\#check\_no\_conflict} }} +defn no_conflict ( C , </ sj // j /> , ind1 , ind2 ) :: :: check_no_conflict :: 'NoConflict_' + {{ com \parbox{5in}{Branched axiom conflict checking, \coderef{types/OptCoercion.lhs}{checkAxInstCo} \\ and \coderef{types/FamInstEnv.lhs}{compatibleBranches} } }} by ------------------------------------------------ :: NoBranch -no_conflict(C, </ si // i/>, -1) +no_conflict(C, </ si // i/>, ind, -1) C = T </ axBranchkk // kk /> -forall </ ni // i />. (</ tj // j /> ~> t') = (</ axBranchkk // kk />)[ind] +forall </ ni // i />. (</ tj // j /> ~> t') = (</ axBranchkk // kk />)[ind2] apart(</ sj // j />, </ tj // j />) -no_conflict(C, </ sj // j />, ind-1) ------------------------------------------------- :: Branch -no_conflict(C, </ sj // j />, ind) +no_conflict(C, </ sj // j />, ind1, ind2-1) +------------------------------------------------ :: Incompat +no_conflict(C, </ sj // j />, ind1, ind2) + +C = T </ axBranchkk // kk /> +forall </ ni // i />. (</ tj // j /> ~> s) = (</ axBranchkk // kk />)[ind1] +forall </ n'i // i />. (</ t'j // j /> ~> s') = (</ axBranchkk // kk />)[ind2] +apart(</ tj // j />, </ t'j // j />) +no_conflict(C, </ sj // j />, ind1, ind2-1) +------------------------------------------- :: CompatApart +no_conflict(C, </ sj // j />, ind1, ind2) + +C = T </ axBranchkk // kk /> +forall </ ni // i />. (</ tj // j /> ~> s) = (</ axBranchkk // kk />)[ind1] +forall </ n'i // i />. (</ t'j // j /> ~> s') = (</ axBranchkk // kk />)[ind2] +unify(</ tj // j />, </ t'j // j />) = subst +subst(s) = subst(s') +----------------------------------------- :: CompatCoincident +no_conflict(C, </ sj // j />, ind1, ind2)
\ No newline at end of file diff --git a/docs/core-spec/CoreSyn.ott b/docs/core-spec/CoreSyn.ott index 4c59849bb6..ca27b8b34c 100644 --- a/docs/core-spec/CoreSyn.ott +++ b/docs/core-spec/CoreSyn.ott @@ -117,7 +117,7 @@ LorR :: 'LeftOrRight_' ::= {{ com left or right deconstructor, \coderef{types/Co C :: 'CoAxiom_' ::= {{ com Axioms, \coderef{types/TyCon.lhs}{CoAxiom} }} | T </ axBranchi // ; // i /> :: :: CoAxiom {{ com Axiom }} - | ( C ) :: M :: Parens {{ com Parentheses }} + | ( C ) :: M :: Parens {{ com Parentheses }} axBranch, b :: 'CoAxBranch_' ::= {{ com Axiom branches, \coderef{types/TyCon.lhs}{CoAxBranch} }} | forall </ ni // i /> . ( </ tj // j /> ~> s ) :: :: CoAxBranch {{ com Axiom branch }} @@ -229,6 +229,7 @@ terminals :: 'terminals_' ::= | Constraint :: :: Constraint {{ tex \textsf{Constraint} }} | no_conflict :: :: no_conflict {{ tex \textsf{no\_conflict} }} | apart :: :: apart {{ tex \textsf{apart} }} + | unify :: :: unify {{ tex \textsf{unify} }} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %% Formulae %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% @@ -270,6 +271,7 @@ formula :: 'formula_' ::= | axBranch1 = axBranch2 :: :: branch_rewrite | C1 = C2 :: :: axiom_rewrite | apart ( </ ti // i /> , </ sj // j /> ) :: :: apart + | unify ( </ ti // i /> , </ sj // j /> ) = subst :: :: unify %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %% Subrules and Parsing %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% diff --git a/docs/core-spec/Makefile b/docs/core-spec/Makefile index 9449a0e1af..3dfed54e15 100644 --- a/docs/core-spec/Makefile +++ b/docs/core-spec/Makefile @@ -5,6 +5,7 @@ TARGET = core-spec $(TARGET).pdf: $(TARGET).tex $(OTT_TEX) latex -output-format=pdf $< + latex -output-format=pdf $< $(TARGET).tex: $(TARGET).mng $(OTT_FILES) ott $(OTT_OPTS) -tex_filter $< $@ $(OTT_FILES) diff --git a/docs/core-spec/core-spec.mng b/docs/core-spec/core-spec.mng index 4b1e986c6d..10ed4f7e9f 100644 --- a/docs/core-spec/core-spec.mng +++ b/docs/core-spec/core-spec.mng @@ -150,6 +150,12 @@ Axioms: \ottaxBranch } +The definition for $[[axBranch]]$ above does not include the list of +incompatible branches (field \texttt{cab\_incomps} of \texttt{CoAxBranch}), +as that would unduly clutter this presentation. Instead, as the list +of incompatible branches can be computed at any time, it is checked for +in the judgment $[[no_conflict]]$. See Section~\ref{sec:no_conflict}. + \subsection{Type constructors} Type constructors in GHC contain \emph{lots} of information. We leave most of it out @@ -306,10 +312,14 @@ There are two very similar checks for names, one declared as a local function: \ottdefnisSubKind{} \subsection{Branched axiom conflict checking} +\label{sec:no_conflict} The following judgment is used within \ottdrulename{Co\_AxiomInstCo} to make sure that a type family application cannot unify with any previous branch -in the axiom. +in the axiom. The actual code scans through only those branches that are +flagged as incompatible. These branches are stored directly in the +$[[axBranch]]$. However, it is cleaner in this presentation to simply +check for compatibility here. \ottdefncheckXXnoXXconflict{} @@ -318,4 +328,7 @@ It checks to see if \coderef{types/Unify.lhs}{tcApartTys} returns \texttt{Surely Two types are apart if neither type is a type family application and if they do not unify. +The algorithm $[[unify]]$ is implemented in \coderef{types/Unify.lhs}{tcUnifyTys}. +It performs a standard unification, returning a substitution upon success. + \end{document} diff --git a/docs/core-spec/core-spec.pdf b/docs/core-spec/core-spec.pdf Binary files differindex be13ca22c5..21de3642a3 100644 --- a/docs/core-spec/core-spec.pdf +++ b/docs/core-spec/core-spec.pdf diff --git a/docs/users_guide/glasgow_exts.xml b/docs/users_guide/glasgow_exts.xml index d9ad6a5787..710efbb1ec 100644 --- a/docs/users_guide/glasgow_exts.xml +++ b/docs/users_guide/glasgow_exts.xml @@ -4872,7 +4872,7 @@ representation).</para> <title>Type families</title> <para> - <firstterm>Indexed type families</firstterm> are a new GHC extension to + <firstterm>Indexed type families</firstterm> form an extension to facilitate type-level programming. Type families are a generalisation of <firstterm>associated data types</firstterm> @@ -4915,11 +4915,11 @@ representation).</para> indices. </para> <para> - Indexed type families come in two flavours: <firstterm>data - families</firstterm> and <firstterm>type synonym - families</firstterm>. They are the indexed family variants of algebraic - data types and type synonyms, respectively. The instances of data families - can be data types and newtypes. + Indexed type families come in three flavours: <firstterm>data + families</firstterm>, <firstterm>open type synonym families</firstterm>, and + <firstterm>closed type synonym families</firstterm>. They are the indexed + family variants of algebraic data types and type synonyms, respectively. The + instances of data families can be data types and newtypes. </para> <para> Type families are enabled by the flag <option>-XTypeFamilies</option>. @@ -5027,7 +5027,7 @@ data instance G [a] b where </para> <para> - Even if type families are defined as toplevel declarations, functions + Even if data families are defined as toplevel declarations, functions that perform different computations for different family instances may still need to be defined as methods of type classes. In particular, the following is not possible: @@ -5073,22 +5073,24 @@ instance Foo Char where <title>Synonym families</title> <para> - Type families appear in two flavours: (1) they can be defined on the - toplevel or (2) they can appear inside type classes (in which case they - are known as associated type synonyms). The former is the more general - variant, as it lacks the requirement for the type-indexes to coincide with - the class parameters. However, the latter can lead to more clearly - structured code and compiler warnings if some type instances were - - possibly accidentally - omitted. In the following, we always discuss the - general toplevel form first and then cover the additional constraints - placed on associated types. + Type families appear in three flavours: (1) they can be defined as open + families on the toplevel, (2) they can be defined as closed families on + the toplevel, or (3) they can appear inside type classes (in which case + they are known as associated type synonyms). Toplevel families are more + general, as they lack the requirement for the type-indexes to coincide + with the class parameters. However, associated type synonyms can lead to + more clearly structured code and compiler warnings if some type instances + were - possibly accidentally - omitted. In the following, we always + discuss the general toplevel forms first and then cover the additional + constraints placed on associated types. Note that closed associated type + synonyms do not exist. </para> <sect3 id="type-family-declarations"> <title>Type family declarations</title> <para> - Indexed type families are introduced by a signature, such as + Open indexed type families are introduced by a signature, such as <programlisting> type family Elem c :: * </programlisting> @@ -5124,12 +5126,7 @@ F Bool -- WRONG: unsaturated application <sect3 id="type-instance-declarations"> <title>Type instance declarations</title> <para> - There are two forms of type family instance declaration: unbranched and - branched. Branched instances list any number of alternatives, to be - checked in order from top to bottom, similarly to normal function - declarations. Unbranched instances supply only one left-hand side. - - Unbranched instance declarations of type families are very similar to + Instance declarations of type families are very similar to standard type synonym declarations. The only two differences are that the keyword <literal>type</literal> is followed by <literal>instance</literal> and that some or all of the type arguments @@ -5145,45 +5142,55 @@ type instance Elem [e] = e </para> <para> - Branched instance declarations, on the other hand, allow many different - left-hand-side type patterns. These patterns are tried in order, from - top to bottom, when simplifying a type family application. A branched instance - declaration is introduced by <literal>type instance where</literal>. For example: + Type family instance declarations are only legitimate when an + appropriate family declaration is in scope - just like class instances + require the class declaration to be visible. Moreover, each instance + declaration has to conform to the kind determined by its family + declaration, and the number of type parameters in an instance + declaration must match the number of type parameters in the family + declaration. Finally, the right-hand side of a type instance must be a + monotype (i.e., it may not include foralls) and after the expansion of + all saturated vanilla type synonyms, no synonyms, except family synonyms + may remain. + </para> + </sect3> + + <sect3 id="closed-type-families"> + <title>Closed type families</title> + <para> + A type family can also be declared with a <literal>where</literal> clause, + defining the full set of equations for that family. For example: <programlisting> -type instance where +type family F a where F Int = Double F Bool = Char F a = String </programlisting> - In this example, we declare an instance for <literal>F</literal> such - that <literal>F Int</literal> simplifies to <literal>Double</literal>, - <literal>F Bool</literal> simplifies to <literal>Char</literal>, and for - any other type <literal>a</literal> that is known not to be - <literal>Int</literal> or <literal>Bool</literal>, <literal>F - a</literal> simplifies to <literal>String</literal>. Note that GHC must - be sure that <literal>a</literal> cannot unify with - <literal>Int</literal> or <literal>Bool</literal> in that last case; if - a programmer specifies just <literal>F a</literal> in their code, GHC will - not be able to simplify the type. After all, <literal>a</literal> might later - be instantiated with <literal>Int</literal>. + A closed type family's equations are tried in order, from top to bottom, + when simplifying a type family application. In this example, we declare + an instance for <literal>F</literal> such that <literal>F Int</literal> + simplifies to <literal>Double</literal>, <literal>F Bool</literal> + simplifies to <literal>Char</literal>, and for any other type + <literal>a</literal> that is known not to be <literal>Int</literal> or + <literal>Bool</literal>, <literal>F a</literal> simplifies to + <literal>String</literal>. Note that GHC must be sure that + <literal>a</literal> cannot unify with <literal>Int</literal> or + <literal>Bool</literal> in that last case; if a programmer specifies + just <literal>F a</literal> in their code, GHC will not be able to + simplify the type. After all, <literal>a</literal> might later be + instantiated with <literal>Int</literal>. </para> <para> - Branched instances and unbranched instances may be mixed freely for the same - type family. + A closed type family's equations have the same restrictions as the + equations for an open type family instances. </para> + </sect3> + <sect3 id="type-family-examples"> + <title>Type family examples</title> <para> - Type family instance declarations are only legitimate when an - appropriate family declaration is in scope - just like class instances - require the class declaration to be visible. Moreover, each instance - declaration has to conform to the kind determined by its family - declaration, and the number of type parameters in an instance - declaration must match the number of type parameters in the family - declaration. Finally, the right-hand side of a type instance must be a - monotype (i.e., it may not include foralls) and after the expansion of - all saturated vanilla type synonyms, no synonyms, except family synonyms - may remain. Here are some examples of admissible and illegal type +Here are some examples of admissible and illegal type instances: <programlisting> type family F a :: * @@ -5192,13 +5199,11 @@ type instance F String = Char -- OK! type instance F (F a) = a -- WRONG: type parameter mentions a type family type instance F (forall a. (a, b)) = b -- WRONG: a forall type appears in a type parameter type instance F Float = forall a.a -- WRONG: right-hand side may not be a forall type -type instance where -- OK! - F (Maybe Int) = Int - F (Maybe Bool) = Bool - F (Maybe a) = String -type instance where -- WRONG: conflicts with earlier instances (see below) - F Int = Float - F a = [a] +type family H a where -- OK! + H Int = Int + H Bool = Bool + H a = String +type instance H Char = Char -- WRONG: cannot have instances of closed family type family G a b :: * -> * type instance G Int = (,) -- WRONG: must be two type parameters @@ -5207,35 +5212,83 @@ type instance G Int Char Float = Double -- WRONG: must be two type parameters </para> </sect3> <sect3 id="type-family-overlap"> - <title>Overlap of type synonym instances</title> + <title>Compatibility and apartness of type family equations</title> <para> - The unbranched instance declarations of a type family used in a single - program may only overlap if the right-hand sides of the overlapping - instances coincide for the overlapping types. More formally, two - instance declarations overlap if there is a substitution that makes - the left-hand sides of the instances syntactically the same. Whenever - that is the case, if the instances are unbranched, the right-hand - sides of the instances must also be syntactically equal under the same - substitution. This condition is independent of whether the type family - is associated or not, and it is not only a matter of consistency, but - one of type safety. Branched instances are not permitted to overlap - with any other instances, branched or unbranched. + There must be some restrictions on the equations of type families, lest + we define an ambiguous rewrite system. So, equations of open type families + are restricted to be <firstterm>compatible</firstterm>. Two type patterns + are compatible if +<orderedlist> +<listitem><para>all corresponding types in the patterns are <firstterm>apart</firstterm>, or</para></listitem> +<listitem><para>the two patterns unify producing a substitution, and the right-hand sides are equal under that substitution.</para></listitem> +</orderedlist> + Two types are considered <firstterm>apart</firstterm> if, for all possible + substitutions, the types cannot reduce to a common reduct. </para> + <para> - Here are two example to illustrate the condition under which overlap - is permitted. + The first clause of "compatible" is the more straightforward one. It says + that the patterns of two distinct type family instances cannot overlap. + For example, the following is disallowed: +<programlisting> +type instance F Int = Bool +type instance F Int = Char +</programlisting> + The second clause is a little more interesting. It says that two + overlapping type family instances are allowed if the right-hand + sides coincide in the region of overlap. Some examples help here: <programlisting> type instance F (a, Int) = [a] type instance F (Int, b) = [b] -- overlap permitted type instance G (a, Int) = [a] type instance G (Char, a) = [a] -- ILLEGAL overlap, as [Char] /= [Int] - -type instance H Int = Int -type instance where -- ILLEGAL overlap, as branched instances may not overlap - H a = a </programlisting> - </para> + Note that this compatibility condition is independent of whether the type family + is associated or not, and it is not only a matter of consistency, but + one of type safety. </para> + + <para> + The definition for "compatible" uses a notion of "apart", whose definition + in turn relies on type family reduction. This condition of "apartness", as + stated, is impossible to check, so we use this conservative approximation: + two types are considered to be apart when the two types cannot be unified, + even by a potentially infinite unifier. Allowing the unifier to be infinite + disallows the following pair of instances: +<programlisting> +type instance H x x = Int +type instance H [x] x = Bool +</programlisting> + The type patterns in this pair equal if <literal>x</literal> is replaced + by an infinite nesting of lists. Rejecting instances such as these is + necessary for type soundness. + </para> + + <para> + Compatibility also affects closed type families. When simplifying an + application of a closed type family, GHC will select an equation only + when it is sure that no incompatible previous equation will ever apply. + Here are some examples: +<programlisting> +type family F a where + F Int = Bool + F a = Char + +type family G a where + G Int = Int + G a = a +</programlisting> + In the definition for <literal>F</literal>, the two equations are + incompatible -- their patterns are not apart, and yet their + right-hand sides do not coincide. Thus, before GHC selects the + second equation, it must be sure that the first can never apply. So, + the type <literal>F a</literal> does not simplify; only a type such + as <literal>F Double</literal> will simplify to + <literal>Char</literal>. In <literal>G</literal>, on the other hand, + the two equations are compatible. Thus, GHC can ignore the first + equation when looking at the second. So, <literal>G a</literal> will + simplify to <literal>a</literal>.</para> + <para> However see <xref linkend="ghci-decls"/> for the overlap rules in GHCi.</para> </sect3> @@ -5366,10 +5419,6 @@ instance GMapKey Flob where the free indexed parameter is of a kind with a finite number of alternatives (unlike <literal>*</literal>). </para> - - <para> - Branched associated type instances are not currently supported. - </para> </sect3> <sect3 id="assoc-decl-defs"> diff --git a/ghc/InteractiveUI.hs b/ghc/InteractiveUI.hs index 7aaa1f1571..4ff822f03b 100644 --- a/ghc/InteractiveUI.hs +++ b/ghc/InteractiveUI.hs @@ -1047,7 +1047,7 @@ filterOutChildren get_thing xs Nothing -> False pprInfo :: PrintExplicitForalls - -> (TyThing, Fixity, [GHC.ClsInst], [GHC.FamInst GHC.Branched]) -> SDoc + -> (TyThing, Fixity, [GHC.ClsInst], [GHC.FamInst]) -> SDoc pprInfo pefas (thing, fixity, cls_insts, fam_insts) = pprTyThingInContextLoc pefas thing $$ show_fixity @@ -2215,7 +2215,7 @@ showBindings = do return $ maybe (text "") (pprTT pefas) mb_stuff pprTT :: PrintExplicitForalls - -> (TyThing, Fixity, [GHC.ClsInst], [GHC.FamInst GHC.Branched]) -> SDoc + -> (TyThing, Fixity, [GHC.ClsInst], [GHC.FamInst]) -> SDoc pprTT pefas (thing, fixity, _cls_insts, _fam_insts) = pprTyThing pefas thing $$ show_fixity |