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

@@ -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)
+
 {-
 ************************************************************************
 *                                                                      *

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

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)
 

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 )

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]
 

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

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

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

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

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
-
 {-
 ************************************************************************
 *                                                                      *

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,

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
 

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