never executed always true always false
    1 {-# LANGUAGE DeriveFunctor       #-}
    2 {-# LANGUAGE GADTs               #-}
    3 {-# LANGUAGE ScopedTypeVariables #-}
    4 {-# LANGUAGE TupleSections       #-}
    5 
    6 {-# OPTIONS_GHC -Wno-incomplete-record-updates #-}
    7 -- (c) The University of Glasgow 2006
    8 --
    9 -- FamInstEnv: Type checked family instance declarations
   10 
   11 module GHC.Core.FamInstEnv (
   12         FamInst(..), FamFlavor(..), famInstAxiom, famInstTyCon, famInstRHS,
   13         famInstsRepTyCons, famInstRepTyCon_maybe, dataFamInstRepTyCon,
   14         pprFamInst, pprFamInsts,
   15         mkImportedFamInst,
   16 
   17         FamInstEnvs, FamInstEnv, emptyFamInstEnv, emptyFamInstEnvs,
   18         extendFamInstEnv, extendFamInstEnvList,
   19         famInstEnvElts, famInstEnvSize, familyInstances,
   20 
   21         -- * CoAxioms
   22         mkCoAxBranch, mkBranchedCoAxiom, mkUnbranchedCoAxiom, mkSingleCoAxiom,
   23         mkNewTypeCoAxiom,
   24 
   25         FamInstMatch(..),
   26         lookupFamInstEnv, lookupFamInstEnvConflicts, lookupFamInstEnvByTyCon,
   27 
   28         isDominatedBy, apartnessCheck,
   29 
   30         -- Injectivity
   31         InjectivityCheckResult(..),
   32         lookupFamInstEnvInjectivityConflicts, injectiveBranches,
   33 
   34         -- Normalisation
   35         topNormaliseType, topNormaliseType_maybe,
   36         normaliseType, normaliseTcApp,
   37         topReduceTyFamApp_maybe, reduceTyFamApp_maybe
   38     ) where
   39 
   40 import GHC.Prelude
   41 
   42 import GHC.Core.Unify
   43 import GHC.Core.Type as Type
   44 import GHC.Core.TyCo.Rep
   45 import GHC.Core.TyCon
   46 import GHC.Core.Coercion
   47 import GHC.Core.Coercion.Axiom
   48 import GHC.Core.Reduction
   49 import GHC.Types.Var.Set
   50 import GHC.Types.Var.Env
   51 import GHC.Types.Name
   52 import GHC.Types.Unique.DFM
   53 import GHC.Data.Maybe
   54 import GHC.Types.Var
   55 import GHC.Types.SrcLoc
   56 import Control.Monad
   57 import Data.List( mapAccumL )
   58 import Data.Array( Array, assocs )
   59 
   60 import GHC.Utils.Misc
   61 import GHC.Utils.Outputable
   62 import GHC.Utils.Panic
   63 import GHC.Utils.Panic.Plain
   64 
   65 {-
   66 ************************************************************************
   67 *                                                                      *
   68           Type checked family instance heads
   69 *                                                                      *
   70 ************************************************************************
   71 
   72 Note [FamInsts and CoAxioms]
   73 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~
   74 * CoAxioms and FamInsts are just like
   75   DFunIds  and ClsInsts
   76 
   77 * A CoAxiom is a System-FC thing: it can relate any two types
   78 
   79 * A FamInst is a Haskell source-language thing, corresponding
   80   to a type/data family instance declaration.
   81     - The FamInst contains a CoAxiom, which is the evidence
   82       for the instance
   83 
   84     - The LHS of the CoAxiom is always of form F ty1 .. tyn
   85       where F is a type family
   86 -}
   87 
   88 data FamInst  -- See Note [FamInsts and CoAxioms]
   89   = FamInst { fi_axiom  :: CoAxiom Unbranched -- The new coercion axiom
   90                                               -- introduced by this family
   91                                               -- instance
   92                  -- INVARIANT: apart from freshening (see below)
   93                  --    fi_tvs = cab_tvs of the (single) axiom branch
   94                  --    fi_cvs = cab_cvs ...ditto...
   95                  --    fi_tys = cab_lhs ...ditto...
   96                  --    fi_rhs = cab_rhs ...ditto...
   97 
   98             , fi_flavor :: FamFlavor
   99 
  100             -- Everything below here is a redundant,
  101             -- cached version of the two things above
  102             -- except that the TyVars are freshened
  103             , fi_fam   :: Name          -- Family name
  104 
  105                 -- Used for "rough matching"; same idea as for class instances
  106                 -- See Note [Rough matching in class and family instances]
  107                 -- in GHC.Core.Unify
  108             , fi_tcs   :: [RoughMatchTc]  -- Top of type args
  109                 -- INVARIANT: fi_tcs = roughMatchTcs fi_tys
  110 
  111             -- Used for "proper matching"; ditto
  112             , fi_tvs :: [TyVar]      -- Template tyvars for full match
  113             , fi_cvs :: [CoVar]      -- Template covars for full match
  114                  -- Like ClsInsts, these variables are always fresh
  115                  -- See Note [Template tyvars are fresh] in GHC.Core.InstEnv
  116 
  117             , fi_tys    :: [Type]       --   The LHS type patterns
  118             -- May be eta-reduced; see Note [Eta reduction for data families]
  119             -- in GHC.Core.Coercion.Axiom
  120 
  121             , fi_rhs :: Type         --   the RHS, with its freshened vars
  122             }
  123 
  124 data FamFlavor
  125   = SynFamilyInst         -- A synonym family
  126   | DataFamilyInst TyCon  -- A data family, with its representation TyCon
  127 
  128 {-
  129 Note [Arity of data families]
  130 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
  131 Data family instances might legitimately be over- or under-saturated.
  132 
  133 Under-saturation has two potential causes:
  134  U1) Eta reduction. See Note [Eta reduction for data families] in
  135      GHC.Core.Coercion.Axiom.
  136  U2) When the user has specified a return kind instead of written out patterns.
  137      Example:
  138 
  139        data family Sing (a :: k)
  140        data instance Sing :: Bool -> Type
  141 
  142      The data family tycon Sing has an arity of 2, the k and the a. But
  143      the data instance has only one pattern, Bool (standing in for k).
  144      This instance is equivalent to `data instance Sing (a :: Bool)`, but
  145      without the last pattern, we have an under-saturated data family instance.
  146      On its own, this example is not compelling enough to add support for
  147      under-saturation, but U1 makes this feature more compelling.
  148 
  149 Over-saturation is also possible:
  150   O1) If the data family's return kind is a type variable (see also #12369),
  151       an instance might legitimately have more arguments than the family.
  152       Example:
  153 
  154         data family Fix :: (Type -> k) -> k
  155         data instance Fix f = MkFix1 (f (Fix f))
  156         data instance Fix f x = MkFix2 (f (Fix f x) x)
  157 
  158       In the first instance here, the k in the data family kind is chosen to
  159       be Type. In the second, it's (Type -> Type).
  160 
  161       However, we require that any over-saturation is eta-reducible. That is,
  162       we require that any extra patterns be bare unrepeated type variables;
  163       see Note [Eta reduction for data families] in GHC.Core.Coercion.Axiom.
  164       Accordingly, the FamInst is never over-saturated.
  165 
  166 Why can we allow such flexibility for data families but not for type families?
  167 Because data families can be decomposed -- that is, they are generative and
  168 injective. A Type family is neither and so always must be applied to all its
  169 arguments.
  170 -}
  171 
  172 -- Obtain the axiom of a family instance
  173 famInstAxiom :: FamInst -> CoAxiom Unbranched
  174 famInstAxiom = fi_axiom
  175 
  176 -- Split the left-hand side of the FamInst
  177 famInstSplitLHS :: FamInst -> (TyCon, [Type])
  178 famInstSplitLHS (FamInst { fi_axiom = axiom, fi_tys = lhs })
  179   = (coAxiomTyCon axiom, lhs)
  180 
  181 -- Get the RHS of the FamInst
  182 famInstRHS :: FamInst -> Type
  183 famInstRHS = fi_rhs
  184 
  185 -- Get the family TyCon of the FamInst
  186 famInstTyCon :: FamInst -> TyCon
  187 famInstTyCon = coAxiomTyCon . famInstAxiom
  188 
  189 -- Return the representation TyCons introduced by data family instances, if any
  190 famInstsRepTyCons :: [FamInst] -> [TyCon]
  191 famInstsRepTyCons fis = [tc | FamInst { fi_flavor = DataFamilyInst tc } <- fis]
  192 
  193 -- Extracts the TyCon for this *data* (or newtype) instance
  194 famInstRepTyCon_maybe :: FamInst -> Maybe TyCon
  195 famInstRepTyCon_maybe fi
  196   = case fi_flavor fi of
  197        DataFamilyInst tycon -> Just tycon
  198        SynFamilyInst        -> Nothing
  199 
  200 dataFamInstRepTyCon :: FamInst -> TyCon
  201 dataFamInstRepTyCon fi
  202   = case fi_flavor fi of
  203        DataFamilyInst tycon -> tycon
  204        SynFamilyInst        -> pprPanic "dataFamInstRepTyCon" (ppr fi)
  205 
  206 {-
  207 ************************************************************************
  208 *                                                                      *
  209         Pretty printing
  210 *                                                                      *
  211 ************************************************************************
  212 -}
  213 
  214 instance NamedThing FamInst where
  215    getName = coAxiomName . fi_axiom
  216 
  217 instance Outputable FamInst where
  218    ppr = pprFamInst
  219 
  220 pprFamInst :: FamInst -> SDoc
  221 -- Prints the FamInst as a family instance declaration
  222 -- NB: This function, FamInstEnv.pprFamInst, is used only for internal,
  223 --     debug printing. See GHC.Types.TyThing.Ppr.pprFamInst for printing for the user
  224 pprFamInst (FamInst { fi_flavor = flavor, fi_axiom = ax
  225                     , fi_tvs = tvs, fi_tys = tys, fi_rhs = rhs })
  226   = hang (ppr_tc_sort <+> text "instance"
  227              <+> pprCoAxBranchUser (coAxiomTyCon ax) (coAxiomSingleBranch ax))
  228        2 (whenPprDebug debug_stuff)
  229   where
  230     ppr_tc_sort = case flavor of
  231                      SynFamilyInst             -> text "type"
  232                      DataFamilyInst tycon
  233                        | isDataTyCon     tycon -> text "data"
  234                        | isNewTyCon      tycon -> text "newtype"
  235                        | isAbstractTyCon tycon -> text "data"
  236                        | otherwise             -> text "WEIRD" <+> ppr tycon
  237 
  238     debug_stuff = vcat [ text "Coercion axiom:" <+> ppr ax
  239                        , text "Tvs:" <+> ppr tvs
  240                        , text "LHS:" <+> ppr tys
  241                        , text "RHS:" <+> ppr rhs ]
  242 
  243 pprFamInsts :: [FamInst] -> SDoc
  244 pprFamInsts finsts = vcat (map pprFamInst finsts)
  245 
  246 {-
  247 Note [Lazy axiom match]
  248 ~~~~~~~~~~~~~~~~~~~~~~~
  249 It is Vitally Important that mkImportedFamInst is *lazy* in its axiom
  250 parameter. The axiom is loaded lazily, via a forkM, in GHC.IfaceToCore. Sometime
  251 later, mkImportedFamInst is called using that axiom. However, the axiom
  252 may itself depend on entities which are not yet loaded as of the time
  253 of the mkImportedFamInst. Thus, if mkImportedFamInst eagerly looks at the
  254 axiom, a dependency loop spontaneously appears and GHC hangs. The solution
  255 is simply for mkImportedFamInst never, ever to look inside of the axiom
  256 until everything else is good and ready to do so. We can assume that this
  257 readiness has been achieved when some other code pulls on the axiom in the
  258 FamInst. Thus, we pattern match on the axiom lazily (in the where clause,
  259 not in the parameter list) and we assert the consistency of names there
  260 also.
  261 -}
  262 
  263 -- Make a family instance representation from the information found in an
  264 -- interface file.  In particular, we get the rough match info from the iface
  265 -- (instead of computing it here).
  266 mkImportedFamInst :: Name               -- Name of the family
  267                   -> [RoughMatchTc]     -- Rough match info
  268                   -> CoAxiom Unbranched -- Axiom introduced
  269                   -> FamInst            -- Resulting family instance
  270 mkImportedFamInst fam mb_tcs axiom
  271   = FamInst {
  272       fi_fam    = fam,
  273       fi_tcs    = mb_tcs,
  274       fi_tvs    = tvs,
  275       fi_cvs    = cvs,
  276       fi_tys    = tys,
  277       fi_rhs    = rhs,
  278       fi_axiom  = axiom,
  279       fi_flavor = flavor }
  280   where
  281      -- See Note [Lazy axiom match]
  282      ~(CoAxBranch { cab_lhs = tys
  283                   , cab_tvs = tvs
  284                   , cab_cvs = cvs
  285                   , cab_rhs = rhs }) = coAxiomSingleBranch axiom
  286 
  287          -- Derive the flavor for an imported FamInst rather disgustingly
  288          -- Maybe we should store it in the IfaceFamInst?
  289      flavor = case splitTyConApp_maybe rhs of
  290                 Just (tc, _)
  291                   | Just ax' <- tyConFamilyCoercion_maybe tc
  292                   , ax' == axiom
  293                   -> DataFamilyInst tc
  294                 _ -> SynFamilyInst
  295 
  296 {-
  297 ************************************************************************
  298 *                                                                      *
  299                 FamInstEnv
  300 *                                                                      *
  301 ************************************************************************
  302 
  303 Note [FamInstEnv]
  304 ~~~~~~~~~~~~~~~~~
  305 A FamInstEnv maps a family name to the list of known instances for that family.
  306 
  307 The same FamInstEnv includes both 'data family' and 'type family' instances.
  308 Type families are reduced during type inference, but not data families;
  309 the user explains when to use a data family instance by using constructors
  310 and pattern matching.
  311 
  312 Nevertheless it is still useful to have data families in the FamInstEnv:
  313 
  314  - For finding overlaps and conflicts
  315 
  316  - For finding the representation type...see FamInstEnv.topNormaliseType
  317    and its call site in GHC.Core.Opt.Simplify
  318 
  319  - In standalone deriving instance Eq (T [Int]) we need to find the
  320    representation type for T [Int]
  321 
  322 Note [Varying number of patterns for data family axioms]
  323 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
  324 For data families, the number of patterns may vary between instances.
  325 For example
  326    data family T a b
  327    data instance T Int a = T1 a | T2
  328    data instance T Bool [a] = T3 a
  329 
  330 Then we get a data type for each instance, and an axiom:
  331    data TInt a = T1 a | T2
  332    data TBoolList a = T3 a
  333 
  334    axiom ax7   :: T Int ~ TInt   -- Eta-reduced
  335    axiom ax8 a :: T Bool [a] ~ TBoolList a
  336 
  337 These two axioms for T, one with one pattern, one with two;
  338 see Note [Eta reduction for data families] in GHC.Core.Coercion.Axiom
  339 
  340 Note [FamInstEnv determinism]
  341 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
  342 We turn FamInstEnvs into a list in some places that don't directly affect
  343 the ABI. That happens in family consistency checks and when producing output
  344 for `:info`. Unfortunately that nondeterminism is nonlocal and it's hard
  345 to tell what it affects without following a chain of functions. It's also
  346 easy to accidentally make that nondeterminism affect the ABI. Furthermore
  347 the envs should be relatively small, so it should be free to use deterministic
  348 maps here. Testing with nofib and validate detected no difference between
  349 UniqFM and UniqDFM.
  350 See Note [Deterministic UniqFM].
  351 -}
  352 
  353 -- Internally we sometimes index by Name instead of TyCon despite
  354 -- of what the type says. This is safe since
  355 -- getUnique (tyCon) == getUniqe (tcName tyCon)
  356 type FamInstEnv = UniqDFM TyCon FamilyInstEnv  -- Maps a family to its instances
  357      -- See Note [FamInstEnv]
  358      -- See Note [FamInstEnv determinism]
  359 
  360 type FamInstEnvs = (FamInstEnv, FamInstEnv)
  361      -- External package inst-env, Home-package inst-env
  362 
  363 newtype FamilyInstEnv
  364   = FamIE [FamInst]     -- The instances for a particular family, in any order
  365 
  366 instance Outputable FamilyInstEnv where
  367   ppr (FamIE fs) = text "FamIE" <+> vcat (map ppr fs)
  368 
  369 -- | Index a FamInstEnv by the tyCons name.
  370 toNameInstEnv :: FamInstEnv -> UniqDFM Name FamilyInstEnv
  371 toNameInstEnv = unsafeCastUDFMKey
  372 
  373 -- | Create a FamInstEnv from Name indices.
  374 fromNameInstEnv :: UniqDFM Name FamilyInstEnv -> FamInstEnv
  375 fromNameInstEnv = unsafeCastUDFMKey
  376 
  377 -- INVARIANTS:
  378 --  * The fs_tvs are distinct in each FamInst
  379 --      of a range value of the map (so we can safely unify them)
  380 
  381 emptyFamInstEnvs :: (FamInstEnv, FamInstEnv)
  382 emptyFamInstEnvs = (emptyFamInstEnv, emptyFamInstEnv)
  383 
  384 emptyFamInstEnv :: FamInstEnv
  385 emptyFamInstEnv = emptyUDFM
  386 
  387 famInstEnvElts :: FamInstEnv -> [FamInst]
  388 famInstEnvElts fi = [elt | FamIE elts <- eltsUDFM fi, elt <- elts]
  389   -- See Note [FamInstEnv determinism]
  390 
  391 famInstEnvSize :: FamInstEnv -> Int
  392 famInstEnvSize = nonDetStrictFoldUDFM (\(FamIE elt) sum -> sum + length elt) 0
  393   -- It's OK to use nonDetStrictFoldUDFM here since we're just computing the
  394   -- size.
  395 
  396 familyInstances :: (FamInstEnv, FamInstEnv) -> TyCon -> [FamInst]
  397 familyInstances (pkg_fie, home_fie) fam
  398   = get home_fie ++ get pkg_fie
  399   where
  400     get env = case lookupUDFM env fam of
  401                 Just (FamIE insts) -> insts
  402                 Nothing                      -> []
  403 
  404 extendFamInstEnvList :: FamInstEnv -> [FamInst] -> FamInstEnv
  405 extendFamInstEnvList inst_env fis = foldl' extendFamInstEnv inst_env fis
  406 
  407 extendFamInstEnv :: FamInstEnv -> FamInst -> FamInstEnv
  408 extendFamInstEnv inst_env
  409                  ins_item@(FamInst {fi_fam = cls_nm})
  410   = fromNameInstEnv $ addToUDFM_C add (toNameInstEnv inst_env) cls_nm (FamIE [ins_item])
  411   where
  412     add (FamIE items) _ = FamIE (ins_item:items)
  413 
  414 {-
  415 ************************************************************************
  416 *                                                                      *
  417                 Compatibility
  418 *                                                                      *
  419 ************************************************************************
  420 
  421 Note [Apartness]
  422 ~~~~~~~~~~~~~~~~
  423 In dealing with closed type families, we must be able to check that one type
  424 will never reduce to another. This check is called /apartness/. The check
  425 is always between a target (which may be an arbitrary type) and a pattern.
  426 Here is how we do it:
  427 
  428 apart(target, pattern) = not (unify(flatten(target), pattern))
  429 
  430 where flatten (implemented in flattenTys, below) converts all type-family
  431 applications into fresh variables. (See
  432 Note [Flattening type-family applications when matching instances] in GHC.Core.Unify.)
  433 
  434 Note [Compatibility]
  435 ~~~~~~~~~~~~~~~~~~~~
  436 Two patterns are /compatible/ if either of the following conditions hold:
  437 1) The patterns are apart.
  438 2) The patterns unify with a substitution S, and their right hand sides
  439 equal under that substitution.
  440 
  441 For open type families, only compatible instances are allowed. For closed
  442 type families, the story is slightly more complicated. Consider the following:
  443 
  444 type family F a where
  445   F Int = Bool
  446   F a   = Int
  447 
  448 g :: Show a => a -> F a
  449 g x = length (show x)
  450 
  451 Should that type-check? No. We need to allow for the possibility that 'a'
  452 might be Int and therefore 'F a' should be Bool. We can simplify 'F a' to Int
  453 only when we can be sure that 'a' is not Int.
  454 
  455 To achieve this, after finding a possible match within the equations, we have to
  456 go back to all previous equations and check that, under the
  457 substitution induced by the match, other branches are surely apart. (See
  458 Note [Apartness].) This is similar to what happens with class
  459 instance selection, when we need to guarantee that there is only a match and
  460 no unifiers. The exact algorithm is different here because the
  461 potentially-overlapping group is closed.
  462 
  463 As another example, consider this:
  464 
  465 type family G x where
  466   G Int = Bool
  467   G a   = Double
  468 
  469 type family H y
  470 -- no instances
  471 
  472 Now, we want to simplify (G (H Char)). We can't, because (H Char) might later
  473 simplify to be Int. So, (G (H Char)) is stuck, for now.
  474 
  475 While everything above is quite sound, it isn't as expressive as we'd like.
  476 Consider this:
  477 
  478 type family J a where
  479   J Int = Int
  480   J a   = a
  481 
  482 Can we simplify (J b) to b? Sure we can. Yes, the first equation matches if
  483 b is instantiated with Int, but the RHSs coincide there, so it's all OK.
  484 
  485 So, the rule is this: when looking up a branch in a closed type family, we
  486 find a branch that matches the target, but then we make sure that the target
  487 is apart from every previous *incompatible* branch. We don't check the
  488 branches that are compatible with the matching branch, because they are either
  489 irrelevant (clause 1 of compatible) or benign (clause 2 of compatible).
  490 
  491 Note [Compatibility of eta-reduced axioms]
  492 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
  493 In newtype instances of data families we eta-reduce the axioms,
  494 See Note [Eta reduction for data families] in GHC.Core.Coercion.Axiom. This means that
  495 we sometimes need to test compatibility of two axioms that were eta-reduced to
  496 different degrees, e.g.:
  497 
  498 
  499 data family D a b c
  500 newtype instance D a Int c = DInt (Maybe a)
  501   -- D a Int ~ Maybe
  502   -- lhs = [a, Int]
  503 newtype instance D Bool Int Char = DIntChar Float
  504   -- D Bool Int Char ~ Float
  505   -- lhs = [Bool, Int, Char]
  506 
  507 These are obviously incompatible. We could detect this by saturating
  508 (eta-expanding) the shorter LHS with fresh tyvars until the lists are of
  509 equal length, but instead we can just remove the tail of the longer list, as
  510 those types will simply unify with the freshly introduced tyvars.
  511 
  512 By doing this, in case the LHS are unifiable, the yielded substitution won't
  513 mention the tyvars that appear in the tail we dropped off, and we might try
  514 to test equality RHSes of different kinds, but that's fine since this case
  515 occurs only for data families, where the RHS is a unique tycon and the equality
  516 fails anyway.
  517 -}
  518 
  519 -- See Note [Compatibility]
  520 compatibleBranches :: CoAxBranch -> CoAxBranch -> Bool
  521 compatibleBranches (CoAxBranch { cab_lhs = lhs1, cab_rhs = rhs1 })
  522                    (CoAxBranch { cab_lhs = lhs2, cab_rhs = rhs2 })
  523   = let (commonlhs1, commonlhs2) = zipAndUnzip lhs1 lhs2
  524              -- See Note [Compatibility of eta-reduced axioms]
  525     in case tcUnifyTysFG alwaysBindFun commonlhs1 commonlhs2 of
  526       SurelyApart -> True
  527       Unifiable subst
  528         | Type.substTyAddInScope subst rhs1 `eqType`
  529           Type.substTyAddInScope subst rhs2
  530         -> True
  531       _ -> False
  532 
  533 -- | Result of testing two type family equations for injectiviy.
  534 data InjectivityCheckResult
  535    = InjectivityAccepted
  536     -- ^ Either RHSs are distinct or unification of RHSs leads to unification of
  537     -- LHSs
  538    | InjectivityUnified CoAxBranch CoAxBranch
  539     -- ^ RHSs unify but LHSs don't unify under that substitution.  Relevant for
  540     -- closed type families where equation after unification might be
  541     -- overlpapped (in which case it is OK if they don't unify).  Constructor
  542     -- stores axioms after unification.
  543 
  544 -- | Check whether two type family axioms don't violate injectivity annotation.
  545 injectiveBranches :: [Bool] -> CoAxBranch -> CoAxBranch
  546                   -> InjectivityCheckResult
  547 injectiveBranches injectivity
  548                   ax1@(CoAxBranch { cab_lhs = lhs1, cab_rhs = rhs1 })
  549                   ax2@(CoAxBranch { cab_lhs = lhs2, cab_rhs = rhs2 })
  550   -- See Note [Verifying injectivity annotation], case 1.
  551   = let getInjArgs  = filterByList injectivity
  552     in case tcUnifyTyWithTFs True rhs1 rhs2 of -- True = two-way pre-unification
  553        Nothing -> InjectivityAccepted
  554          -- RHS are different, so equations are injective.
  555          -- This is case 1A from Note [Verifying injectivity annotation]
  556        Just subst -> -- RHS unify under a substitution
  557         let lhs1Subst = Type.substTys subst (getInjArgs lhs1)
  558             lhs2Subst = Type.substTys subst (getInjArgs lhs2)
  559         -- If LHSs are equal under the substitution used for RHSs then this pair
  560         -- of equations does not violate injectivity annotation. If LHSs are not
  561         -- equal under that substitution then this pair of equations violates
  562         -- injectivity annotation, but for closed type families it still might
  563         -- be the case that one LHS after substitution is unreachable.
  564         in if eqTypes lhs1Subst lhs2Subst  -- check case 1B1 from Note.
  565            then InjectivityAccepted
  566            else InjectivityUnified ( ax1 { cab_lhs = Type.substTys subst lhs1
  567                                          , cab_rhs = Type.substTy  subst rhs1 })
  568                                    ( ax2 { cab_lhs = Type.substTys subst lhs2
  569                                          , cab_rhs = Type.substTy  subst rhs2 })
  570                 -- payload of InjectivityUnified used only for check 1B2, only
  571                 -- for closed type families
  572 
  573 -- takes a CoAxiom with unknown branch incompatibilities and computes
  574 -- the compatibilities
  575 -- See Note [Storing compatibility] in GHC.Core.Coercion.Axiom
  576 computeAxiomIncomps :: [CoAxBranch] -> [CoAxBranch]
  577 computeAxiomIncomps branches
  578   = snd (mapAccumL go [] branches)
  579   where
  580     go :: [CoAxBranch] -> CoAxBranch -> ([CoAxBranch], CoAxBranch)
  581     go prev_brs cur_br
  582        = (cur_br : prev_brs, new_br)
  583        where
  584          new_br = cur_br { cab_incomps = mk_incomps prev_brs cur_br }
  585 
  586     mk_incomps :: [CoAxBranch] -> CoAxBranch -> [CoAxBranch]
  587     mk_incomps prev_brs cur_br
  588        = filter (not . compatibleBranches cur_br) prev_brs
  589 
  590 {-
  591 ************************************************************************
  592 *                                                                      *
  593            Constructing axioms
  594     These functions are here because tidyType / tcUnifyTysFG
  595     are not available in GHC.Core.Coercion.Axiom
  596 
  597     Also computeAxiomIncomps is too sophisticated for CoAxiom
  598 *                                                                      *
  599 ************************************************************************
  600 
  601 Note [Tidy axioms when we build them]
  602 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
  603 Like types and classes, we build axioms fully quantified over all
  604 their variables, and tidy them when we build them. For example,
  605 we print out axioms and don't want to print stuff like
  606     F k k a b = ...
  607 Instead we must tidy those kind variables.  See #7524.
  608 
  609 We could instead tidy when we print, but that makes it harder to get
  610 things like injectivity errors to come out right. Danger of
  611      Type family equation violates injectivity annotation.
  612      Kind variable ‘k’ cannot be inferred from the right-hand side.
  613      In the type family equation:
  614         PolyKindVars @[k1] @[k2] ('[] @k1) = '[] @k2
  615 
  616 Note [Always number wildcard types in CoAxBranch]
  617 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
  618 Consider the following example (from the DataFamilyInstanceLHS test case):
  619 
  620   data family Sing (a :: k)
  621   data instance Sing (_ :: MyKind) where
  622       SingA :: Sing A
  623       SingB :: Sing B
  624 
  625 If we're not careful during tidying, then when this program is compiled with
  626 -ddump-types, we'll get the following information:
  627 
  628   COERCION AXIOMS
  629     axiom DataFamilyInstanceLHS.D:R:SingMyKind_0 ::
  630       Sing _ = DataFamilyInstanceLHS.R:SingMyKind_ _
  631 
  632 It's misleading to have a wildcard type appearing on the RHS like
  633 that. To avoid this issue, when building a CoAxiom (which is what eventually
  634 gets printed above), we tidy all the variables in an env that already contains
  635 '_'. Thus, any variable named '_' will be renamed, giving us the nicer output
  636 here:
  637 
  638   COERCION AXIOMS
  639     axiom DataFamilyInstanceLHS.D:R:SingMyKind_0 ::
  640       Sing _1 = DataFamilyInstanceLHS.R:SingMyKind_ _1
  641 
  642 Which is at least legal syntax.
  643 
  644 See also Note [CoAxBranch type variables] in GHC.Core.Coercion.Axiom; note that we
  645 are tidying (changing OccNames only), not freshening, in accordance with
  646 that Note.
  647 -}
  648 
  649 -- all axiom roles are Nominal, as this is only used with type families
  650 mkCoAxBranch :: [TyVar] -- original, possibly stale, tyvars
  651              -> [TyVar] -- Extra eta tyvars
  652              -> [CoVar] -- possibly stale covars
  653              -> [Type]  -- LHS patterns
  654              -> Type    -- RHS
  655              -> [Role]
  656              -> SrcSpan
  657              -> CoAxBranch
  658 mkCoAxBranch tvs eta_tvs cvs lhs rhs roles loc
  659   = CoAxBranch { cab_tvs     = tvs'
  660                , cab_eta_tvs = eta_tvs'
  661                , cab_cvs     = cvs'
  662                , cab_lhs     = tidyTypes env lhs
  663                , cab_roles   = roles
  664                , cab_rhs     = tidyType env rhs
  665                , cab_loc     = loc
  666                , cab_incomps = placeHolderIncomps }
  667   where
  668     (env1, tvs')     = tidyVarBndrs init_tidy_env tvs
  669     (env2, eta_tvs') = tidyVarBndrs env1          eta_tvs
  670     (env,  cvs')     = tidyVarBndrs env2          cvs
  671     -- See Note [Tidy axioms when we build them]
  672     -- See also Note [CoAxBranch type variables] in GHC.Core.Coercion.Axiom
  673 
  674     init_occ_env = initTidyOccEnv [mkTyVarOcc "_"]
  675     init_tidy_env = mkEmptyTidyEnv init_occ_env
  676     -- See Note [Always number wildcard types in CoAxBranch]
  677 
  678 -- all of the following code is here to avoid mutual dependencies with
  679 -- Coercion
  680 mkBranchedCoAxiom :: Name -> TyCon -> [CoAxBranch] -> CoAxiom Branched
  681 mkBranchedCoAxiom ax_name fam_tc branches
  682   = CoAxiom { co_ax_unique   = nameUnique ax_name
  683             , co_ax_name     = ax_name
  684             , co_ax_tc       = fam_tc
  685             , co_ax_role     = Nominal
  686             , co_ax_implicit = False
  687             , co_ax_branches = manyBranches (computeAxiomIncomps branches) }
  688 
  689 mkUnbranchedCoAxiom :: Name -> TyCon -> CoAxBranch -> CoAxiom Unbranched
  690 mkUnbranchedCoAxiom ax_name fam_tc branch
  691   = CoAxiom { co_ax_unique   = nameUnique ax_name
  692             , co_ax_name     = ax_name
  693             , co_ax_tc       = fam_tc
  694             , co_ax_role     = Nominal
  695             , co_ax_implicit = False
  696             , co_ax_branches = unbranched (branch { cab_incomps = [] }) }
  697 
  698 mkSingleCoAxiom :: Role -> Name
  699                 -> [TyVar] -> [TyVar] -> [CoVar]
  700                 -> TyCon -> [Type] -> Type
  701                 -> CoAxiom Unbranched
  702 -- Make a single-branch CoAxiom, including making the branch itself
  703 -- Used for both type family (Nominal) and data family (Representational)
  704 -- axioms, hence passing in the Role
  705 mkSingleCoAxiom role ax_name tvs eta_tvs cvs fam_tc lhs_tys rhs_ty
  706   = CoAxiom { co_ax_unique   = nameUnique ax_name
  707             , co_ax_name     = ax_name
  708             , co_ax_tc       = fam_tc
  709             , co_ax_role     = role
  710             , co_ax_implicit = False
  711             , co_ax_branches = unbranched (branch { cab_incomps = [] }) }
  712   where
  713     branch = mkCoAxBranch tvs eta_tvs cvs lhs_tys rhs_ty
  714                           (map (const Nominal) tvs)
  715                           (getSrcSpan ax_name)
  716 
  717 -- | Create a coercion constructor (axiom) suitable for the given
  718 --   newtype 'TyCon'. The 'Name' should be that of a new coercion
  719 --   'CoAxiom', the 'TyVar's the arguments expected by the @newtype@ and
  720 --   the type the appropriate right hand side of the @newtype@, with
  721 --   the free variables a subset of those 'TyVar's.
  722 mkNewTypeCoAxiom :: Name -> TyCon -> [TyVar] -> [Role] -> Type -> CoAxiom Unbranched
  723 mkNewTypeCoAxiom name tycon tvs roles rhs_ty
  724   = CoAxiom { co_ax_unique   = nameUnique name
  725             , co_ax_name     = name
  726             , co_ax_implicit = True  -- See Note [Implicit axioms] in GHC.Core.TyCon
  727             , co_ax_role     = Representational
  728             , co_ax_tc       = tycon
  729             , co_ax_branches = unbranched (branch { cab_incomps = [] }) }
  730   where
  731     branch = mkCoAxBranch tvs [] [] (mkTyVarTys tvs) rhs_ty
  732                           roles (getSrcSpan name)
  733 
  734 {-
  735 ************************************************************************
  736 *                                                                      *
  737                 Looking up a family instance
  738 *                                                                      *
  739 ************************************************************************
  740 
  741 @lookupFamInstEnv@ looks up in a @FamInstEnv@, using a one-way match.
  742 Multiple matches are only possible in case of type families (not data
  743 families), and then, it doesn't matter which match we choose (as the
  744 instances are guaranteed confluent).
  745 
  746 We return the matching family instances and the type instance at which it
  747 matches.  For example, if we lookup 'T [Int]' and have a family instance
  748 
  749   data instance T [a] = ..
  750 
  751 desugared to
  752 
  753   data :R42T a = ..
  754   coe :Co:R42T a :: T [a] ~ :R42T a
  755 
  756 we return the matching instance '(FamInst{.., fi_tycon = :R42T}, Int)'.
  757 -}
  758 
  759 -- when matching a type family application, we get a FamInst,
  760 -- and the list of types the axiom should be applied to
  761 data FamInstMatch = FamInstMatch { fim_instance :: FamInst
  762                                  , fim_tys      :: [Type]
  763                                  , fim_cos      :: [Coercion]
  764                                  }
  765   -- See Note [Over-saturated matches]
  766 
  767 instance Outputable FamInstMatch where
  768   ppr (FamInstMatch { fim_instance = inst
  769                     , fim_tys      = tys
  770                     , fim_cos      = cos })
  771     = text "match with" <+> parens (ppr inst) <+> ppr tys <+> ppr cos
  772 
  773 lookupFamInstEnvByTyCon :: FamInstEnvs -> TyCon -> [FamInst]
  774 lookupFamInstEnvByTyCon (pkg_ie, home_ie) fam_tc
  775   = get pkg_ie ++ get home_ie
  776   where
  777     get ie = case lookupUDFM ie fam_tc of
  778                Nothing          -> []
  779                Just (FamIE fis) -> fis
  780 
  781 lookupFamInstEnv
  782     :: FamInstEnvs
  783     -> TyCon -> [Type]          -- What we are looking for
  784     -> [FamInstMatch]           -- Successful matches
  785 -- Precondition: the tycon is saturated (or over-saturated)
  786 
  787 lookupFamInstEnv
  788    = lookup_fam_inst_env match
  789    where
  790      match _ _ tpl_tys tys = tcMatchTys tpl_tys tys
  791 
  792 lookupFamInstEnvConflicts
  793     :: FamInstEnvs
  794     -> FamInst          -- Putative new instance
  795     -> [FamInstMatch]   -- Conflicting matches (don't look at the fim_tys field)
  796 -- E.g. when we are about to add
  797 --    f : type instance F [a] = a->a
  798 -- we do (lookupFamInstConflicts f [b])
  799 -- to find conflicting matches
  800 --
  801 -- Precondition: the tycon is saturated (or over-saturated)
  802 
  803 lookupFamInstEnvConflicts envs fam_inst@(FamInst { fi_axiom = new_axiom })
  804   = lookup_fam_inst_env my_unify envs fam tys
  805   where
  806     (fam, tys) = famInstSplitLHS fam_inst
  807         -- In example above,   fam tys' = F [b]
  808 
  809     my_unify (FamInst { fi_axiom = old_axiom }) tpl_tvs tpl_tys _
  810        = assertPpr (tyCoVarsOfTypes tys `disjointVarSet` tpl_tvs)
  811                    ((ppr fam <+> ppr tys) $$
  812                     (ppr tpl_tvs <+> ppr tpl_tys)) $
  813                 -- Unification will break badly if the variables overlap
  814                 -- They shouldn't because we allocate separate uniques for them
  815          if compatibleBranches (coAxiomSingleBranch old_axiom) new_branch
  816            then Nothing
  817            else Just noSubst
  818       -- Note [Family instance overlap conflicts]
  819 
  820     noSubst = panic "lookupFamInstEnvConflicts noSubst"
  821     new_branch = coAxiomSingleBranch new_axiom
  822 
  823 --------------------------------------------------------------------------------
  824 --                 Type family injectivity checking bits                      --
  825 --------------------------------------------------------------------------------
  826 
  827 {- Note [Verifying injectivity annotation]
  828 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
  829 
  830 Injectivity means that the RHS of a type family uniquely determines the LHS (see
  831 Note [Type inference for type families with injectivity]).  The user informs us about
  832 injectivity using an injectivity annotation and it is GHC's task to verify that
  833 this annotation is correct w.r.t. type family equations. Whenever we see a new
  834 equation of a type family we need to make sure that adding this equation to the
  835 already known equations of a type family does not violate the injectivity annotation
  836 supplied by the user (see Note [Injectivity annotation]).  Of course if the type
  837 family has no injectivity annotation then no check is required.  But if a type
  838 family has injectivity annotation we need to make sure that the following
  839 conditions hold:
  840 
  841 1. For each pair of *different* equations of a type family, one of the following
  842    conditions holds:
  843 
  844    A:  RHSs are different. (Check done in GHC.Core.FamInstEnv.injectiveBranches)
  845 
  846    B1: OPEN TYPE FAMILIES: If the RHSs can be unified under some substitution
  847        then it must be possible to unify the LHSs under the same substitution.
  848        Example:
  849 
  850           type family FunnyId a = r | r -> a
  851           type instance FunnyId Int = Int
  852           type instance FunnyId a = a
  853 
  854        RHSs of these two equations unify under [ a |-> Int ] substitution.
  855        Under this substitution LHSs are equal therefore these equations don't
  856        violate injectivity annotation. (Check done in GHC.Core.FamInstEnv.injectiveBranches)
  857 
  858    B2: CLOSED TYPE FAMILIES: If the RHSs can be unified under some
  859        substitution then either the LHSs unify under the same substitution or
  860        the LHS of the latter equation is overlapped by earlier equations.
  861        Example 1:
  862 
  863           type family SwapIntChar a = r | r -> a where
  864               SwapIntChar Int  = Char
  865               SwapIntChar Char = Int
  866               SwapIntChar a    = a
  867 
  868        Say we are checking the last two equations. RHSs unify under [ a |->
  869        Int ] substitution but LHSs don't. So we apply the substitution to LHS
  870        of last equation and check whether it is overlapped by any of previous
  871        equations. Since it is overlapped by the first equation we conclude
  872        that pair of last two equations does not violate injectivity
  873        annotation. (Check done in GHC.Tc.Validity.checkValidCoAxiom#gather_conflicts)
  874 
  875    A special case of B is when RHSs unify with an empty substitution ie. they
  876    are identical.
  877 
  878    If any of the above two conditions holds we conclude that the pair of
  879    equations does not violate injectivity annotation. But if we find a pair
  880    of equations where neither of the above holds we report that this pair
  881    violates injectivity annotation because for a given RHS we don't have a
  882    unique LHS. (Note that (B) actually implies (A).)
  883 
  884    Note that we only take into account these LHS patterns that were declared
  885    as injective.
  886 
  887 2. If an RHS of a type family equation is a bare type variable then
  888    all LHS variables (including implicit kind variables) also have to be bare.
  889    In other words, this has to be a sole equation of that type family and it has
  890    to cover all possible patterns.  So for example this definition will be
  891    rejected:
  892 
  893       type family W1 a = r | r -> a
  894       type instance W1 [a] = a
  895 
  896    If it were accepted we could call `W1 [W1 Int]`, which would reduce to
  897    `W1 Int` and then by injectivity we could conclude that `[W1 Int] ~ Int`,
  898    which is bogus. Checked FamInst.bareTvInRHSViolated.
  899 
  900 3. If the RHS of a type family equation is a type family application then the type
  901    family is rejected as not injective. This is checked by FamInst.isTFHeaded.
  902 
  903 4. If a LHS type variable that is declared as injective is not mentioned in an
  904    injective position in the RHS then the type family is rejected as not
  905    injective.  "Injective position" means either an argument to a type
  906    constructor or argument to a type family on injective position.
  907    There are subtleties here. See Note [Coverage condition for injective type families]
  908    in GHC.Tc.Instance.Family.
  909 
  910 Check (1) must be done for all family instances (transitively) imported. Other
  911 checks (2-4) should be done just for locally written equations, as they are checks
  912 involving just a single equation, not about interactions. Doing the other checks for
  913 imported equations led to #17405, as the behavior of check (4) depends on
  914 -XUndecidableInstances (see Note [Coverage condition for injective type families] in
  915 FamInst), which may vary between modules.
  916 
  917 See also Note [Injective type families] in GHC.Core.TyCon
  918 -}
  919 
  920 
  921 -- | Check whether an open type family equation can be added to already existing
  922 -- instance environment without causing conflicts with supplied injectivity
  923 -- annotations.  Returns list of conflicting axioms (type instance
  924 -- declarations).
  925 lookupFamInstEnvInjectivityConflicts
  926     :: [Bool]         -- injectivity annotation for this type family instance
  927                       -- INVARIANT: list contains at least one True value
  928     ->  FamInstEnvs   -- all type instances seens so far
  929     ->  FamInst       -- new type instance that we're checking
  930     -> [CoAxBranch]   -- conflicting instance declarations
  931 lookupFamInstEnvInjectivityConflicts injList (pkg_ie, home_ie)
  932                              fam_inst@(FamInst { fi_axiom = new_axiom })
  933   -- See Note [Verifying injectivity annotation]. This function implements
  934   -- check (1.B1) for open type families described there.
  935   = lookup_inj_fam_conflicts home_ie ++ lookup_inj_fam_conflicts pkg_ie
  936     where
  937       fam        = famInstTyCon fam_inst
  938       new_branch = coAxiomSingleBranch new_axiom
  939 
  940       -- filtering function used by `lookup_inj_fam_conflicts` to check whether
  941       -- a pair of equations conflicts with the injectivity annotation.
  942       isInjConflict (FamInst { fi_axiom = old_axiom })
  943           | InjectivityAccepted <-
  944             injectiveBranches injList (coAxiomSingleBranch old_axiom) new_branch
  945           = False -- no conflict
  946           | otherwise = True
  947 
  948       lookup_inj_fam_conflicts ie
  949           | isOpenFamilyTyCon fam, Just (FamIE insts) <- lookupUDFM ie fam
  950           = map (coAxiomSingleBranch . fi_axiom) $
  951             filter isInjConflict insts
  952           | otherwise = []
  953 
  954 
  955 --------------------------------------------------------------------------------
  956 --                    Type family overlap checking bits                       --
  957 --------------------------------------------------------------------------------
  958 
  959 {-
  960 Note [Family instance overlap conflicts]
  961 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
  962 - In the case of data family instances, any overlap is fundamentally a
  963   conflict (as these instances imply injective type mappings).
  964 
  965 - In the case of type family instances, overlap is admitted as long as
  966   the right-hand sides of the overlapping rules coincide under the
  967   overlap substitution.  eg
  968        type instance F a Int = a
  969        type instance F Int b = b
  970   These two overlap on (F Int Int) but then both RHSs are Int,
  971   so all is well. We require that they are syntactically equal;
  972   anything else would be difficult to test for at this stage.
  973 -}
  974 
  975 ------------------------------------------------------------
  976 -- Might be a one-way match or a unifier
  977 type MatchFun =  FamInst                -- The FamInst template
  978               -> TyVarSet -> [Type]     --   fi_tvs, fi_tys of that FamInst
  979               -> [Type]                 -- Target to match against
  980               -> Maybe TCvSubst
  981 
  982 lookup_fam_inst_env'          -- The worker, local to this module
  983     :: MatchFun
  984     -> FamInstEnv
  985     -> TyCon -> [Type]        -- What we are looking for
  986     -> [FamInstMatch]
  987 lookup_fam_inst_env' match_fun ie fam match_tys
  988   | isOpenFamilyTyCon fam
  989   , Just (FamIE insts) <- lookupUDFM ie fam
  990   = find insts    -- The common case
  991   | otherwise = []
  992   where
  993 
  994     find [] = []
  995     find (item@(FamInst { fi_tcs = mb_tcs, fi_tvs = tpl_tvs, fi_cvs = tpl_cvs
  996                         , fi_tys = tpl_tys }) : rest)
  997         -- Fast check for no match, uses the "rough match" fields
  998       | instanceCantMatch rough_tcs mb_tcs
  999       = find rest
 1000 
 1001         -- Proper check
 1002       | Just subst <- match_fun item (mkVarSet tpl_tvs) tpl_tys match_tys1
 1003       = (FamInstMatch { fim_instance = item
 1004                       , fim_tys      = substTyVars subst tpl_tvs `chkAppend` match_tys2
 1005                       , fim_cos      = assert (all (isJust . lookupCoVar subst) tpl_cvs) $
 1006                                        substCoVars subst tpl_cvs
 1007                       })
 1008         : find rest
 1009 
 1010         -- No match => try next
 1011       | otherwise
 1012       = find rest
 1013       where
 1014         (rough_tcs, match_tys1, match_tys2) = split_tys tpl_tys
 1015 
 1016       -- Precondition: the tycon is saturated (or over-saturated)
 1017 
 1018     -- Deal with over-saturation
 1019     -- See Note [Over-saturated matches]
 1020     split_tys tpl_tys
 1021       | isTypeFamilyTyCon fam
 1022       = pre_rough_split_tys
 1023 
 1024       | otherwise
 1025       = let (match_tys1, match_tys2) = splitAtList tpl_tys match_tys
 1026             rough_tcs = roughMatchTcs match_tys1
 1027         in (rough_tcs, match_tys1, match_tys2)
 1028 
 1029     (pre_match_tys1, pre_match_tys2) = splitAt (tyConArity fam) match_tys
 1030     pre_rough_split_tys
 1031       = (roughMatchTcs pre_match_tys1, pre_match_tys1, pre_match_tys2)
 1032 
 1033 lookup_fam_inst_env           -- The worker, local to this module
 1034     :: MatchFun
 1035     -> FamInstEnvs
 1036     -> TyCon -> [Type]        -- What we are looking for
 1037     -> [FamInstMatch]         -- Successful matches
 1038 
 1039 -- Precondition: the tycon is saturated (or over-saturated)
 1040 
 1041 lookup_fam_inst_env match_fun (pkg_ie, home_ie) fam tys
 1042   =  lookup_fam_inst_env' match_fun home_ie fam tys
 1043   ++ lookup_fam_inst_env' match_fun pkg_ie  fam tys
 1044 
 1045 {-
 1046 Note [Over-saturated matches]
 1047 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 1048 It's ok to look up an over-saturated type constructor.  E.g.
 1049      type family F a :: * -> *
 1050      type instance F (a,b) = Either (a->b)
 1051 
 1052 The type instance gives rise to a newtype TyCon (at a higher kind
 1053 which you can't do in Haskell!):
 1054      newtype FPair a b = FP (Either (a->b))
 1055 
 1056 Then looking up (F (Int,Bool) Char) will return a FamInstMatch
 1057      (FPair, [Int,Bool,Char])
 1058 The "extra" type argument [Char] just stays on the end.
 1059 
 1060 We handle data families and type families separately here:
 1061 
 1062  * For type families, all instances of a type family must have the
 1063    same arity, so we can precompute the split between the match_tys
 1064    and the overflow tys. This is done in pre_rough_split_tys.
 1065 
 1066  * For data family instances, though, we need to re-split for each
 1067    instance, because the breakdown might be different for each
 1068    instance.  Why?  Because of eta reduction; see
 1069    Note [Eta reduction for data families] in GHC.Core.Coercion.Axiom.
 1070 -}
 1071 
 1072 -- checks if one LHS is dominated by a list of other branches
 1073 -- in other words, if an application would match the first LHS, it is guaranteed
 1074 -- to match at least one of the others. The RHSs are ignored.
 1075 -- This algorithm is conservative:
 1076 --   True -> the LHS is definitely covered by the others
 1077 --   False -> no information
 1078 -- It is currently (Oct 2012) used only for generating errors for
 1079 -- inaccessible branches. If these errors go unreported, no harm done.
 1080 -- This is defined here to avoid a dependency from CoAxiom to Unify
 1081 isDominatedBy :: CoAxBranch -> [CoAxBranch] -> Bool
 1082 isDominatedBy branch branches
 1083   = or $ map match branches
 1084     where
 1085       lhs = coAxBranchLHS branch
 1086       match (CoAxBranch { cab_lhs = tys })
 1087         = isJust $ tcMatchTys tys lhs
 1088 
 1089 {-
 1090 ************************************************************************
 1091 *                                                                      *
 1092                 Choosing an axiom application
 1093 *                                                                      *
 1094 ************************************************************************
 1095 
 1096 The lookupFamInstEnv function does a nice job for *open* type families,
 1097 but we also need to handle closed ones when normalising a type:
 1098 -}
 1099 
 1100 reduceTyFamApp_maybe :: FamInstEnvs
 1101                      -> Role              -- Desired role of result coercion
 1102                      -> TyCon -> [Type]
 1103                      -> Maybe Reduction
 1104 -- Attempt to do a *one-step* reduction of a type-family application
 1105 --    but *not* newtypes
 1106 -- Works on type-synonym families always; data-families only if
 1107 --     the role we seek is representational
 1108 -- It does *not* normalise the type arguments first, so this may not
 1109 --     go as far as you want. If you want normalised type arguments,
 1110 --     use topReduceTyFamApp_maybe
 1111 --
 1112 -- The TyCon can be oversaturated.
 1113 -- Works on both open and closed families
 1114 --
 1115 -- Always returns a *homogeneous* coercion -- type family reductions are always
 1116 -- homogeneous
 1117 reduceTyFamApp_maybe envs role tc tys
 1118   | Phantom <- role
 1119   = Nothing
 1120 
 1121   | case role of
 1122       Representational -> isOpenFamilyTyCon     tc
 1123       _                -> isOpenTypeFamilyTyCon tc
 1124        -- If we seek a representational coercion
 1125        -- (e.g. the call in topNormaliseType_maybe) then we can
 1126        -- unwrap data families as well as type-synonym families;
 1127        -- otherwise only type-synonym families
 1128   , FamInstMatch { fim_instance = FamInst { fi_axiom = ax }
 1129                  , fim_tys      = inst_tys
 1130                  , fim_cos      = inst_cos } : _ <- lookupFamInstEnv envs tc tys
 1131       -- NB: Allow multiple matches because of compatible overlap
 1132 
 1133   = let co = mkUnbranchedAxInstCo role ax inst_tys inst_cos
 1134     in Just $ coercionRedn co
 1135 
 1136   | Just ax <- isClosedSynFamilyTyConWithAxiom_maybe tc
 1137   , Just (ind, inst_tys, inst_cos) <- chooseBranch ax tys
 1138   = let co = mkAxInstCo role ax ind inst_tys inst_cos
 1139     in Just $ coercionRedn co
 1140 
 1141   | Just ax           <- isBuiltInSynFamTyCon_maybe tc
 1142   , Just (coax,ts,ty) <- sfMatchFam ax tys
 1143   , role == coaxrRole coax
 1144   = let co = mkAxiomRuleCo coax (zipWith mkReflCo (coaxrAsmpRoles coax) ts)
 1145     in Just $ mkReduction co ty
 1146 
 1147   | otherwise
 1148   = Nothing
 1149 
 1150 -- The axiom can be oversaturated. (Closed families only.)
 1151 chooseBranch :: CoAxiom Branched -> [Type]
 1152              -> Maybe (BranchIndex, [Type], [Coercion])  -- found match, with args
 1153 chooseBranch axiom tys
 1154   = do { let num_pats = coAxiomNumPats axiom
 1155              (target_tys, extra_tys) = splitAt num_pats tys
 1156              branches = coAxiomBranches axiom
 1157        ; (ind, inst_tys, inst_cos)
 1158            <- findBranch (unMkBranches branches) target_tys
 1159        ; return ( ind, inst_tys `chkAppend` extra_tys, inst_cos ) }
 1160 
 1161 -- The axiom must *not* be oversaturated
 1162 findBranch :: Array BranchIndex CoAxBranch
 1163            -> [Type]
 1164            -> Maybe (BranchIndex, [Type], [Coercion])
 1165     -- coercions relate requested types to returned axiom LHS at role N
 1166 findBranch branches target_tys
 1167   = foldr go Nothing (assocs branches)
 1168   where
 1169     go :: (BranchIndex, CoAxBranch)
 1170        -> Maybe (BranchIndex, [Type], [Coercion])
 1171        -> Maybe (BranchIndex, [Type], [Coercion])
 1172     go (index, branch) other
 1173       = let (CoAxBranch { cab_tvs = tpl_tvs, cab_cvs = tpl_cvs
 1174                         , cab_lhs = tpl_lhs
 1175                         , cab_incomps = incomps }) = branch
 1176             in_scope = mkInScopeSet (unionVarSets $
 1177                             map (tyCoVarsOfTypes . coAxBranchLHS) incomps)
 1178             -- See Note [Flattening type-family applications when matching instances]
 1179             -- in GHC.Core.Unify
 1180             flattened_target = flattenTys in_scope target_tys
 1181         in case tcMatchTys tpl_lhs target_tys of
 1182         Just subst -- matching worked. now, check for apartness.
 1183           |  apartnessCheck flattened_target branch
 1184           -> -- matching worked & we're apart from all incompatible branches.
 1185              -- success
 1186              assert (all (isJust . lookupCoVar subst) tpl_cvs) $
 1187              Just (index, substTyVars subst tpl_tvs, substCoVars subst tpl_cvs)
 1188 
 1189         -- failure. keep looking
 1190         _ -> other
 1191 
 1192 -- | Do an apartness check, as described in the "Closed Type Families" paper
 1193 -- (POPL '14). This should be used when determining if an equation
 1194 -- ('CoAxBranch') of a closed type family can be used to reduce a certain target
 1195 -- type family application.
 1196 apartnessCheck :: [Type]
 1197   -- ^ /flattened/ target arguments. Make sure they're flattened! See
 1198   -- Note [Flattening type-family applications when matching instances]
 1199   -- in GHC.Core.Unify.
 1200                -> CoAxBranch -- ^ the candidate equation we wish to use
 1201                              -- Precondition: this matches the target
 1202                -> Bool       -- ^ True <=> equation can fire
 1203 apartnessCheck flattened_target (CoAxBranch { cab_incomps = incomps })
 1204   = all (isSurelyApart
 1205          . tcUnifyTysFG alwaysBindFun flattened_target
 1206          . coAxBranchLHS) incomps
 1207   where
 1208     isSurelyApart SurelyApart = True
 1209     isSurelyApart _           = False
 1210 
 1211 {-
 1212 ************************************************************************
 1213 *                                                                      *
 1214                 Looking up a family instance
 1215 *                                                                      *
 1216 ************************************************************************
 1217 
 1218 Note [Normalising types]
 1219 ~~~~~~~~~~~~~~~~~~~~~~~~
 1220 The topNormaliseType function removes all occurrences of type families
 1221 and newtypes from the top-level structure of a type. normaliseTcApp does
 1222 the type family lookup and is fairly straightforward. normaliseType is
 1223 a little more involved.
 1224 
 1225 The complication comes from the fact that a type family might be used in the
 1226 kind of a variable bound in a forall. We wish to remove this type family
 1227 application, but that means coming up with a fresh variable (with the new
 1228 kind). Thus, we need a substitution to be built up as we recur through the
 1229 type. However, an ordinary TCvSubst just won't do: when we hit a type variable
 1230 whose kind has changed during normalisation, we need both the new type
 1231 variable *and* the coercion. We could conjure up a new VarEnv with just this
 1232 property, but a usable substitution environment already exists:
 1233 LiftingContexts from the liftCoSubst family of functions, defined in GHC.Core.Coercion.
 1234 A LiftingContext maps a type variable to a coercion and a coercion variable to
 1235 a pair of coercions. Let's ignore coercion variables for now. Because the
 1236 coercion a type variable maps to contains the destination type (via
 1237 coercionKind), we don't need to store that destination type separately. Thus,
 1238 a LiftingContext has what we need: a map from type variables to (Coercion,
 1239 Type) pairs.
 1240 
 1241 We also benefit because we can piggyback on the liftCoSubstVarBndr function to
 1242 deal with binders. However, I had to modify that function to work with this
 1243 application. Thus, we now have liftCoSubstVarBndrUsing, which takes
 1244 a function used to process the kind of the binder. We don't wish
 1245 to lift the kind, but instead normalise it. So, we pass in a callback function
 1246 that processes the kind of the binder.
 1247 
 1248 After that brilliant explanation of all this, I'm sure you've forgotten the
 1249 dangling reference to coercion variables. What do we do with those? Nothing at
 1250 all. The point of normalising types is to remove type family applications, but
 1251 there's no sense in removing these from coercions. We would just get back a
 1252 new coercion witnessing the equality between the same types as the original
 1253 coercion. Because coercions are irrelevant anyway, there is no point in doing
 1254 this. So, whenever we encounter a coercion, we just say that it won't change.
 1255 That's what the CoercionTy case is doing within normalise_type.
 1256 
 1257 Note [Normalisation and type synonyms]
 1258 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 1259 We need to be a bit careful about normalising in the presence of type
 1260 synonyms (#13035).  Suppose S is a type synonym, and we have
 1261    S t1 t2
 1262 If S is family-free (on its RHS) we can just normalise t1 and t2 and
 1263 reconstruct (S t1' t2').   Expanding S could not reveal any new redexes
 1264 because type families are saturated.
 1265 
 1266 But if S has a type family on its RHS we expand /before/ normalising
 1267 the args t1, t2.  If we normalise t1, t2 first, we'll re-normalise them
 1268 after expansion, and that can lead to /exponential/ behaviour; see #13035.
 1269 
 1270 Notice, though, that expanding first can in principle duplicate t1,t2,
 1271 which might contain redexes. I'm sure you could conjure up an exponential
 1272 case by that route too, but it hasn't happened in practice yet!
 1273 -}
 1274 
 1275 topNormaliseType :: FamInstEnvs -> Type -> Type
 1276 topNormaliseType env ty
 1277   = case topNormaliseType_maybe env ty of
 1278       Just redn -> reductionReducedType redn
 1279       Nothing   -> ty
 1280 
 1281 topNormaliseType_maybe :: FamInstEnvs -> Type -> Maybe Reduction
 1282 
 1283 -- ^ Get rid of *outermost* (or toplevel)
 1284 --      * type function redex
 1285 --      * data family redex
 1286 --      * newtypes
 1287 -- returning an appropriate Representational coercion.  Specifically, if
 1288 --   topNormaliseType_maybe env ty = Just (co, ty')
 1289 -- then
 1290 --   (a) co :: ty ~R ty'
 1291 --   (b) ty' is not a newtype, and is not a type-family or data-family redex
 1292 --
 1293 -- However, ty' can be something like (Maybe (F ty)), where
 1294 -- (F ty) is a redex.
 1295 --
 1296 -- Always operates homogeneously: the returned type has the same kind as the
 1297 -- original type, and the returned coercion is always homogeneous.
 1298 topNormaliseType_maybe env ty
 1299   = do { ((co, mkind_co), nty) <- topNormaliseTypeX stepper combine ty
 1300        ; let hredn = mkHetReduction (mkReduction co nty) mkind_co
 1301        ; return $ homogeniseHetRedn Representational hredn }
 1302   where
 1303     stepper = unwrapNewTypeStepper' `composeSteppers` tyFamStepper
 1304 
 1305     combine (c1, mc1) (c2, mc2) = (c1 `mkTransCo` c2, mc1 `mkTransMCo` mc2)
 1306 
 1307     unwrapNewTypeStepper' :: NormaliseStepper (Coercion, MCoercionN)
 1308     unwrapNewTypeStepper' rec_nts tc tys
 1309       = mapStepResult (, MRefl) $ unwrapNewTypeStepper rec_nts tc tys
 1310 
 1311       -- second coercion below is the kind coercion relating the original type's kind
 1312       -- to the normalised type's kind
 1313     tyFamStepper :: NormaliseStepper (Coercion, MCoercionN)
 1314     tyFamStepper rec_nts tc tys  -- Try to step a type/data family
 1315       = case topReduceTyFamApp_maybe env tc tys of
 1316           Just (HetReduction (Reduction co rhs) res_co)
 1317             -> NS_Step rec_nts rhs (co, res_co)
 1318           _ -> NS_Done
 1319 
 1320 ---------------
 1321 normaliseTcApp :: FamInstEnvs -> Role -> TyCon -> [Type] -> Reduction
 1322 -- See comments on normaliseType for the arguments of this function
 1323 normaliseTcApp env role tc tys
 1324   = initNormM env role (tyCoVarsOfTypes tys) $
 1325     normalise_tc_app tc tys
 1326 
 1327 -- See Note [Normalising types] about the LiftingContext
 1328 normalise_tc_app :: TyCon -> [Type] -> NormM Reduction
 1329 normalise_tc_app tc tys
 1330   | Just (tenv, rhs, tys') <- expandSynTyCon_maybe tc tys
 1331   , not (isFamFreeTyCon tc)  -- Expand and try again
 1332   = -- A synonym with type families in the RHS
 1333     -- Expand and try again
 1334     -- See Note [Normalisation and type synonyms]
 1335     normalise_type (mkAppTys (substTy (mkTvSubstPrs tenv) rhs) tys')
 1336 
 1337   | isFamilyTyCon tc
 1338   = -- A type-family application
 1339     do { env <- getEnv
 1340        ; role <- getRole
 1341        ; ArgsReductions redns@(Reductions args_cos ntys) res_co <- normalise_tc_args tc tys
 1342        ; case reduceTyFamApp_maybe env role tc ntys of
 1343            Just redn1
 1344              -> do { redn2 <- normalise_reduction redn1
 1345                    ; let redn3 = mkTyConAppCo role tc args_cos `mkTransRedn` redn2
 1346                    ; return $ assemble_result role redn3 res_co }
 1347            _ -> -- No unique matching family instance exists;
 1348                 -- we do not do anything
 1349                 return $
 1350                   assemble_result role (mkTyConAppRedn role tc redns) res_co }
 1351 
 1352   | otherwise
 1353   = -- A synonym with no type families in the RHS; or data type etc
 1354     -- Just normalise the arguments and rebuild
 1355     do { ArgsReductions redns res_co <- normalise_tc_args tc tys
 1356        ; role <- getRole
 1357        ; return $
 1358             assemble_result role (mkTyConAppRedn role tc redns) res_co }
 1359 
 1360   where
 1361     assemble_result :: Role       -- r, ambient role in NormM monad
 1362                     -> Reduction  -- orig_ty ~r nty, possibly heterogeneous (nty possibly of changed kind)
 1363                     -> MCoercionN -- typeKind(orig_ty) ~N typeKind(nty)
 1364                     -> Reduction  -- orig_ty ~r nty_casted
 1365                                   -- where nty_casted has same kind as orig_ty
 1366     assemble_result r redn kind_co
 1367       = mkCoherenceRightMRedn r redn (mkSymMCo kind_co)
 1368 
 1369 ---------------
 1370 -- | Try to simplify a type-family application, by *one* step
 1371 -- If topReduceTyFamApp_maybe env r F tys = Just (HetReduction (Reduction co rhs) res_co)
 1372 -- then    co     :: F tys ~R# rhs
 1373 --         res_co :: typeKind(F tys) ~ typeKind(rhs)
 1374 -- Type families and data families; always Representational role
 1375 topReduceTyFamApp_maybe :: FamInstEnvs -> TyCon -> [Type]
 1376                         -> Maybe HetReduction
 1377 topReduceTyFamApp_maybe envs fam_tc arg_tys
 1378   | isFamilyTyCon fam_tc   -- type families and data families
 1379   , Just redn <- reduceTyFamApp_maybe envs role fam_tc ntys
 1380   = Just $
 1381       mkHetReduction
 1382         (mkTyConAppCo role fam_tc args_cos `mkTransRedn` redn)
 1383         res_co
 1384   | otherwise
 1385   = Nothing
 1386   where
 1387     role = Representational
 1388     ArgsReductions (Reductions args_cos ntys) res_co
 1389       = initNormM envs role (tyCoVarsOfTypes arg_tys)
 1390       $ normalise_tc_args fam_tc arg_tys
 1391 
 1392 normalise_tc_args :: TyCon -> [Type] -> NormM ArgsReductions
 1393 normalise_tc_args tc tys
 1394   = do { role <- getRole
 1395        ; normalise_args (tyConKind tc) (tyConRolesX role tc) tys }
 1396 
 1397 ---------------
 1398 normaliseType :: FamInstEnvs
 1399               -> Role  -- desired role of coercion
 1400               -> Type -> Reduction
 1401 normaliseType env role ty
 1402   = initNormM env role (tyCoVarsOfType ty) $ normalise_type ty
 1403 
 1404 normalise_type :: Type -> NormM Reduction
 1405 -- Normalise the input type, by eliminating *all* type-function redexes
 1406 -- but *not* newtypes (which are visible to the programmer)
 1407 -- Returns with Refl if nothing happens
 1408 -- Does nothing to newtypes
 1409 -- The returned coercion *must* be *homogeneous*
 1410 -- See Note [Normalising types]
 1411 -- Try not to disturb type synonyms if possible
 1412 
 1413 normalise_type ty
 1414   = go ty
 1415   where
 1416     go :: Type -> NormM Reduction
 1417     go (TyConApp tc tys) = normalise_tc_app tc tys
 1418     go ty@(LitTy {})
 1419       = do { r <- getRole
 1420            ; return $ mkReflRedn r ty }
 1421     go (AppTy ty1 ty2) = go_app_tys ty1 [ty2]
 1422 
 1423     go (FunTy { ft_af = vis, ft_mult = w, ft_arg = ty1, ft_res = ty2 })
 1424       = do { arg_redn <- go ty1
 1425            ; res_redn <- go ty2
 1426            ; w_redn <- withRole Nominal $ go w
 1427            ; r <- getRole
 1428            ; return $ mkFunRedn r vis w_redn arg_redn res_redn }
 1429     go (ForAllTy (Bndr tcvar vis) ty)
 1430       = do { (lc', tv', k_redn) <- normalise_var_bndr tcvar
 1431            ; redn <- withLC lc' $ normalise_type ty
 1432            ; return $ mkForAllRedn vis tv' k_redn redn }
 1433     go (TyVarTy tv)    = normalise_tyvar tv
 1434     go (CastTy ty co)
 1435       = do { redn <- go ty
 1436            ; lc <- getLC
 1437            ; let co' = substRightCo lc co
 1438            ; return $ mkCastRedn2 Nominal ty co redn co'
 1439              --       ^^^^^^^^^^^ uses castCoercionKind2
 1440            }
 1441     go (CoercionTy co)
 1442       = do { lc <- getLC
 1443            ; r <- getRole
 1444            ; let kco = liftCoSubst Nominal lc (coercionType co)
 1445                  co' = substRightCo lc co
 1446            ; return $ mkProofIrrelRedn r kco co co' }
 1447 
 1448     go_app_tys :: Type   -- function
 1449                -> [Type] -- args
 1450                -> NormM Reduction
 1451     -- cf. GHC.Tc.Solver.Rewrite.rewrite_app_ty_args
 1452     go_app_tys (AppTy ty1 ty2) tys = go_app_tys ty1 (ty2 : tys)
 1453     go_app_tys fun_ty arg_tys
 1454       = do { fun_redn@(Reduction fun_co nfun) <- go fun_ty
 1455            ; case tcSplitTyConApp_maybe nfun of
 1456                Just (tc, xis) ->
 1457                  do { redn <- go (mkTyConApp tc (xis ++ arg_tys))
 1458                    -- rewrite_app_ty_args avoids redundantly processing the xis,
 1459                    -- but that's a much more performance-sensitive function.
 1460                    -- This type normalisation is not called in a loop.
 1461                     ; return $
 1462                         mkAppCos fun_co (map mkNomReflCo arg_tys) `mkTransRedn` redn }
 1463                Nothing ->
 1464                  do { ArgsReductions redns res_co
 1465                         <- normalise_args (typeKind nfun)
 1466                                           (repeat Nominal)
 1467                                           arg_tys
 1468                     ; role <- getRole
 1469                     ; return $
 1470                         mkCoherenceRightMRedn role
 1471                           (mkAppRedns fun_redn redns)
 1472                           (mkSymMCo res_co) } }
 1473 
 1474 normalise_args :: Kind    -- of the function
 1475                -> [Role]  -- roles at which to normalise args
 1476                -> [Type]  -- args
 1477                -> NormM ArgsReductions
 1478 -- returns ArgsReductions (Reductions cos xis) res_co,
 1479 -- where each xi is the normalised version of the corresponding type,
 1480 -- each co is orig_arg ~ xi, and res_co :: kind(f orig_args) ~ kind(f xis).
 1481 -- NB: The xis might *not* have the same kinds as the input types,
 1482 -- but the resulting application *will* be well-kinded
 1483 -- cf. GHC.Tc.Solver.Rewrite.rewrite_args_slow
 1484 normalise_args fun_ki roles args
 1485   = do { normed_args <- zipWithM normalise1 roles args
 1486        ; return $ simplifyArgsWorker ki_binders inner_ki fvs roles normed_args }
 1487   where
 1488     (ki_binders, inner_ki) = splitPiTys fun_ki
 1489     fvs = tyCoVarsOfTypes args
 1490 
 1491     normalise1 role ty
 1492       = withRole role $ normalise_type ty
 1493 
 1494 normalise_tyvar :: TyVar -> NormM Reduction
 1495 normalise_tyvar tv
 1496   = assert (isTyVar tv) $
 1497     do { lc <- getLC
 1498        ; r  <- getRole
 1499        ; return $ case liftCoSubstTyVar lc r tv of
 1500            Just co -> coercionRedn co
 1501            Nothing -> mkReflRedn r (mkTyVarTy tv) }
 1502 
 1503 normalise_reduction :: Reduction -> NormM Reduction
 1504 normalise_reduction (Reduction co ty)
 1505   = do { redn' <- normalise_type ty
 1506        ; return $ co `mkTransRedn` redn' }
 1507 
 1508 normalise_var_bndr :: TyCoVar -> NormM (LiftingContext, TyCoVar, Reduction)
 1509 normalise_var_bndr tcvar
 1510   -- works for both tvar and covar
 1511   = do { lc1 <- getLC
 1512        ; env <- getEnv
 1513        ; let callback lc ki = runNormM (normalise_type ki) env lc Nominal
 1514        ; return $ liftCoSubstVarBndrUsing reductionCoercion callback lc1 tcvar }
 1515 
 1516 -- | a monad for the normalisation functions, reading 'FamInstEnvs',
 1517 -- a 'LiftingContext', and a 'Role'.
 1518 newtype NormM a = NormM { runNormM ::
 1519                             FamInstEnvs -> LiftingContext -> Role -> a }
 1520     deriving (Functor)
 1521 
 1522 initNormM :: FamInstEnvs -> Role
 1523           -> TyCoVarSet   -- the in-scope variables
 1524           -> NormM a -> a
 1525 initNormM env role vars (NormM thing_inside)
 1526   = thing_inside env lc role
 1527   where
 1528     in_scope = mkInScopeSet vars
 1529     lc       = emptyLiftingContext in_scope
 1530 
 1531 getRole :: NormM Role
 1532 getRole = NormM (\ _ _ r -> r)
 1533 
 1534 getLC :: NormM LiftingContext
 1535 getLC = NormM (\ _ lc _ -> lc)
 1536 
 1537 getEnv :: NormM FamInstEnvs
 1538 getEnv = NormM (\ env _ _ -> env)
 1539 
 1540 withRole :: Role -> NormM a -> NormM a
 1541 withRole r thing = NormM $ \ envs lc _old_r -> runNormM thing envs lc r
 1542 
 1543 withLC :: LiftingContext -> NormM a -> NormM a
 1544 withLC lc thing = NormM $ \ envs _old_lc r -> runNormM thing envs lc r
 1545 
 1546 instance Monad NormM where
 1547   ma >>= fmb = NormM $ \env lc r ->
 1548                let a = runNormM ma env lc r in
 1549                runNormM (fmb a) env lc r
 1550 
 1551 instance Applicative NormM where
 1552   pure x = NormM $ \ _ _ _ -> x
 1553   (<*>)  = ap