From 1af0d36be801a2039ba5c3c1546f06b6dad9b7a1 Mon Sep 17 00:00:00 2001 From: Simon Peyton Jones Date: Thu, 24 Dec 2015 14:55:35 +0000 Subject: [PATCH] Refactoring only This moves code around to more sensible places. - Construction for CoAxiom is localised in FamInstEnv - orphNamesOfxx moves to CoreFVs - roughMatchTcs, instanceCantMatch moves to Unify - mkNewTypeCo moves from Coercion to FamInstEnv, and is renamed mkNewTypeCoAxiom, which makes more sense --- compiler/coreSyn/CoreFVs.hs | 103 ++++++++++++++++++++++++++++- compiler/iface/BuildTyCl.hs | 9 ++- compiler/iface/IfaceSyn.hs | 2 +- compiler/main/InteractiveEval.hs | 3 +- compiler/prelude/TysWiredIn.hs | 4 +- compiler/typecheck/Inst.hs | 1 + compiler/typecheck/TcHsType.hs | 4 +- compiler/typecheck/TcRnDriver.hs | 1 + compiler/typecheck/TcTyClsDecls.hs | 4 +- compiler/typecheck/TcType.hs | 88 +----------------------- compiler/types/CoAxiom.hs | 17 +++-- compiler/types/Coercion.hs | 23 +------ compiler/types/FamInstEnv.hs | 92 +++++++++++++++----------- compiler/types/InstEnv.hs | 58 ++++++---------- compiler/types/TyCoRep.hs | 5 +- compiler/types/Type.hs | 7 +- compiler/types/Unify.hs | 32 +++++++++ 17 files changed, 247 insertions(+), 206 deletions(-) diff --git a/compiler/coreSyn/CoreFVs.hs b/compiler/coreSyn/CoreFVs.hs index bf5d773a66..2e1c182132 100644 --- a/compiler/coreSyn/CoreFVs.hs +++ b/compiler/coreSyn/CoreFVs.hs @@ -30,11 +30,16 @@ module CoreFVs ( idRuleVars, idRuleRhsVars, stableUnfoldingVars, ruleRhsFreeVars, ruleFreeVars, rulesFreeVars, rulesFreeVarsDSet, - ruleLhsFreeIds, exprsOrphNames, + ruleLhsFreeIds, vectsFreeVars, expr_fvs, + -- * Orphan names + orphNamesOfType, orphNamesOfCo, orphNamesOfAxiom, + orphNamesOfTypes, orphNamesOfCoCon, + exprsOrphNames, orphNamesOfFamInst, + -- * Core syntax tree annotation with free variables FVAnn, -- annotation, abstract CoreExprWithFVs, -- = AnnExpr Id FVAnn @@ -59,8 +64,12 @@ import Literal ( literalType ) import Name import VarSet import Var -import TcType import Type +import TyCoRep +import TyCon +import CoAxiom +import FamInstEnv +import TysPrim( funTyConName ) import Coercion import Maybes( orElse ) import Util @@ -262,6 +271,96 @@ exprOrphNames e exprsOrphNames :: [CoreExpr] -> NameSet exprsOrphNames es = foldr (unionNameSet . exprOrphNames) emptyNameSet es + +{- ********************************************************************** +%* * + orphNamesXXX + +%* * +%********************************************************************* -} + +orphNamesOfTyCon :: TyCon -> NameSet +orphNamesOfTyCon tycon = unitNameSet (getName tycon) `unionNameSet` case tyConClass_maybe tycon of + Nothing -> emptyNameSet + Just cls -> unitNameSet (getName cls) + +orphNamesOfType :: Type -> NameSet +orphNamesOfType ty | Just ty' <- coreView ty = orphNamesOfType ty' + -- Look through type synonyms (Trac #4912) +orphNamesOfType (TyVarTy _) = emptyNameSet +orphNamesOfType (LitTy {}) = emptyNameSet +orphNamesOfType (TyConApp tycon tys) = orphNamesOfTyCon tycon + `unionNameSet` orphNamesOfTypes tys +orphNamesOfType (ForAllTy bndr res) = unitNameSet funTyConName -- NB! See Trac #8535 + `unionNameSet` orphNamesOfType (binderType bndr) + `unionNameSet` orphNamesOfType res +orphNamesOfType (AppTy fun arg) = orphNamesOfType fun `unionNameSet` orphNamesOfType arg +orphNamesOfType (CastTy ty co) = orphNamesOfType ty `unionNameSet` orphNamesOfCo co +orphNamesOfType (CoercionTy co) = orphNamesOfCo co + +orphNamesOfThings :: (a -> NameSet) -> [a] -> NameSet +orphNamesOfThings f = foldr (unionNameSet . f) emptyNameSet + +orphNamesOfTypes :: [Type] -> NameSet +orphNamesOfTypes = orphNamesOfThings orphNamesOfType + +orphNamesOfCo :: Coercion -> NameSet +orphNamesOfCo (Refl _ ty) = orphNamesOfType ty +orphNamesOfCo (TyConAppCo _ tc cos) = unitNameSet (getName tc) `unionNameSet` orphNamesOfCos cos +orphNamesOfCo (AppCo co1 co2) = orphNamesOfCo co1 `unionNameSet` orphNamesOfCo co2 +orphNamesOfCo (ForAllCo _ kind_co co) + = orphNamesOfCo kind_co `unionNameSet` orphNamesOfCo co +orphNamesOfCo (CoVarCo _) = emptyNameSet +orphNamesOfCo (AxiomInstCo con _ cos) = orphNamesOfCoCon con `unionNameSet` orphNamesOfCos cos +orphNamesOfCo (UnivCo p _ t1 t2) = orphNamesOfProv p `unionNameSet` orphNamesOfType t1 `unionNameSet` orphNamesOfType t2 +orphNamesOfCo (SymCo co) = orphNamesOfCo co +orphNamesOfCo (TransCo co1 co2) = orphNamesOfCo co1 `unionNameSet` orphNamesOfCo co2 +orphNamesOfCo (NthCo _ co) = orphNamesOfCo co +orphNamesOfCo (LRCo _ co) = orphNamesOfCo co +orphNamesOfCo (InstCo co arg) = orphNamesOfCo co `unionNameSet` orphNamesOfCo arg +orphNamesOfCo (CoherenceCo co1 co2) = orphNamesOfCo co1 `unionNameSet` orphNamesOfCo co2 +orphNamesOfCo (KindCo co) = orphNamesOfCo co +orphNamesOfCo (SubCo co) = orphNamesOfCo co +orphNamesOfCo (AxiomRuleCo _ cs) = orphNamesOfCos cs + +orphNamesOfProv :: UnivCoProvenance -> NameSet +orphNamesOfProv UnsafeCoerceProv = emptyNameSet +orphNamesOfProv (PhantomProv co) = orphNamesOfCo co +orphNamesOfProv (ProofIrrelProv co) = orphNamesOfCo co +orphNamesOfProv (PluginProv _) = emptyNameSet +orphNamesOfProv (HoleProv _) = emptyNameSet + +orphNamesOfCos :: [Coercion] -> NameSet +orphNamesOfCos = orphNamesOfThings orphNamesOfCo + +orphNamesOfCoCon :: CoAxiom br -> NameSet +orphNamesOfCoCon (CoAxiom { co_ax_tc = tc, co_ax_branches = branches }) + = orphNamesOfTyCon tc `unionNameSet` orphNamesOfCoAxBranches branches + +orphNamesOfAxiom :: CoAxiom br -> NameSet +orphNamesOfAxiom axiom + = orphNamesOfTypes (concatMap coAxBranchLHS $ fromBranches $ coAxiomBranches axiom) + `extendNameSet` getName (coAxiomTyCon axiom) + +orphNamesOfCoAxBranches :: Branches br -> NameSet +orphNamesOfCoAxBranches + = foldr (unionNameSet . orphNamesOfCoAxBranch) emptyNameSet . fromBranches + +orphNamesOfCoAxBranch :: CoAxBranch -> NameSet +orphNamesOfCoAxBranch (CoAxBranch { cab_lhs = lhs, cab_rhs = rhs }) + = orphNamesOfTypes lhs `unionNameSet` orphNamesOfType rhs + +-- | orphNamesOfAxiom collects the names of the concrete types and +-- type constructors that make up the LHS of a type family instance, +-- including the family name itself. +-- +-- For instance, given `type family Foo a b`: +-- `type instance Foo (F (G (H a))) b = ...` would yield [Foo,F,G,H] +-- +-- Used in the implementation of ":info" in GHCi. +orphNamesOfFamInst :: FamInst -> NameSet +orphNamesOfFamInst fam_inst = orphNamesOfAxiom (famInstAxiom fam_inst) + {- ************************************************************************ * * diff --git a/compiler/iface/BuildTyCl.hs b/compiler/iface/BuildTyCl.hs index d370d3712f..876c9c008d 100644 --- a/compiler/iface/BuildTyCl.hs +++ b/compiler/iface/BuildTyCl.hs @@ -17,7 +17,7 @@ module BuildTyCl ( #include "HsVersions.h" import IfaceEnv -import FamInstEnv( FamInstEnvs ) +import FamInstEnv( FamInstEnvs, mkNewTypeCoAxiom ) import TysWiredIn( isCTupleTyConName ) import PrelNames( tyConRepModOcc ) import DataCon @@ -31,7 +31,6 @@ import Class import TyCon import Type import Id -import Coercion import TcType import SrcLoc( noSrcSpan ) @@ -65,12 +64,12 @@ mkNewTyConRhs :: Name -> TyCon -> DataCon -> TcRnIf m n AlgTyConRhs -- because the latter is part of a knot, whereas the former is not. mkNewTyConRhs tycon_name tycon con = do { co_tycon_name <- newImplicitBinder tycon_name mkNewTyCoOcc - ; let co_tycon = mkNewTypeCo co_tycon_name tycon etad_tvs etad_roles etad_rhs - ; traceIf (text "mkNewTyConRhs" <+> ppr co_tycon) + ; let nt_ax = mkNewTypeCoAxiom co_tycon_name tycon etad_tvs etad_roles etad_rhs + ; traceIf (text "mkNewTyConRhs" <+> ppr nt_ax) ; return (NewTyCon { data_con = con, nt_rhs = rhs_ty, nt_etad_rhs = (etad_tvs, etad_rhs), - nt_co = co_tycon } ) } + nt_co = nt_ax } ) } -- Coreview looks through newtypes with a Nothing -- for nt_co, or uses explicit coercions otherwise where diff --git a/compiler/iface/IfaceSyn.hs b/compiler/iface/IfaceSyn.hs index b5929e0d1b..503653dd0e 100644 --- a/compiler/iface/IfaceSyn.hs +++ b/compiler/iface/IfaceSyn.hs @@ -37,6 +37,7 @@ module IfaceSyn ( #include "HsVersions.h" import IfaceType +import CoreSyn( IsOrphan ) import PprCore() -- Printing DFunArgs import Demand import Class @@ -60,7 +61,6 @@ import HsBinds import TyCon ( Role (..), Injectivity(..) ) import StaticFlags (opt_PprStyle_Debug) import Util( filterOut, filterByList ) -import InstEnv import DataCon (SrcStrictness(..), SrcUnpackedness(..)) import Lexeme (isLexSym) diff --git a/compiler/main/InteractiveEval.hs b/compiler/main/InteractiveEval.hs index eb23a60f82..7839f1b9ed 100644 --- a/compiler/main/InteractiveEval.hs +++ b/compiler/main/InteractiveEval.hs @@ -58,7 +58,8 @@ import HsSyn import HscTypes import InstEnv import IfaceEnv ( newInteractiveBinder ) -import FamInstEnv ( FamInst, orphNamesOfFamInst ) +import FamInstEnv ( FamInst ) +import CoreFVs ( orphNamesOfFamInst ) import TyCon import Type hiding( typeKind ) import TcType hiding( typeKind ) diff --git a/compiler/prelude/TysWiredIn.hs b/compiler/prelude/TysWiredIn.hs index c26521d011..3c3eab66bf 100644 --- a/compiler/prelude/TysWiredIn.hs +++ b/compiler/prelude/TysWiredIn.hs @@ -108,8 +108,8 @@ import PrelNames import TysPrim -- others: +import FamInstEnv( mkNewTypeCoAxiom ) import CoAxiom -import Coercion import Id import Constants ( mAX_TUPLE_SIZE, mAX_CTUPLE_SIZE ) import Module ( Module ) @@ -1094,7 +1094,7 @@ ipTyCon = mkClassTyCon ipTyConName kind [ip,a] [] rhs ipClass NonRecursive rhs = NewTyCon ipDataCon (mkTyVarTy a) ([], mkTyVarTy a) ipCoAxiom ipCoAxiom :: CoAxiom Unbranched -ipCoAxiom = mkNewTypeCo ipCoName ipTyCon [ip,a] [Nominal, Nominal] (mkTyVarTy a) +ipCoAxiom = mkNewTypeCoAxiom ipCoName ipTyCon [ip,a] [Nominal, Nominal] (mkTyVarTy a) where [ip,a] = mkTemplateTyVars [typeSymbolKind, liftedTypeKind] diff --git a/compiler/typecheck/Inst.hs b/compiler/typecheck/Inst.hs index 50c28db510..22f16b1f35 100644 --- a/compiler/typecheck/Inst.hs +++ b/compiler/typecheck/Inst.hs @@ -40,6 +40,7 @@ import TcEvidence import InstEnv import DataCon ( dataConWrapId ) import TysWiredIn ( heqDataCon ) +import CoreSyn ( isOrphan ) import FunDeps import TcMType import Type diff --git a/compiler/typecheck/TcHsType.hs b/compiler/typecheck/TcHsType.hs index 1200bf105c..769c45f43d 100644 --- a/compiler/typecheck/TcHsType.hs +++ b/compiler/typecheck/TcHsType.hs @@ -644,8 +644,8 @@ tc_infer_hs_type_ek mode ty ek --------------------------- tupKindSort_maybe :: TcKind -> Maybe TupleSort tupKindSort_maybe k - | Just (k', _) <- tcSplitCastTy_maybe k = tupKindSort_maybe k' - | Just k' <- coreView k = tupKindSort_maybe k' + | Just (k', _) <- splitCastTy_maybe k = tupKindSort_maybe k' + | Just k' <- coreView k = tupKindSort_maybe k' | isConstraintKind k = Just ConstraintTuple | isLiftedTypeKind k = Just BoxedTuple | otherwise = Nothing diff --git a/compiler/typecheck/TcRnDriver.hs b/compiler/typecheck/TcRnDriver.hs index 298a9533a9..8764c33dcf 100644 --- a/compiler/typecheck/TcRnDriver.hs +++ b/compiler/typecheck/TcRnDriver.hs @@ -53,6 +53,7 @@ import TcRnMonad import TcEvidence import PprTyThing( pprTyThing ) import Coercion( pprCoAxiom ) +import CoreFVs( orphNamesOfFamInst ) import FamInst import InstEnv import FamInstEnv diff --git a/compiler/typecheck/TcTyClsDecls.hs b/compiler/typecheck/TcTyClsDecls.hs index 8376176219..3f13c348c0 100644 --- a/compiler/typecheck/TcTyClsDecls.hs +++ b/compiler/typecheck/TcTyClsDecls.hs @@ -1032,7 +1032,9 @@ tcTyFamInstEqn fam_tc_shape@(fam_tc_name,_,_) mb_clsinfo ; rhs_ty <- zonkTcTypeToType emptyZonkEnv rhs_ty ; traceTc "tcTyFamInstEqn" (ppr fam_tc_name <+> pprTvBndrs tvs') -- don't print out the pats here, as they might be zonked inside the knot - ; return (mkCoAxBranch tvs' [] pats' rhs_ty loc) } + ; return (mkCoAxBranch tvs' [] pats' rhs_ty + (map (const Nominal) tvs') + loc) } kcDataDefn :: Name -- ^ the family name, for error msgs only -> HsTyPats Name -- ^ the patterns, for error msgs only diff --git a/compiler/typecheck/TcType.hs b/compiler/typecheck/TcType.hs index 82431c36c4..879f977045 100644 --- a/compiler/typecheck/TcType.hs +++ b/compiler/typecheck/TcType.hs @@ -63,7 +63,6 @@ module TcType ( tcInstHeadTyNotSynonym, tcInstHeadTyAppAllTyVars, tcGetTyVar_maybe, tcGetTyVar, nextRole, tcSplitSigmaTy, tcDeepSplitSigmaTy_maybe, - tcSplitCastTy_maybe, --------------------------------- -- Predicates. @@ -81,7 +80,7 @@ module TcType ( --------------------------------- -- Misc type manipulators deNoteType, occurCheckExpand, OccCheckResult(..), - orphNamesOfType, orphNamesOfDFunHead, orphNamesOfCo, + orphNamesOfType, orphNamesOfCo, orphNamesOfTypes, orphNamesOfCoCon, getDFunTyKey, evVarPred_maybe, evVarPred, @@ -188,10 +187,10 @@ import VarSet import Coercion import Type import TyCon -import CoAxiom -- others: import DynFlags +import CoreFVs import Name -- hiding (varName) -- We use this to make dictionaries for type literals. -- Perhaps there's a better way to do this? @@ -1226,12 +1225,6 @@ tcIsTyVarTy (CastTy ty _) = tcIsTyVarTy ty -- look through casts, as tcIsTyVarTy (TyVarTy _) = True tcIsTyVarTy _ = False ------------------------ -tcSplitCastTy_maybe :: TcType -> Maybe (TcType, Coercion) -tcSplitCastTy_maybe ty | Just ty' <- coreView ty = tcSplitCastTy_maybe ty' -tcSplitCastTy_maybe (CastTy ty co) = Just (ty, co) -tcSplitCastTy_maybe _ = Nothing - ----------------------- tcSplitDFunTy :: Type -> ([TyVar], [Type], Class, [Type]) -- Split the type of a dictionary function @@ -2011,83 +2004,6 @@ Find the free tycons and classes of a type. This is used in the front end of the compiler. -} -orphNamesOfTyCon :: TyCon -> NameSet -orphNamesOfTyCon tycon = unitNameSet (getName tycon) `unionNameSet` case tyConClass_maybe tycon of - Nothing -> emptyNameSet - Just cls -> unitNameSet (getName cls) - -orphNamesOfType :: Type -> NameSet -orphNamesOfType ty | Just ty' <- coreView ty = orphNamesOfType ty' - -- Look through type synonyms (Trac #4912) -orphNamesOfType (TyVarTy _) = emptyNameSet -orphNamesOfType (LitTy {}) = emptyNameSet -orphNamesOfType (TyConApp tycon tys) = orphNamesOfTyCon tycon - `unionNameSet` orphNamesOfTypes tys -orphNamesOfType (ForAllTy bndr res) = orphNamesOfTyCon funTyCon -- NB! See Trac #8535 - `unionNameSet` orphNamesOfType (binderType bndr) - `unionNameSet` orphNamesOfType res -orphNamesOfType (AppTy fun arg) = orphNamesOfType fun `unionNameSet` orphNamesOfType arg -orphNamesOfType (CastTy ty co) = orphNamesOfType ty `unionNameSet` orphNamesOfCo co -orphNamesOfType (CoercionTy co) = orphNamesOfCo co - -orphNamesOfThings :: (a -> NameSet) -> [a] -> NameSet -orphNamesOfThings f = foldr (unionNameSet . f) emptyNameSet - -orphNamesOfTypes :: [Type] -> NameSet -orphNamesOfTypes = orphNamesOfThings orphNamesOfType - -orphNamesOfDFunHead :: Type -> NameSet --- Find the free type constructors and classes --- of the head of the dfun instance type --- The 'dfun_head_type' is because of --- instance Foo a => Baz T where ... --- The decl is an orphan if Baz and T are both not locally defined, --- even if Foo *is* locally defined -orphNamesOfDFunHead dfun_ty - = case tcSplitSigmaTy dfun_ty of - (_, _, head_ty) -> orphNamesOfType head_ty - -orphNamesOfCo :: Coercion -> NameSet -orphNamesOfCo (Refl _ ty) = orphNamesOfType ty -orphNamesOfCo (TyConAppCo _ tc cos) = unitNameSet (getName tc) `unionNameSet` orphNamesOfCos cos -orphNamesOfCo (AppCo co1 co2) = orphNamesOfCo co1 `unionNameSet` orphNamesOfCo co2 -orphNamesOfCo (ForAllCo _ kind_co co) - = orphNamesOfCo kind_co `unionNameSet` orphNamesOfCo co -orphNamesOfCo (CoVarCo _) = emptyNameSet -orphNamesOfCo (AxiomInstCo con _ cos) = orphNamesOfCoCon con `unionNameSet` orphNamesOfCos cos -orphNamesOfCo (UnivCo p _ t1 t2) = orphNamesOfProv p `unionNameSet` orphNamesOfType t1 `unionNameSet` orphNamesOfType t2 -orphNamesOfCo (SymCo co) = orphNamesOfCo co -orphNamesOfCo (TransCo co1 co2) = orphNamesOfCo co1 `unionNameSet` orphNamesOfCo co2 -orphNamesOfCo (NthCo _ co) = orphNamesOfCo co -orphNamesOfCo (LRCo _ co) = orphNamesOfCo co -orphNamesOfCo (InstCo co arg) = orphNamesOfCo co `unionNameSet` orphNamesOfCo arg -orphNamesOfCo (CoherenceCo co1 co2) = orphNamesOfCo co1 `unionNameSet` orphNamesOfCo co2 -orphNamesOfCo (KindCo co) = orphNamesOfCo co -orphNamesOfCo (SubCo co) = orphNamesOfCo co -orphNamesOfCo (AxiomRuleCo _ cs) = orphNamesOfCos cs - -orphNamesOfProv :: UnivCoProvenance -> NameSet -orphNamesOfProv UnsafeCoerceProv = emptyNameSet -orphNamesOfProv (PhantomProv co) = orphNamesOfCo co -orphNamesOfProv (ProofIrrelProv co) = orphNamesOfCo co -orphNamesOfProv (PluginProv _) = emptyNameSet -orphNamesOfProv (HoleProv _) = emptyNameSet - -orphNamesOfCos :: [Coercion] -> NameSet -orphNamesOfCos = orphNamesOfThings orphNamesOfCo - -orphNamesOfCoCon :: CoAxiom br -> NameSet -orphNamesOfCoCon (CoAxiom { co_ax_tc = tc, co_ax_branches = branches }) - = orphNamesOfTyCon tc `unionNameSet` orphNamesOfCoAxBranches branches - -orphNamesOfCoAxBranches :: Branches br -> NameSet -orphNamesOfCoAxBranches - = foldr (unionNameSet . orphNamesOfCoAxBranch) emptyNameSet . fromBranches - -orphNamesOfCoAxBranch :: CoAxBranch -> NameSet -orphNamesOfCoAxBranch (CoAxBranch { cab_lhs = lhs, cab_rhs = rhs }) - = orphNamesOfTypes lhs `unionNameSet` orphNamesOfType rhs - {- ************************************************************************ * * diff --git a/compiler/types/CoAxiom.hs b/compiler/types/CoAxiom.hs index 01c6502f5e..3d00b14c01 100644 --- a/compiler/types/CoAxiom.hs +++ b/compiler/types/CoAxiom.hs @@ -206,11 +206,12 @@ of the branches. -- See Note [GHC Formalism] in coreSyn/CoreLint.hs data CoAxiom br = CoAxiom -- Type equality axiom. - { co_ax_unique :: Unique -- unique identifier - , co_ax_name :: Name -- name for pretty-printing - , co_ax_role :: Role -- role of the axiom's equality - , co_ax_tc :: TyCon -- the head of the LHS patterns - , co_ax_branches :: Branches br -- the branches that form this axiom + { co_ax_unique :: Unique -- Unique identifier + , co_ax_name :: Name -- Name for pretty-printing + , co_ax_role :: Role -- Role of the axiom's equality + , co_ax_tc :: TyCon -- The head of the LHS patterns + -- e.g. the newtype or family tycon + , co_ax_branches :: Branches br -- The branches that form this axiom , co_ax_implicit :: Bool -- True <=> the axiom is "implicit" -- See Note [Implicit axioms] -- INVARIANT: co_ax_implicit == True implies length co_ax_branches == 1. @@ -229,6 +230,7 @@ data CoAxBranch -- in TcTyClsDecls , cab_roles :: [Role] -- See Note [CoAxBranch roles] , cab_lhs :: [Type] -- Type patterns to match against + -- See Note [CoAxiom saturation] , cab_rhs :: Type -- Right-hand side of the equality , cab_incomps :: [CoAxBranch] -- The previous incompatible branches -- See Note [Storing compatibility] @@ -307,7 +309,10 @@ coAxBranchIncomps = cab_incomps placeHolderIncomps :: [CoAxBranch] placeHolderIncomps = panic "placeHolderIncomps" -{- +{- Note [CoAxiom saturation] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +* When co + Note [CoAxBranch type variables] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ In the case of a CoAxBranch of an associated type-family instance, diff --git a/compiler/types/Coercion.hs b/compiler/types/Coercion.hs index 277936960f..3aa56e2e04 100644 --- a/compiler/types/Coercion.hs +++ b/compiler/types/Coercion.hs @@ -34,7 +34,7 @@ module Coercion ( mkForAllCo, mkForAllCos, mkHomoForAllCos, mkHomoForAllCos_NoRefl, mkPhantomCo, mkHomoPhantomCo, toPhantomCo, mkUnsafeCo, mkHoleCo, mkUnivCo, mkSubCo, - mkNewTypeCo, mkAxiomInstCo, mkProofIrrelCo, + mkAxiomInstCo, mkProofIrrelCo, downgradeRole, maybeSubCo, mkAxiomRuleCo, mkCoherenceCo, mkCoherenceRightCo, mkCoherenceLeftCo, mkKindCo, castCoercionKind, @@ -1194,27 +1194,6 @@ castCoercionKind g h1 h2 -- See note [Newtype coercions] in TyCon --- | Create a coercion constructor (axiom) suitable for the given --- newtype 'TyCon'. The 'Name' should be that of a new coercion --- 'CoAxiom', the 'TyVar's the arguments expected by the @newtype@ and --- the type the appropriate right hand side of the @newtype@, with --- the free variables a subset of those 'TyVar's. -mkNewTypeCo :: Name -> TyCon -> [TyVar] -> [Role] -> Type -> CoAxiom Unbranched -mkNewTypeCo name tycon tvs roles rhs_ty - = CoAxiom { co_ax_unique = nameUnique name - , co_ax_name = name - , co_ax_implicit = True -- See Note [Implicit axioms] in TyCon - , co_ax_role = Representational - , co_ax_tc = tycon - , co_ax_branches = unbranched branch } - where branch = CoAxBranch { cab_loc = getSrcSpan name - , cab_tvs = tvs - , cab_cvs = [] - , cab_lhs = mkTyVarTys tvs - , cab_roles = roles - , cab_rhs = rhs_ty - , cab_incomps = [] } - mkPiCos :: Role -> [Var] -> Coercion -> Coercion mkPiCos r vs co = foldr (mkPiCo r) co vs diff --git a/compiler/types/FamInstEnv.hs b/compiler/types/FamInstEnv.hs index b5d3c21d0a..00a128d026 100644 --- a/compiler/types/FamInstEnv.hs +++ b/compiler/types/FamInstEnv.hs @@ -12,11 +12,11 @@ module FamInstEnv ( FamInstEnvs, FamInstEnv, emptyFamInstEnv, emptyFamInstEnvs, extendFamInstEnv, deleteFromFamInstEnv, extendFamInstEnvList, - identicalFamInstHead, famInstEnvElts, familyInstances, orphNamesOfFamInst, + identicalFamInstHead, famInstEnvElts, familyInstances, -- * CoAxioms mkCoAxBranch, mkBranchedCoAxiom, mkUnbranchedCoAxiom, mkSingleCoAxiom, - computeAxiomIncomps, + mkNewTypeCoAxiom, FamInstMatch(..), lookupFamInstEnv, lookupFamInstEnvConflicts, lookupFamInstEnvByTyCon, @@ -38,10 +38,8 @@ module FamInstEnv ( #include "HsVersions.h" -import InstEnv import Unify import Type -import TcType ( orphNamesOfTypes ) import TyCoRep import TyCon import Coercion @@ -59,11 +57,11 @@ import Util import Var import Pair import SrcLoc -import NameSet import FastString import MonadUtils import Control.Monad import Data.Function ( on ) +import Data.List( mapAccumL ) {- ************************************************************************ @@ -92,6 +90,12 @@ data FamInst -- See Note [FamInsts and CoAxioms] = FamInst { fi_axiom :: CoAxiom Unbranched -- The new coercion axiom -- introduced by this family -- instance + -- INVARIANT: apart from freshening (see below) + -- fi_tvs = cab_tvs of the (single) axiom branch + -- fi_cvs = cab_cvs ...ditto... + -- fi_tys = cab_lhs ...ditto... + -- fi_rhs = cab_rhs ...ditto... + , fi_flavor :: FamFlavor -- Everything below here is a redundant, @@ -106,16 +110,13 @@ data FamInst -- See Note [FamInsts and CoAxioms] -- Used for "proper matching"; ditto , fi_tvs :: [TyVar] -- Template tyvars for full match + , fi_cvs :: [CoVar] -- Template covars for full match -- Like ClsInsts, these variables are always fresh -- See Note [Template tyvars are fresh] in InstEnv - -- INVARIANT: fi_tvs = coAxiomTyVars fi_axiom - - , fi_cvs :: [CoVar] -- Template covars for full match , fi_tys :: [Type] -- The LHS type patterns -- May be eta-reduced; see Note [Eta reduction for data families] - , fi_rhs :: Type -- the RHS, with its freshened vars } @@ -159,6 +160,9 @@ Bottom line: i.e. LHS is unsaturated - fi_rhs will be (rep_tc fi_tvs) i.e. RHS is un-saturated + + But when fi_flavour = SynFamilyInst, + - fi_tys has the exact arity of the family tycon -} -- Obtain the axiom of a family instance @@ -390,21 +394,6 @@ familyInstances (pkg_fie, home_fie) fam Just (FamIE insts) -> insts Nothing -> [] --- | Collects the names of the concrete types and type constructors that --- make up the LHS of a type family instance, including the family --- name itself. --- --- For instance, given `type family Foo a b`: --- `type instance Foo (F (G (H a))) b = ...` would yield [Foo,F,G,H] --- --- Used in the implementation of ":info" in GHCi. -orphNamesOfFamInst :: FamInst -> NameSet -orphNamesOfFamInst fam_inst - = orphNamesOfTypes (concat (map cab_lhs (fromBranches $ coAxiomBranches axiom))) - `extendNameSet` getName (coAxiomTyCon axiom) - where - axiom = fi_axiom fam_inst - extendFamInstEnvList :: FamInstEnv -> [FamInst] -> FamInstEnv extendFamInstEnvList inst_env fis = foldl extendFamInstEnv inst_env fis @@ -525,7 +514,7 @@ irrelevant (clause 1 of compatible) or benign (clause 2 of compatible). compatibleBranches :: CoAxBranch -> CoAxBranch -> Bool compatibleBranches (CoAxBranch { cab_lhs = lhs1, cab_rhs = rhs1 }) (CoAxBranch { cab_lhs = lhs2, cab_rhs = rhs2 }) - = case tcUnifyTysFG instanceBindFun lhs1 lhs2 of + = case tcUnifyTysFG (const BindMe) lhs1 lhs2 of SurelyApart -> True Unifiable subst | Type.substTy subst rhs1 `eqType` Type.substTy subst rhs2 @@ -573,15 +562,19 @@ injectiveBranches injectivity -- takes a CoAxiom with unknown branch incompatibilities and computes -- the compatibilities -- See Note [Storing compatibility] in CoAxiom -computeAxiomIncomps :: CoAxiom br -> CoAxiom br -computeAxiomIncomps ax@(CoAxiom { co_ax_branches = branches }) - = ax { co_ax_branches = mapAccumBranches go branches } +computeAxiomIncomps :: [CoAxBranch] -> [CoAxBranch] +computeAxiomIncomps branches + = snd (mapAccumL go [] branches) where - go :: [CoAxBranch] -> CoAxBranch -> CoAxBranch - go prev_branches br = br { cab_incomps = mk_incomps br prev_branches } + go :: [CoAxBranch] -> CoAxBranch -> ([CoAxBranch], CoAxBranch) + go prev_brs cur_br + = (cur_br : prev_brs, new_br) + where + new_br = cur_br { cab_incomps = mk_incomps prev_brs cur_br } - mk_incomps :: CoAxBranch -> [CoAxBranch] -> [CoAxBranch] - mk_incomps br = filter (not . compatibleBranches br) + mk_incomps :: [CoAxBranch] -> CoAxBranch -> [CoAxBranch] + mk_incomps prev_brs cur_br + = filter (not . compatibleBranches cur_br) prev_brs {- ************************************************************************ @@ -589,6 +582,8 @@ computeAxiomIncomps ax@(CoAxiom { co_ax_branches = branches }) Constructing axioms These functions are here because tidyType / tcUnifyTysFG are not available in CoAxiom + + Also computeAxiomIncomps is too sophisticated for CoAxiom * * ************************************************************************ @@ -604,13 +599,14 @@ mkCoAxBranch :: [TyVar] -- original, possibly stale, tyvars -> [CoVar] -- possibly stale covars -> [Type] -- LHS patterns -> Type -- RHS + -> [Role] -> SrcSpan -> CoAxBranch -mkCoAxBranch tvs cvs lhs rhs loc +mkCoAxBranch tvs cvs lhs rhs roles loc = CoAxBranch { cab_tvs = tvs1 , cab_cvs = cvs1 , cab_lhs = tidyTypes env lhs - , cab_roles = map (const Nominal) tvs1 + , cab_roles = roles , cab_rhs = tidyType env rhs , cab_loc = loc , cab_incomps = placeHolderIncomps } @@ -623,13 +619,12 @@ mkCoAxBranch tvs cvs lhs rhs loc -- Coercion mkBranchedCoAxiom :: Name -> TyCon -> [CoAxBranch] -> CoAxiom Branched mkBranchedCoAxiom ax_name fam_tc branches - = computeAxiomIncomps $ - CoAxiom { co_ax_unique = nameUnique ax_name + = CoAxiom { co_ax_unique = nameUnique ax_name , co_ax_name = ax_name , co_ax_tc = fam_tc , co_ax_role = Nominal , co_ax_implicit = False - , co_ax_branches = manyBranches branches } + , co_ax_branches = manyBranches (computeAxiomIncomps branches) } mkUnbranchedCoAxiom :: Name -> TyCon -> CoAxBranch -> CoAxiom Unbranched mkUnbranchedCoAxiom ax_name fam_tc branch @@ -654,7 +649,26 @@ mkSingleCoAxiom role ax_name tvs cvs fam_tc lhs_tys rhs_ty , co_ax_implicit = False , co_ax_branches = unbranched (branch { cab_incomps = [] }) } where - branch = mkCoAxBranch tvs cvs lhs_tys rhs_ty (getSrcSpan ax_name) + branch = mkCoAxBranch tvs cvs lhs_tys rhs_ty + (map (const Nominal) tvs) + (getSrcSpan ax_name) + +-- | Create a coercion constructor (axiom) suitable for the given +-- newtype 'TyCon'. The 'Name' should be that of a new coercion +-- 'CoAxiom', the 'TyVar's the arguments expected by the @newtype@ and +-- the type the appropriate right hand side of the @newtype@, with +-- the free variables a subset of those 'TyVar's. +mkNewTypeCoAxiom :: Name -> TyCon -> [TyVar] -> [Role] -> Type -> CoAxiom Unbranched +mkNewTypeCoAxiom name tycon tvs roles rhs_ty + = CoAxiom { co_ax_unique = nameUnique name + , co_ax_name = name + , co_ax_implicit = True -- See Note [Implicit axioms] in TyCon + , co_ax_role = Representational + , co_ax_tc = tycon + , co_ax_branches = unbranched (branch { cab_incomps = [] }) } + where + branch = mkCoAxBranch tvs [] (mkTyVarTys tvs) rhs_ty + roles (getSrcSpan name) {- ************************************************************************ @@ -1118,7 +1132,7 @@ apartnessCheck :: [Type] -- ^ /flattened/ target arguments. Make sure -> Bool -- ^ True <=> equation can fire apartnessCheck flattened_target (CoAxBranch { cab_incomps = incomps }) = all (isSurelyApart - . tcUnifyTysFG instanceBindFun flattened_target + . tcUnifyTysFG (const BindMe) flattened_target . coAxBranchLHS) incomps where isSurelyApart SurelyApart = True diff --git a/compiler/types/InstEnv.hs b/compiler/types/InstEnv.hs index c3cd916051..b37566a772 100644 --- a/compiler/types/InstEnv.hs +++ b/compiler/types/InstEnv.hs @@ -15,29 +15,27 @@ module InstEnv ( ClsInst(..), DFunInstType, pprInstance, pprInstanceHdr, pprInstances, instanceHead, instanceSig, mkLocalInstance, mkImportedInstance, instanceDFunId, tidyClsInstDFun, instanceRoughTcs, - fuzzyClsInstCmp, - - IsOrphan(..), isOrphan, notOrphan, + fuzzyClsInstCmp, orphNamesOfClsInst, InstEnvs(..), VisibleOrphanModules, InstEnv, emptyInstEnv, extendInstEnv, deleteFromInstEnv, identicalClsInstHead, extendInstEnvList, lookupUniqueInstEnv, lookupInstEnv, instEnvElts, memberInstEnv, instIsVisible, - classInstances, orphNamesOfClsInst, instanceBindFun, + classInstances, instanceBindFun, instanceCantMatch, roughMatchTcs ) where #include "HsVersions.h" -import CoreSyn ( IsOrphan(..), isOrphan, notOrphan, chooseOrphanAnchor ) +import TcType -- InstEnv is really part of the type checker, + -- and depends on TcType in many ways +import CoreSyn ( IsOrphan(..), isOrphan, chooseOrphanAnchor ) import Module import Class import Var import VarSet import Name import NameSet -import TcType -import TyCon import Unify import Outputable import ErrUtils @@ -167,6 +165,7 @@ tidyClsInstDFun tidy_dfun ispec instanceRoughTcs :: ClsInst -> [Maybe Name] instanceRoughTcs = is_tcs + instance NamedThing ClsInst where getName ispec = getName (is_dfun ispec) @@ -196,6 +195,22 @@ instanceHead (ClsInst { is_tvs = tvs, is_tys = tys, is_dfun = dfun }) where (_, _, cls, _) = tcSplitDFunTy (idType dfun) +-- | Collects the names of concrete types and type constructors that make +-- up the head of a class instance. For instance, given `class Foo a b`: +-- +-- `instance Foo (Either (Maybe Int) a) Bool` would yield +-- [Either, Maybe, Int, Bool] +-- +-- Used in the implementation of ":info" in GHCi. +-- +-- The 'tcSplitSigmaTy' is because of +-- instance Foo a => Baz T where ... +-- The decl is an orphan if Baz and T are both not locally defined, +-- even if Foo *is* locally defined +orphNamesOfClsInst :: ClsInst -> NameSet +orphNamesOfClsInst (ClsInst { is_cls_nm = cls_nm, is_tys = tys }) + = orphNamesOfTypes tys `unionNameSet` unitNameSet cls_nm + instanceSig :: ClsInst -> ([TyVar], [Type], Class, [Type]) -- Decomposes the DFunId instanceSig ispec = tcSplitDFunTy (idType (is_dfun ispec)) @@ -258,25 +273,6 @@ mkImportedInstance cls_nm mb_tcs dfun oflag orphan where (tvs, _, cls, tys) = tcSplitDFunTy (idType dfun) -roughMatchTcs :: [Type] -> [Maybe Name] -roughMatchTcs tys = map rough tys - where - rough ty - | Just (ty', _) <- tcSplitCastTy_maybe ty = rough ty' - | Just (tc,_) <- tcSplitTyConApp_maybe ty = Just (tyConName tc) - | otherwise = Nothing - -instanceCantMatch :: [Maybe Name] -> [Maybe Name] -> Bool --- (instanceCantMatch tcs1 tcs2) returns True if tcs1 cannot --- possibly be instantiated to actual, nor vice versa; --- False is non-committal -instanceCantMatch (mt : ts) (ma : as) = itemCantMatch mt ma || instanceCantMatch ts as -instanceCantMatch _ _ = False -- Safe - -itemCantMatch :: Maybe Name -> Maybe Name -> Bool -itemCantMatch (Just t) (Just a) = t /= a -itemCantMatch _ _ = False - {- Note [When exactly is an instance decl an orphan?] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ @@ -394,16 +390,6 @@ classInstances (InstEnvs { ie_global = pkg_ie, ie_local = home_ie, ie_visible = Just (ClsIE insts) -> filter (instIsVisible vis_mods) insts Nothing -> [] --- | Collects the names of concrete types and type constructors that make --- up the head of a class instance. For instance, given `class Foo a b`: --- --- `instance Foo (Either (Maybe Int) a) Bool` would yield --- [Either, Maybe, Int, Bool] --- --- Used in the implementation of ":info" in GHCi. -orphNamesOfClsInst :: ClsInst -> NameSet -orphNamesOfClsInst = orphNamesOfDFunHead . idType . instanceDFunId - -- | Checks for an exact match of ClsInst in the instance environment. -- We use this when we do signature checking in TcRnDriver memberInstEnv :: InstEnv -> ClsInst -> Bool diff --git a/compiler/types/TyCoRep.hs b/compiler/types/TyCoRep.hs index d64b03fb5e..48f7c0f9a9 100644 --- a/compiler/types/TyCoRep.hs +++ b/compiler/types/TyCoRep.hs @@ -55,7 +55,7 @@ module TyCoRep ( pprPrefixApp, pprArrowChain, ppr_type, pprDataCons, - -- Free variables + -- * Free variables tyCoVarsOfType, tyCoVarsOfTypeDSet, tyCoVarsOfTypes, tyCoVarsOfTypesDSet, tyCoVarsBndrAcc, tyCoVarsOfTypeAcc, tyCoVarsOfTypeList, tyCoVarsOfTypesAcc, tyCoVarsOfTypesList, @@ -69,7 +69,7 @@ module TyCoRep ( closeOverKinds, tyCoVarsOfTelescope, - -- Substitutions + -- * Substitutions TCvSubst(..), TvSubstEnv, CvSubstEnv, emptyTvSubstEnv, emptyCvSubstEnv, composeTCvSubstEnv, composeTCvSubst, emptyTCvSubst, mkEmptyTCvSubst, isEmptyTCvSubst, mkTCvSubst, getTvSubstEnv, @@ -1210,6 +1210,7 @@ tyCoVarsOfTelescope [] fvs = fvs tyCoVarsOfTelescope (v:vs) fvs = tyCoVarsOfTelescope vs fvs `delVarSet` v `unionVarSet` tyCoVarsOfType (varType v) + {- %************************************************************************ %* * diff --git a/compiler/types/Type.hs b/compiler/types/Type.hs index d8064167a9..685ec830f1 100644 --- a/compiler/types/Type.hs +++ b/compiler/types/Type.hs @@ -47,7 +47,7 @@ module Type ( mkNumLitTy, isNumLitTy, mkStrLitTy, isStrLitTy, - mkCastTy, mkCoercionTy, + mkCastTy, mkCoercionTy, splitCastTy_maybe, userTypeError_maybe, pprUserTypeErrorTy, @@ -934,6 +934,11 @@ ForAllTy. The only trouble is avoiding capture. -} +splitCastTy_maybe :: Type -> Maybe (Type, Coercion) +splitCastTy_maybe ty | Just ty' <- coreView ty = splitCastTy_maybe ty' +splitCastTy_maybe (CastTy ty co) = Just (ty, co) +splitCastTy_maybe _ = Nothing + -- | Make a 'CastTy'. The Coercion must be nominal. mkCastTy :: Type -> Coercion -> Type -- Running example: diff --git a/compiler/types/Unify.hs b/compiler/types/Unify.hs index 0c2469a9ed..37c1dc4679 100644 --- a/compiler/types/Unify.hs +++ b/compiler/types/Unify.hs @@ -8,6 +8,8 @@ module Unify ( tcMatchTy, tcMatchTys, tcMatchTyX, tcMatchTysX, tcUnifyTyWithTFs, ruleMatchTyX, + -- * Rough matching + roughMatchTcs, instanceCantMatch, typesCantMatch, -- Side-effect free unification @@ -26,6 +28,7 @@ import Var import VarEnv import VarSet import Kind +import Name( Name ) import Type hiding ( getTvSubstEnv ) import Coercion hiding ( getCvSubstEnv ) import TyCon @@ -154,6 +157,35 @@ ruleMatchTyX tmpl_tvs rn_env tenv tmpl target matchBindFun :: TyCoVarSet -> TyVar -> BindFlag matchBindFun tvs tv = if tv `elemVarSet` tvs then BindMe else Skolem + +{- ********************************************************************* +* * + Rough matching +* * +********************************************************************* -} + +-- See Note [Rough match] field in InstEnv + +roughMatchTcs :: [Type] -> [Maybe Name] +roughMatchTcs tys = map rough tys + where + rough ty + | Just (ty', _) <- splitCastTy_maybe ty = rough ty' + | Just (tc,_) <- splitTyConApp_maybe ty = Just (tyConName tc) + | otherwise = Nothing + +instanceCantMatch :: [Maybe Name] -> [Maybe Name] -> Bool +-- (instanceCantMatch tcs1 tcs2) returns True if tcs1 cannot +-- possibly be instantiated to actual, nor vice versa; +-- False is non-committal +instanceCantMatch (mt : ts) (ma : as) = itemCantMatch mt ma || instanceCantMatch ts as +instanceCantMatch _ _ = False -- Safe + +itemCantMatch :: Maybe Name -> Maybe Name -> Bool +itemCantMatch (Just t) (Just a) = t /= a +itemCantMatch _ _ = False + + {- ************************************************************************ * * -- GitLab