-- (c) The University of Glasgow 2006
--
-- FamInstEnv: Type checked family instance declarations

{-# LANGUAGE CPP, GADTs, ScopedTypeVariables, BangPatterns, TupleSections,
    DeriveFunctor #-}

{-# OPTIONS_GHC -Wno-incomplete-record-updates #-}

module GHC.Core.FamInstEnv (
        FamInst(..), FamFlavor(..), famInstAxiom, famInstTyCon, famInstRHS,
        famInstsRepTyCons, famInstRepTyCon_maybe, dataFamInstRepTyCon,
        pprFamInst, pprFamInsts,
        mkImportedFamInst,

        FamInstEnvs, FamInstEnv, emptyFamInstEnv, emptyFamInstEnvs,
        extendFamInstEnv, extendFamInstEnvList,
        famInstEnvElts, famInstEnvSize, familyInstances,

        -- * CoAxioms
        mkCoAxBranch, mkBranchedCoAxiom, mkUnbranchedCoAxiom, mkSingleCoAxiom,
        mkNewTypeCoAxiom,

        FamInstMatch(..),
        lookupFamInstEnv, lookupFamInstEnvConflicts, lookupFamInstEnvByTyCon,

        isDominatedBy, apartnessCheck,

        -- Injectivity
        InjectivityCheckResult(..),
        lookupFamInstEnvInjectivityConflicts, injectiveBranches,

        -- Normalisation
        topNormaliseType, topNormaliseType_maybe,
        normaliseType, normaliseTcApp,
        topReduceTyFamApp_maybe, reduceTyFamApp_maybe,

        -- Flattening
        flattenTys
    ) where

#include "HsVersions.h"

import GHC.Prelude

import GHC.Core.Unify
import GHC.Core.Type as Type
import GHC.Core.TyCo.Rep
import GHC.Core.TyCon
import GHC.Core.Coercion
import GHC.Core.Coercion.Axiom
import GHC.Types.Var.Set
import GHC.Types.Var.Env
import GHC.Types.Name
import GHC.Types.Unique.DFM
import GHC.Utils.Outputable
import GHC.Data.Maybe
import GHC.Core.Map
import GHC.Types.Unique
import GHC.Utils.Misc
import GHC.Types.Var
import GHC.Types.SrcLoc
import GHC.Data.FastString
import Control.Monad
import Data.List( mapAccumL )
import Data.Array( Array, assocs )

{-
************************************************************************
*                                                                      *
          Type checked family instance heads
*                                                                      *
************************************************************************

Note [FamInsts and CoAxioms]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~
* CoAxioms and FamInsts are just like
  DFunIds  and ClsInsts

* A CoAxiom is a System-FC thing: it can relate any two types

* A FamInst is a Haskell source-language thing, corresponding
  to a type/data family instance declaration.
    - The FamInst contains a CoAxiom, which is the evidence
      for the instance

    - The LHS of the CoAxiom is always of form F ty1 .. tyn
      where F is a type family
-}

data FamInst  -- See Note [FamInsts and CoAxioms]
  = FamInst { FamInst -> CoAxiom Unbranched
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...

            , FamInst -> FamFlavor
fi_flavor :: FamFlavor

            -- Everything below here is a redundant,
            -- cached version of the two things above
            -- except that the TyVars are freshened
            , FamInst -> Name
fi_fam   :: Name          -- Family name

                -- Used for "rough matching"; same idea as for class instances
                -- See Note [Rough-match field] in GHC.Core.InstEnv
            , FamInst -> [Maybe Name]
fi_tcs   :: [Maybe Name]  -- Top of type args
                -- INVARIANT: fi_tcs = roughMatchTcs fi_tys

            -- Used for "proper matching"; ditto
            , FamInst -> [TyVar]
fi_tvs :: [TyVar]      -- Template tyvars for full match
            , FamInst -> [TyVar]
fi_cvs :: [CoVar]      -- Template covars for full match
                 -- Like ClsInsts, these variables are always fresh
                 -- See Note [Template tyvars are fresh] in GHC.Core.InstEnv

            , FamInst -> [Type]
fi_tys    :: [Type]       --   The LHS type patterns
            -- May be eta-reduced; see Note [Eta reduction for data families]
            -- in GHC.Core.Coercion.Axiom

            , FamInst -> Type
fi_rhs :: Type         --   the RHS, with its freshened vars
            }

data FamFlavor
  = SynFamilyInst         -- A synonym family
  | DataFamilyInst TyCon  -- A data family, with its representation TyCon

{-
Note [Arity of data families]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Data family instances might legitimately be over- or under-saturated.

Under-saturation has two potential causes:
 U1) Eta reduction. See Note [Eta reduction for data families] in
     GHC.Core.Coercion.Axiom.
 U2) When the user has specified a return kind instead of written out patterns.
     Example:

       data family Sing (a :: k)
       data instance Sing :: Bool -> Type

     The data family tycon Sing has an arity of 2, the k and the a. But
     the data instance has only one pattern, Bool (standing in for k).
     This instance is equivalent to `data instance Sing (a :: Bool)`, but
     without the last pattern, we have an under-saturated data family instance.
     On its own, this example is not compelling enough to add support for
     under-saturation, but U1 makes this feature more compelling.

Over-saturation is also possible:
  O1) If the data family's return kind is a type variable (see also #12369),
      an instance might legitimately have more arguments than the family.
      Example:

        data family Fix :: (Type -> k) -> k
        data instance Fix f = MkFix1 (f (Fix f))
        data instance Fix f x = MkFix2 (f (Fix f x) x)

      In the first instance here, the k in the data family kind is chosen to
      be Type. In the second, it's (Type -> Type).

      However, we require that any over-saturation is eta-reducible. That is,
      we require that any extra patterns be bare unrepeated type variables;
      see Note [Eta reduction for data families] in GHC.Core.Coercion.Axiom.
      Accordingly, the FamInst is never over-saturated.

Why can we allow such flexibility for data families but not for type families?
Because data families can be decomposed -- that is, they are generative and
injective. A Type family is neither and so always must be applied to all its
arguments.
-}

-- Obtain the axiom of a family instance
famInstAxiom :: FamInst -> CoAxiom Unbranched
famInstAxiom :: FamInst -> CoAxiom Unbranched
famInstAxiom = FamInst -> CoAxiom Unbranched
fi_axiom

-- Split the left-hand side of the FamInst
famInstSplitLHS :: FamInst -> (TyCon, [Type])
famInstSplitLHS :: FamInst -> (TyCon, [Type])
famInstSplitLHS (FamInst { fi_axiom :: FamInst -> CoAxiom Unbranched
fi_axiom = CoAxiom Unbranched
axiom, fi_tys :: FamInst -> [Type]
fi_tys = [Type]
lhs })
  = (CoAxiom Unbranched -> TyCon
forall (br :: BranchFlag). CoAxiom br -> TyCon
coAxiomTyCon CoAxiom Unbranched
axiom, [Type]
lhs)

-- Get the RHS of the FamInst
famInstRHS :: FamInst -> Type
famInstRHS :: FamInst -> Type
famInstRHS = FamInst -> Type
fi_rhs

-- Get the family TyCon of the FamInst
famInstTyCon :: FamInst -> TyCon
famInstTyCon :: FamInst -> TyCon
famInstTyCon = CoAxiom Unbranched -> TyCon
forall (br :: BranchFlag). CoAxiom br -> TyCon
coAxiomTyCon (CoAxiom Unbranched -> TyCon)
-> (FamInst -> CoAxiom Unbranched) -> FamInst -> TyCon
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FamInst -> CoAxiom Unbranched
famInstAxiom

-- Return the representation TyCons introduced by data family instances, if any
famInstsRepTyCons :: [FamInst] -> [TyCon]
famInstsRepTyCons :: [FamInst] -> [TyCon]
famInstsRepTyCons [FamInst]
fis = [TyCon
tc | FamInst { fi_flavor :: FamInst -> FamFlavor
fi_flavor = DataFamilyInst TyCon
tc } <- [FamInst]
fis]

-- Extracts the TyCon for this *data* (or newtype) instance
famInstRepTyCon_maybe :: FamInst -> Maybe TyCon
famInstRepTyCon_maybe :: FamInst -> Maybe TyCon
famInstRepTyCon_maybe FamInst
fi
  = case FamInst -> FamFlavor
fi_flavor FamInst
fi of
       DataFamilyInst TyCon
tycon -> TyCon -> Maybe TyCon
forall a. a -> Maybe a
Just TyCon
tycon
       FamFlavor
SynFamilyInst        -> Maybe TyCon
forall a. Maybe a
Nothing

dataFamInstRepTyCon :: FamInst -> TyCon
dataFamInstRepTyCon :: FamInst -> TyCon
dataFamInstRepTyCon FamInst
fi
  = case FamInst -> FamFlavor
fi_flavor FamInst
fi of
       DataFamilyInst TyCon
tycon -> TyCon
tycon
       FamFlavor
SynFamilyInst        -> String -> SDoc -> TyCon
forall a. HasCallStack => String -> SDoc -> a
pprPanic String
"dataFamInstRepTyCon" (FamInst -> SDoc
forall a. Outputable a => a -> SDoc
ppr FamInst
fi)

{-
************************************************************************
*                                                                      *
        Pretty printing
*                                                                      *
************************************************************************
-}

instance NamedThing FamInst where
   getName :: FamInst -> Name
getName = CoAxiom Unbranched -> Name
forall (br :: BranchFlag). CoAxiom br -> Name
coAxiomName (CoAxiom Unbranched -> Name)
-> (FamInst -> CoAxiom Unbranched) -> FamInst -> Name
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FamInst -> CoAxiom Unbranched
fi_axiom

instance Outputable FamInst where
   ppr :: FamInst -> SDoc
ppr = FamInst -> SDoc
pprFamInst

pprFamInst :: FamInst -> SDoc
-- Prints the FamInst as a family instance declaration
-- NB: This function, FamInstEnv.pprFamInst, is used only for internal,
--     debug printing. See GHC.Core.Ppr.TyThing.pprFamInst for printing for the user
pprFamInst :: FamInst -> SDoc
pprFamInst (FamInst { fi_flavor :: FamInst -> FamFlavor
fi_flavor = FamFlavor
flavor, fi_axiom :: FamInst -> CoAxiom Unbranched
fi_axiom = CoAxiom Unbranched
ax
                    , fi_tvs :: FamInst -> [TyVar]
fi_tvs = [TyVar]
tvs, fi_tys :: FamInst -> [Type]
fi_tys = [Type]
tys, fi_rhs :: FamInst -> Type
fi_rhs = Type
rhs })
  = SDoc -> Arity -> SDoc -> SDoc
hang (SDoc
ppr_tc_sort SDoc -> SDoc -> SDoc
<+> String -> SDoc
text String
"instance"
             SDoc -> SDoc -> SDoc
<+> TyCon -> CoAxBranch -> SDoc
pprCoAxBranchUser (CoAxiom Unbranched -> TyCon
forall (br :: BranchFlag). CoAxiom br -> TyCon
coAxiomTyCon CoAxiom Unbranched
ax) (CoAxiom Unbranched -> CoAxBranch
coAxiomSingleBranch CoAxiom Unbranched
ax))
       Arity
2 (SDoc -> SDoc
whenPprDebug SDoc
debug_stuff)
  where
    ppr_tc_sort :: SDoc
ppr_tc_sort = case FamFlavor
flavor of
                     FamFlavor
SynFamilyInst             -> String -> SDoc
text String
"type"
                     DataFamilyInst TyCon
tycon
                       | TyCon -> Bool
isDataTyCon     TyCon
tycon -> String -> SDoc
text String
"data"
                       | TyCon -> Bool
isNewTyCon      TyCon
tycon -> String -> SDoc
text String
"newtype"
                       | TyCon -> Bool
isAbstractTyCon TyCon
tycon -> String -> SDoc
text String
"data"
                       | Bool
otherwise             -> String -> SDoc
text String
"WEIRD" SDoc -> SDoc -> SDoc
<+> TyCon -> SDoc
forall a. Outputable a => a -> SDoc
ppr TyCon
tycon

    debug_stuff :: SDoc
debug_stuff = [SDoc] -> SDoc
vcat [ String -> SDoc
text String
"Coercion axiom:" SDoc -> SDoc -> SDoc
<+> CoAxiom Unbranched -> SDoc
forall a. Outputable a => a -> SDoc
ppr CoAxiom Unbranched
ax
                       , String -> SDoc
text String
"Tvs:" SDoc -> SDoc -> SDoc
<+> [TyVar] -> SDoc
forall a. Outputable a => a -> SDoc
ppr [TyVar]
tvs
                       , String -> SDoc
text String
"LHS:" SDoc -> SDoc -> SDoc
<+> [Type] -> SDoc
forall a. Outputable a => a -> SDoc
ppr [Type]
tys
                       , String -> SDoc
text String
"RHS:" SDoc -> SDoc -> SDoc
<+> Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
rhs ]

pprFamInsts :: [FamInst] -> SDoc
pprFamInsts :: [FamInst] -> SDoc
pprFamInsts [FamInst]
finsts = [SDoc] -> SDoc
vcat ((FamInst -> SDoc) -> [FamInst] -> [SDoc]
forall a b. (a -> b) -> [a] -> [b]
map FamInst -> SDoc
pprFamInst [FamInst]
finsts)

{-
Note [Lazy axiom match]
~~~~~~~~~~~~~~~~~~~~~~~
It is Vitally Important that mkImportedFamInst is *lazy* in its axiom
parameter. The axiom is loaded lazily, via a forkM, in GHC.IfaceToCore. Sometime
later, mkImportedFamInst is called using that axiom. However, the axiom
may itself depend on entities which are not yet loaded as of the time
of the mkImportedFamInst. Thus, if mkImportedFamInst eagerly looks at the
axiom, a dependency loop spontaneously appears and GHC hangs. The solution
is simply for mkImportedFamInst never, ever to look inside of the axiom
until everything else is good and ready to do so. We can assume that this
readiness has been achieved when some other code pulls on the axiom in the
FamInst. Thus, we pattern match on the axiom lazily (in the where clause,
not in the parameter list) and we assert the consistency of names there
also.
-}

-- Make a family instance representation from the information found in an
-- interface file.  In particular, we get the rough match info from the iface
-- (instead of computing it here).
mkImportedFamInst :: Name               -- Name of the family
                  -> [Maybe Name]       -- Rough match info
                  -> CoAxiom Unbranched -- Axiom introduced
                  -> FamInst            -- Resulting family instance
mkImportedFamInst :: Name -> [Maybe Name] -> CoAxiom Unbranched -> FamInst
mkImportedFamInst Name
fam [Maybe Name]
mb_tcs CoAxiom Unbranched
axiom
  = FamInst :: CoAxiom Unbranched
-> FamFlavor
-> Name
-> [Maybe Name]
-> [TyVar]
-> [TyVar]
-> [Type]
-> Type
-> FamInst
FamInst {
      fi_fam :: Name
fi_fam    = Name
fam,
      fi_tcs :: [Maybe Name]
fi_tcs    = [Maybe Name]
mb_tcs,
      fi_tvs :: [TyVar]
fi_tvs    = [TyVar]
tvs,
      fi_cvs :: [TyVar]
fi_cvs    = [TyVar]
cvs,
      fi_tys :: [Type]
fi_tys    = [Type]
tys,
      fi_rhs :: Type
fi_rhs    = Type
rhs,
      fi_axiom :: CoAxiom Unbranched
fi_axiom  = CoAxiom Unbranched
axiom,
      fi_flavor :: FamFlavor
fi_flavor = FamFlavor
flavor }
  where
     -- See Note [Lazy axiom match]
     ~(CoAxBranch { cab_lhs :: CoAxBranch -> [Type]
cab_lhs = [Type]
tys
                  , cab_tvs :: CoAxBranch -> [TyVar]
cab_tvs = [TyVar]
tvs
                  , cab_cvs :: CoAxBranch -> [TyVar]
cab_cvs = [TyVar]
cvs
                  , cab_rhs :: CoAxBranch -> Type
cab_rhs = Type
rhs }) = CoAxiom Unbranched -> CoAxBranch
coAxiomSingleBranch CoAxiom Unbranched
axiom

         -- Derive the flavor for an imported FamInst rather disgustingly
         -- Maybe we should store it in the IfaceFamInst?
     flavor :: FamFlavor
flavor = case HasDebugCallStack => Type -> Maybe (TyCon, [Type])
Type -> Maybe (TyCon, [Type])
splitTyConApp_maybe Type
rhs of
                Just (TyCon
tc, [Type]
_)
                  | Just CoAxiom Unbranched
ax' <- TyCon -> Maybe (CoAxiom Unbranched)
tyConFamilyCoercion_maybe TyCon
tc
                  , CoAxiom Unbranched
ax' CoAxiom Unbranched -> CoAxiom Unbranched -> Bool
forall a. Eq a => a -> a -> Bool
== CoAxiom Unbranched
axiom
                  -> TyCon -> FamFlavor
DataFamilyInst TyCon
tc
                Maybe (TyCon, [Type])
_ -> FamFlavor
SynFamilyInst

{-
************************************************************************
*                                                                      *
                FamInstEnv
*                                                                      *
************************************************************************

Note [FamInstEnv]
~~~~~~~~~~~~~~~~~
A FamInstEnv maps a family name to the list of known instances for that family.

The same FamInstEnv includes both 'data family' and 'type family' instances.
Type families are reduced during type inference, but not data families;
the user explains when to use a data family instance by using constructors
and pattern matching.

Nevertheless it is still useful to have data families in the FamInstEnv:

 - For finding overlaps and conflicts

 - For finding the representation type...see FamInstEnv.topNormaliseType
   and its call site in GHC.Core.Opt.Simplify

 - In standalone deriving instance Eq (T [Int]) we need to find the
   representation type for T [Int]

Note [Varying number of patterns for data family axioms]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
For data families, the number of patterns may vary between instances.
For example
   data family T a b
   data instance T Int a = T1 a | T2
   data instance T Bool [a] = T3 a

Then we get a data type for each instance, and an axiom:
   data TInt a = T1 a | T2
   data TBoolList a = T3 a

   axiom ax7   :: T Int ~ TInt   -- Eta-reduced
   axiom ax8 a :: T Bool [a] ~ TBoolList a

These two axioms for T, one with one pattern, one with two;
see Note [Eta reduction for data families] in GHC.Core.Coercion.Axiom

Note [FamInstEnv determinism]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
We turn FamInstEnvs into a list in some places that don't directly affect
the ABI. That happens in family consistency checks and when producing output
for `:info`. Unfortunately that nondeterminism is nonlocal and it's hard
to tell what it affects without following a chain of functions. It's also
easy to accidentally make that nondeterminism affect the ABI. Furthermore
the envs should be relatively small, so it should be free to use deterministic
maps here. Testing with nofib and validate detected no difference between
UniqFM and UniqDFM.
See Note [Deterministic UniqFM].
-}

-- Internally we sometimes index by Name instead of TyCon despite
-- of what the type says. This is safe since
-- getUnique (tyCon) == getUniqe (tcName tyCon)
type FamInstEnv = UniqDFM TyCon FamilyInstEnv  -- Maps a family to its instances
     -- See Note [FamInstEnv]
     -- See Note [FamInstEnv determinism]

type FamInstEnvs = (FamInstEnv, FamInstEnv)
     -- External package inst-env, Home-package inst-env

newtype FamilyInstEnv
  = FamIE [FamInst]     -- The instances for a particular family, in any order

instance Outputable FamilyInstEnv where
  ppr :: FamilyInstEnv -> SDoc
ppr (FamIE [FamInst]
fs) = String -> SDoc
text String
"FamIE" SDoc -> SDoc -> SDoc
<+> [SDoc] -> SDoc
vcat ((FamInst -> SDoc) -> [FamInst] -> [SDoc]
forall a b. (a -> b) -> [a] -> [b]
map FamInst -> SDoc
forall a. Outputable a => a -> SDoc
ppr [FamInst]
fs)

-- | Index a FamInstEnv by the tyCons name.
toNameInstEnv :: FamInstEnv -> UniqDFM Name FamilyInstEnv
toNameInstEnv :: FamInstEnv -> UniqDFM Name FamilyInstEnv
toNameInstEnv = FamInstEnv -> UniqDFM Name FamilyInstEnv
forall key1 elt key2. UniqDFM key1 elt -> UniqDFM key2 elt
unsafeCastUDFMKey

-- | Create a FamInstEnv from Name indices.
fromNameInstEnv :: UniqDFM Name FamilyInstEnv -> FamInstEnv
fromNameInstEnv :: UniqDFM Name FamilyInstEnv -> FamInstEnv
fromNameInstEnv = UniqDFM Name FamilyInstEnv -> FamInstEnv
forall key1 elt key2. UniqDFM key1 elt -> UniqDFM key2 elt
unsafeCastUDFMKey

-- INVARIANTS:
--  * The fs_tvs are distinct in each FamInst
--      of a range value of the map (so we can safely unify them)

emptyFamInstEnvs :: (FamInstEnv, FamInstEnv)
emptyFamInstEnvs :: (FamInstEnv, FamInstEnv)
emptyFamInstEnvs = (FamInstEnv
emptyFamInstEnv, FamInstEnv
emptyFamInstEnv)

emptyFamInstEnv :: FamInstEnv
emptyFamInstEnv :: FamInstEnv
emptyFamInstEnv = FamInstEnv
forall key elt. UniqDFM key elt
emptyUDFM

famInstEnvElts :: FamInstEnv -> [FamInst]
famInstEnvElts :: FamInstEnv -> [FamInst]
famInstEnvElts FamInstEnv
fi = [FamInst
elt | FamIE [FamInst]
elts <- FamInstEnv -> [FamilyInstEnv]
forall key elt. UniqDFM key elt -> [elt]
eltsUDFM FamInstEnv
fi, FamInst
elt <- [FamInst]
elts]
  -- See Note [FamInstEnv determinism]

famInstEnvSize :: FamInstEnv -> Int
famInstEnvSize :: FamInstEnv -> Arity
famInstEnvSize = (FamilyInstEnv -> Arity -> Arity) -> Arity -> FamInstEnv -> Arity
forall elt a key. (elt -> a -> a) -> a -> UniqDFM key elt -> a
nonDetStrictFoldUDFM (\(FamIE [FamInst]
elt) Arity
sum -> Arity
sum Arity -> Arity -> Arity
forall a. Num a => a -> a -> a
+ [FamInst] -> Arity
forall (t :: * -> *) a. Foldable t => t a -> Arity
length [FamInst]
elt) Arity
0
  -- It's OK to use nonDetStrictFoldUDFM here since we're just computing the
  -- size.

familyInstances :: (FamInstEnv, FamInstEnv) -> TyCon -> [FamInst]
familyInstances :: (FamInstEnv, FamInstEnv) -> TyCon -> [FamInst]
familyInstances (FamInstEnv
pkg_fie, FamInstEnv
home_fie) TyCon
fam
  = FamInstEnv -> [FamInst]
get FamInstEnv
home_fie [FamInst] -> [FamInst] -> [FamInst]
forall a. [a] -> [a] -> [a]
++ FamInstEnv -> [FamInst]
get FamInstEnv
pkg_fie
  where
    get :: FamInstEnv -> [FamInst]
get FamInstEnv
env = case FamInstEnv -> TyCon -> Maybe FamilyInstEnv
forall key elt.
Uniquable key =>
UniqDFM key elt -> key -> Maybe elt
lookupUDFM FamInstEnv
env TyCon
fam of
                Just (FamIE [FamInst]
insts) -> [FamInst]
insts
                Maybe FamilyInstEnv
Nothing                      -> []

extendFamInstEnvList :: FamInstEnv -> [FamInst] -> FamInstEnv
extendFamInstEnvList :: FamInstEnv -> [FamInst] -> FamInstEnv
extendFamInstEnvList FamInstEnv
inst_env [FamInst]
fis = (FamInstEnv -> FamInst -> FamInstEnv)
-> FamInstEnv -> [FamInst] -> FamInstEnv
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' FamInstEnv -> FamInst -> FamInstEnv
extendFamInstEnv FamInstEnv
inst_env [FamInst]
fis

extendFamInstEnv :: FamInstEnv -> FamInst -> FamInstEnv
extendFamInstEnv :: FamInstEnv -> FamInst -> FamInstEnv
extendFamInstEnv FamInstEnv
inst_env
                 ins_item :: FamInst
ins_item@(FamInst {fi_fam :: FamInst -> Name
fi_fam = Name
cls_nm})
  = UniqDFM Name FamilyInstEnv -> FamInstEnv
fromNameInstEnv (UniqDFM Name FamilyInstEnv -> FamInstEnv)
-> UniqDFM Name FamilyInstEnv -> FamInstEnv
forall a b. (a -> b) -> a -> b
$ (FamilyInstEnv -> FamilyInstEnv -> FamilyInstEnv)
-> UniqDFM Name FamilyInstEnv
-> Name
-> FamilyInstEnv
-> UniqDFM Name FamilyInstEnv
forall key elt.
Uniquable key =>
(elt -> elt -> elt)
-> UniqDFM key elt -> key -> elt -> UniqDFM key elt
addToUDFM_C FamilyInstEnv -> FamilyInstEnv -> FamilyInstEnv
add (FamInstEnv -> UniqDFM Name FamilyInstEnv
toNameInstEnv FamInstEnv
inst_env) Name
cls_nm ([FamInst] -> FamilyInstEnv
FamIE [FamInst
ins_item])
  where
    add :: FamilyInstEnv -> FamilyInstEnv -> FamilyInstEnv
add (FamIE [FamInst]
items) FamilyInstEnv
_ = [FamInst] -> FamilyInstEnv
FamIE (FamInst
ins_itemFamInst -> [FamInst] -> [FamInst]
forall a. a -> [a] -> [a]
:[FamInst]
items)

{-
************************************************************************
*                                                                      *
                Compatibility
*                                                                      *
************************************************************************

Note [Apartness]
~~~~~~~~~~~~~~~~
In dealing with closed type families, we must be able to check that one type
will never reduce to another. This check is called /apartness/. The check
is always between a target (which may be an arbitrary type) and a pattern.
Here is how we do it:

apart(target, pattern) = not (unify(flatten(target), pattern))

where flatten (implemented in flattenTys, below) converts all type-family
applications into fresh variables. (See Note [Flattening].)

Note [Compatibility]
~~~~~~~~~~~~~~~~~~~~
Two patterns are /compatible/ if either of the following conditions hold:
1) The patterns are apart.
2) The patterns unify with a substitution S, and their right hand sides
equal under that substitution.

For open type families, only compatible instances are allowed. For closed
type families, the story is slightly more complicated. Consider the following:

type family F a where
  F Int = Bool
  F a   = Int

g :: Show a => a -> F a
g x = length (show x)

Should that type-check? No. We need to allow for the possibility that 'a'
might be Int and therefore 'F a' should be Bool. We can simplify 'F a' to Int
only when we can be sure that 'a' is not Int.

To achieve this, after finding a possible match within the equations, we have to
go back to all previous equations and check that, under the
substitution induced by the match, other branches are surely apart. (See
Note [Apartness].) This is similar to what happens with class
instance selection, when we need to guarantee that there is only a match and
no unifiers. The exact algorithm is different here because the
potentially-overlapping group is closed.

As another example, consider this:

type family G x where
  G Int = Bool
  G a   = Double

type family H y
-- no instances

Now, we want to simplify (G (H Char)). We can't, because (H Char) might later
simplify to be Int. So, (G (H Char)) is stuck, for now.

While everything above is quite sound, it isn't as expressive as we'd like.
Consider this:

type family J a where
  J Int = Int
  J a   = a

Can we simplify (J b) to b? Sure we can. Yes, the first equation matches if
b is instantiated with Int, but the RHSs coincide there, so it's all OK.

So, the rule is this: when looking up a branch in a closed type family, we
find a branch that matches the target, but then we make sure that the target
is apart from every previous *incompatible* branch. We don't check the
branches that are compatible with the matching branch, because they are either
irrelevant (clause 1 of compatible) or benign (clause 2 of compatible).

Note [Compatibility of eta-reduced axioms]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
In newtype instances of data families we eta-reduce the axioms,
See Note [Eta reduction for data families] in GHC.Core.Coercion.Axiom. This means that
we sometimes need to test compatibility of two axioms that were eta-reduced to
different degrees, e.g.:


data family D a b c
newtype instance D a Int c = DInt (Maybe a)
  -- D a Int ~ Maybe
  -- lhs = [a, Int]
newtype instance D Bool Int Char = DIntChar Float
  -- D Bool Int Char ~ Float
  -- lhs = [Bool, Int, Char]

These are obviously incompatible. We could detect this by saturating
(eta-expanding) the shorter LHS with fresh tyvars until the lists are of
equal length, but instead we can just remove the tail of the longer list, as
those types will simply unify with the freshly introduced tyvars.

By doing this, in case the LHS are unifiable, the yielded substitution won't
mention the tyvars that appear in the tail we dropped off, and we might try
to test equality RHSes of different kinds, but that's fine since this case
occurs only for data families, where the RHS is a unique tycon and the equality
fails anyway.
-}

-- See Note [Compatibility]
compatibleBranches :: CoAxBranch -> CoAxBranch -> Bool
compatibleBranches :: CoAxBranch -> CoAxBranch -> Bool
compatibleBranches (CoAxBranch { cab_lhs :: CoAxBranch -> [Type]
cab_lhs = [Type]
lhs1, cab_rhs :: CoAxBranch -> Type
cab_rhs = Type
rhs1 })
                   (CoAxBranch { cab_lhs :: CoAxBranch -> [Type]
cab_lhs = [Type]
lhs2, cab_rhs :: CoAxBranch -> Type
cab_rhs = Type
rhs2 })
  = let ([Type]
commonlhs1, [Type]
commonlhs2) = [Type] -> [Type] -> ([Type], [Type])
forall a b. [a] -> [b] -> ([a], [b])
zipAndUnzip [Type]
lhs1 [Type]
lhs2
             -- See Note [Compatibility of eta-reduced axioms]
    in case (TyVar -> BindFlag) -> [Type] -> [Type] -> UnifyResult
tcUnifyTysFG (BindFlag -> TyVar -> BindFlag
forall a b. a -> b -> a
const BindFlag
BindMe) [Type]
commonlhs1 [Type]
commonlhs2 of
      UnifyResult
SurelyApart -> Bool
True
      Unifiable TCvSubst
subst
        | TCvSubst -> Type -> Type
Type.substTyAddInScope TCvSubst
subst Type
rhs1 Type -> Type -> Bool
`eqType`
          TCvSubst -> Type -> Type
Type.substTyAddInScope TCvSubst
subst Type
rhs2
        -> Bool
True
      UnifyResult
_ -> Bool
False

-- | Result of testing two type family equations for injectiviy.
data InjectivityCheckResult
   = InjectivityAccepted
    -- ^ Either RHSs are distinct or unification of RHSs leads to unification of
    -- LHSs
   | InjectivityUnified CoAxBranch CoAxBranch
    -- ^ RHSs unify but LHSs don't unify under that substitution.  Relevant for
    -- closed type families where equation after unification might be
    -- overlpapped (in which case it is OK if they don't unify).  Constructor
    -- stores axioms after unification.

-- | Check whether two type family axioms don't violate injectivity annotation.
injectiveBranches :: [Bool] -> CoAxBranch -> CoAxBranch
                  -> InjectivityCheckResult
injectiveBranches :: [Bool] -> CoAxBranch -> CoAxBranch -> InjectivityCheckResult
injectiveBranches [Bool]
injectivity
                  ax1 :: CoAxBranch
ax1@(CoAxBranch { cab_lhs :: CoAxBranch -> [Type]
cab_lhs = [Type]
lhs1, cab_rhs :: CoAxBranch -> Type
cab_rhs = Type
rhs1 })
                  ax2 :: CoAxBranch
ax2@(CoAxBranch { cab_lhs :: CoAxBranch -> [Type]
cab_lhs = [Type]
lhs2, cab_rhs :: CoAxBranch -> Type
cab_rhs = Type
rhs2 })
  -- See Note [Verifying injectivity annotation], case 1.
  = let getInjArgs :: [Type] -> [Type]
getInjArgs  = [Bool] -> [Type] -> [Type]
forall a. [Bool] -> [a] -> [a]
filterByList [Bool]
injectivity
    in case Bool -> Type -> Type -> Maybe TCvSubst
tcUnifyTyWithTFs Bool
True Type
rhs1 Type
rhs2 of -- True = two-way pre-unification
       Maybe TCvSubst
Nothing -> InjectivityCheckResult
InjectivityAccepted
         -- RHS are different, so equations are injective.
         -- This is case 1A from Note [Verifying injectivity annotation]
       Just TCvSubst
subst -> -- RHS unify under a substitution
        let lhs1Subst :: [Type]
lhs1Subst = HasCallStack => TCvSubst -> [Type] -> [Type]
TCvSubst -> [Type] -> [Type]
Type.substTys TCvSubst
subst ([Type] -> [Type]
getInjArgs [Type]
lhs1)
            lhs2Subst :: [Type]
lhs2Subst = HasCallStack => TCvSubst -> [Type] -> [Type]
TCvSubst -> [Type] -> [Type]
Type.substTys TCvSubst
subst ([Type] -> [Type]
getInjArgs [Type]
lhs2)
        -- If LHSs are equal under the substitution used for RHSs then this pair
        -- of equations does not violate injectivity annotation. If LHSs are not
        -- equal under that substitution then this pair of equations violates
        -- injectivity annotation, but for closed type families it still might
        -- be the case that one LHS after substitution is unreachable.
        in if [Type] -> [Type] -> Bool
eqTypes [Type]
lhs1Subst [Type]
lhs2Subst  -- check case 1B1 from Note.
           then InjectivityCheckResult
InjectivityAccepted
           else CoAxBranch -> CoAxBranch -> InjectivityCheckResult
InjectivityUnified ( CoAxBranch
ax1 { cab_lhs :: [Type]
cab_lhs = HasCallStack => TCvSubst -> [Type] -> [Type]
TCvSubst -> [Type] -> [Type]
Type.substTys TCvSubst
subst [Type]
lhs1
                                         , cab_rhs :: Type
cab_rhs = HasCallStack => TCvSubst -> Type -> Type
TCvSubst -> Type -> Type
Type.substTy  TCvSubst
subst Type
rhs1 })
                                   ( CoAxBranch
ax2 { cab_lhs :: [Type]
cab_lhs = HasCallStack => TCvSubst -> [Type] -> [Type]
TCvSubst -> [Type] -> [Type]
Type.substTys TCvSubst
subst [Type]
lhs2
                                         , cab_rhs :: Type
cab_rhs = HasCallStack => TCvSubst -> Type -> Type
TCvSubst -> Type -> Type
Type.substTy  TCvSubst
subst Type
rhs2 })
                -- payload of InjectivityUnified used only for check 1B2, only
                -- for closed type families

-- takes a CoAxiom with unknown branch incompatibilities and computes
-- the compatibilities
-- See Note [Storing compatibility] in GHC.Core.Coercion.Axiom
computeAxiomIncomps :: [CoAxBranch] -> [CoAxBranch]
computeAxiomIncomps :: [CoAxBranch] -> [CoAxBranch]
computeAxiomIncomps [CoAxBranch]
branches
  = ([CoAxBranch], [CoAxBranch]) -> [CoAxBranch]
forall a b. (a, b) -> b
snd (([CoAxBranch] -> CoAxBranch -> ([CoAxBranch], CoAxBranch))
-> [CoAxBranch] -> [CoAxBranch] -> ([CoAxBranch], [CoAxBranch])
forall (t :: * -> *) s a b.
Traversable t =>
(s -> a -> (s, b)) -> s -> t a -> (s, t b)
mapAccumL [CoAxBranch] -> CoAxBranch -> ([CoAxBranch], CoAxBranch)
go [] [CoAxBranch]
branches)
  where
    go :: [CoAxBranch] -> CoAxBranch -> ([CoAxBranch], CoAxBranch)
    go :: [CoAxBranch] -> CoAxBranch -> ([CoAxBranch], CoAxBranch)
go [CoAxBranch]
prev_brs CoAxBranch
cur_br
       = (CoAxBranch
cur_br CoAxBranch -> [CoAxBranch] -> [CoAxBranch]
forall a. a -> [a] -> [a]
: [CoAxBranch]
prev_brs, CoAxBranch
new_br)
       where
         new_br :: CoAxBranch
new_br = CoAxBranch
cur_br { cab_incomps :: [CoAxBranch]
cab_incomps = [CoAxBranch] -> CoAxBranch -> [CoAxBranch]
mk_incomps [CoAxBranch]
prev_brs CoAxBranch
cur_br }

    mk_incomps :: [CoAxBranch] -> CoAxBranch -> [CoAxBranch]
    mk_incomps :: [CoAxBranch] -> CoAxBranch -> [CoAxBranch]
mk_incomps [CoAxBranch]
prev_brs CoAxBranch
cur_br
       = (CoAxBranch -> Bool) -> [CoAxBranch] -> [CoAxBranch]
forall a. (a -> Bool) -> [a] -> [a]
filter (Bool -> Bool
not (Bool -> Bool) -> (CoAxBranch -> Bool) -> CoAxBranch -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CoAxBranch -> CoAxBranch -> Bool
compatibleBranches CoAxBranch
cur_br) [CoAxBranch]
prev_brs

{-
************************************************************************
*                                                                      *
           Constructing axioms
    These functions are here because tidyType / tcUnifyTysFG
    are not available in GHC.Core.Coercion.Axiom

    Also computeAxiomIncomps is too sophisticated for CoAxiom
*                                                                      *
************************************************************************

Note [Tidy axioms when we build them]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Like types and classes, we build axioms fully quantified over all
their variables, and tidy them when we build them. For example,
we print out axioms and don't want to print stuff like
    F k k a b = ...
Instead we must tidy those kind variables.  See #7524.

We could instead tidy when we print, but that makes it harder to get
things like injectivity errors to come out right. Danger of
     Type family equation violates injectivity annotation.
     Kind variable ‘k’ cannot be inferred from the right-hand side.
     In the type family equation:
        PolyKindVars @[k1] @[k2] ('[] @k1) = '[] @k2

Note [Always number wildcard types in CoAxBranch]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Consider the following example (from the DataFamilyInstanceLHS test case):

  data family Sing (a :: k)
  data instance Sing (_ :: MyKind) where
      SingA :: Sing A
      SingB :: Sing B

If we're not careful during tidying, then when this program is compiled with
-ddump-types, we'll get the following information:

  COERCION AXIOMS
    axiom DataFamilyInstanceLHS.D:R:SingMyKind_0 ::
      Sing _ = DataFamilyInstanceLHS.R:SingMyKind_ _

It's misleading to have a wildcard type appearing on the RHS like
that. To avoid this issue, when building a CoAxiom (which is what eventually
gets printed above), we tidy all the variables in an env that already contains
'_'. Thus, any variable named '_' will be renamed, giving us the nicer output
here:

  COERCION AXIOMS
    axiom DataFamilyInstanceLHS.D:R:SingMyKind_0 ::
      Sing _1 = DataFamilyInstanceLHS.R:SingMyKind_ _1

Which is at least legal syntax.

See also Note [CoAxBranch type variables] in GHC.Core.Coercion.Axiom; note that we
are tidying (changing OccNames only), not freshening, in accordance with
that Note.
-}

-- all axiom roles are Nominal, as this is only used with type families
mkCoAxBranch :: [TyVar] -- original, possibly stale, tyvars
             -> [TyVar] -- Extra eta tyvars
             -> [CoVar] -- possibly stale covars
             -> [Type]  -- LHS patterns
             -> Type    -- RHS
             -> [Role]
             -> SrcSpan
             -> CoAxBranch
mkCoAxBranch :: [TyVar]
-> [TyVar]
-> [TyVar]
-> [Type]
-> Type
-> [Role]
-> SrcSpan
-> CoAxBranch
mkCoAxBranch [TyVar]
tvs [TyVar]
eta_tvs [TyVar]
cvs [Type]
lhs Type
rhs [Role]
roles SrcSpan
loc
  = CoAxBranch :: SrcSpan
-> [TyVar]
-> [TyVar]
-> [TyVar]
-> [Role]
-> [Type]
-> Type
-> [CoAxBranch]
-> CoAxBranch
CoAxBranch { cab_tvs :: [TyVar]
cab_tvs     = [TyVar]
tvs'
               , cab_eta_tvs :: [TyVar]
cab_eta_tvs = [TyVar]
eta_tvs'
               , cab_cvs :: [TyVar]
cab_cvs     = [TyVar]
cvs'
               , cab_lhs :: [Type]
cab_lhs     = TidyEnv -> [Type] -> [Type]
tidyTypes TidyEnv
env [Type]
lhs
               , cab_roles :: [Role]
cab_roles   = [Role]
roles
               , cab_rhs :: Type
cab_rhs     = TidyEnv -> Type -> Type
tidyType TidyEnv
env Type
rhs
               , cab_loc :: SrcSpan
cab_loc     = SrcSpan
loc
               , cab_incomps :: [CoAxBranch]
cab_incomps = [CoAxBranch]
placeHolderIncomps }
  where
    (TidyEnv
env1, [TyVar]
tvs')     = TidyEnv -> [TyVar] -> (TidyEnv, [TyVar])
tidyVarBndrs TidyEnv
init_tidy_env [TyVar]
tvs
    (TidyEnv
env2, [TyVar]
eta_tvs') = TidyEnv -> [TyVar] -> (TidyEnv, [TyVar])
tidyVarBndrs TidyEnv
env1          [TyVar]
eta_tvs
    (TidyEnv
env,  [TyVar]
cvs')     = TidyEnv -> [TyVar] -> (TidyEnv, [TyVar])
tidyVarBndrs TidyEnv
env2          [TyVar]
cvs
    -- See Note [Tidy axioms when we build them]
    -- See also Note [CoAxBranch type variables] in GHC.Core.Coercion.Axiom

    init_occ_env :: TidyOccEnv
init_occ_env = [OccName] -> TidyOccEnv
initTidyOccEnv [String -> OccName
mkTyVarOcc String
"_"]
    init_tidy_env :: TidyEnv
init_tidy_env = TidyOccEnv -> TidyEnv
mkEmptyTidyEnv TidyOccEnv
init_occ_env
    -- See Note [Always number wildcard types in CoAxBranch]

-- all of the following code is here to avoid mutual dependencies with
-- Coercion
mkBranchedCoAxiom :: Name -> TyCon -> [CoAxBranch] -> CoAxiom Branched
mkBranchedCoAxiom :: Name -> TyCon -> [CoAxBranch] -> CoAxiom Branched
mkBranchedCoAxiom Name
ax_name TyCon
fam_tc [CoAxBranch]
branches
  = CoAxiom :: forall (br :: BranchFlag).
Unique
-> Name -> Role -> TyCon -> Branches br -> Bool -> CoAxiom br
CoAxiom { co_ax_unique :: Unique
co_ax_unique   = Name -> Unique
nameUnique Name
ax_name
            , co_ax_name :: Name
co_ax_name     = Name
ax_name
            , co_ax_tc :: TyCon
co_ax_tc       = TyCon
fam_tc
            , co_ax_role :: Role
co_ax_role     = Role
Nominal
            , co_ax_implicit :: Bool
co_ax_implicit = Bool
False
            , co_ax_branches :: Branches Branched
co_ax_branches = [CoAxBranch] -> Branches Branched
manyBranches ([CoAxBranch] -> [CoAxBranch]
computeAxiomIncomps [CoAxBranch]
branches) }

mkUnbranchedCoAxiom :: Name -> TyCon -> CoAxBranch -> CoAxiom Unbranched
mkUnbranchedCoAxiom :: Name -> TyCon -> CoAxBranch -> CoAxiom Unbranched
mkUnbranchedCoAxiom Name
ax_name TyCon
fam_tc CoAxBranch
branch
  = CoAxiom :: forall (br :: BranchFlag).
Unique
-> Name -> Role -> TyCon -> Branches br -> Bool -> CoAxiom br
CoAxiom { co_ax_unique :: Unique
co_ax_unique   = Name -> Unique
nameUnique Name
ax_name
            , co_ax_name :: Name
co_ax_name     = Name
ax_name
            , co_ax_tc :: TyCon
co_ax_tc       = TyCon
fam_tc
            , co_ax_role :: Role
co_ax_role     = Role
Nominal
            , co_ax_implicit :: Bool
co_ax_implicit = Bool
False
            , co_ax_branches :: Branches Unbranched
co_ax_branches = CoAxBranch -> Branches Unbranched
unbranched (CoAxBranch
branch { cab_incomps :: [CoAxBranch]
cab_incomps = [] }) }

mkSingleCoAxiom :: Role -> Name
                -> [TyVar] -> [TyVar] -> [CoVar]
                -> TyCon -> [Type] -> Type
                -> CoAxiom Unbranched
-- Make a single-branch CoAxiom, including making the branch itself
-- Used for both type family (Nominal) and data family (Representational)
-- axioms, hence passing in the Role
mkSingleCoAxiom :: Role
-> Name
-> [TyVar]
-> [TyVar]
-> [TyVar]
-> TyCon
-> [Type]
-> Type
-> CoAxiom Unbranched
mkSingleCoAxiom Role
role Name
ax_name [TyVar]
tvs [TyVar]
eta_tvs [TyVar]
cvs TyCon
fam_tc [Type]
lhs_tys Type
rhs_ty
  = CoAxiom :: forall (br :: BranchFlag).
Unique
-> Name -> Role -> TyCon -> Branches br -> Bool -> CoAxiom br
CoAxiom { co_ax_unique :: Unique
co_ax_unique   = Name -> Unique
nameUnique Name
ax_name
            , co_ax_name :: Name
co_ax_name     = Name
ax_name
            , co_ax_tc :: TyCon
co_ax_tc       = TyCon
fam_tc
            , co_ax_role :: Role
co_ax_role     = Role
role
            , co_ax_implicit :: Bool
co_ax_implicit = Bool
False
            , co_ax_branches :: Branches Unbranched
co_ax_branches = CoAxBranch -> Branches Unbranched
unbranched (CoAxBranch
branch { cab_incomps :: [CoAxBranch]
cab_incomps = [] }) }
  where
    branch :: CoAxBranch
branch = [TyVar]
-> [TyVar]
-> [TyVar]
-> [Type]
-> Type
-> [Role]
-> SrcSpan
-> CoAxBranch
mkCoAxBranch [TyVar]
tvs [TyVar]
eta_tvs [TyVar]
cvs [Type]
lhs_tys Type
rhs_ty
                          ((TyVar -> Role) -> [TyVar] -> [Role]
forall a b. (a -> b) -> [a] -> [b]
map (Role -> TyVar -> Role
forall a b. a -> b -> a
const Role
Nominal) [TyVar]
tvs)
                          (Name -> SrcSpan
forall a. NamedThing a => a -> SrcSpan
getSrcSpan Name
ax_name)

-- | Create a coercion constructor (axiom) suitable for the given
--   newtype 'TyCon'. The 'Name' should be that of a new coercion
--   'CoAxiom', the 'TyVar's the arguments expected by the @newtype@ and
--   the type the appropriate right hand side of the @newtype@, with
--   the free variables a subset of those 'TyVar's.
mkNewTypeCoAxiom :: Name -> TyCon -> [TyVar] -> [Role] -> Type -> CoAxiom Unbranched
mkNewTypeCoAxiom :: Name -> TyCon -> [TyVar] -> [Role] -> Type -> CoAxiom Unbranched
mkNewTypeCoAxiom Name
name TyCon
tycon [TyVar]
tvs [Role]
roles Type
rhs_ty
  = CoAxiom :: forall (br :: BranchFlag).
Unique
-> Name -> Role -> TyCon -> Branches br -> Bool -> CoAxiom br
CoAxiom { co_ax_unique :: Unique
co_ax_unique   = Name -> Unique
nameUnique Name
name
            , co_ax_name :: Name
co_ax_name     = Name
name
            , co_ax_implicit :: Bool
co_ax_implicit = Bool
True  -- See Note [Implicit axioms] in GHC.Core.TyCon
            , co_ax_role :: Role
co_ax_role     = Role
Representational
            , co_ax_tc :: TyCon
co_ax_tc       = TyCon
tycon
            , co_ax_branches :: Branches Unbranched
co_ax_branches = CoAxBranch -> Branches Unbranched
unbranched (CoAxBranch
branch { cab_incomps :: [CoAxBranch]
cab_incomps = [] }) }
  where
    branch :: CoAxBranch
branch = [TyVar]
-> [TyVar]
-> [TyVar]
-> [Type]
-> Type
-> [Role]
-> SrcSpan
-> CoAxBranch
mkCoAxBranch [TyVar]
tvs [] [] ([TyVar] -> [Type]
mkTyVarTys [TyVar]
tvs) Type
rhs_ty
                          [Role]
roles (Name -> SrcSpan
forall a. NamedThing a => a -> SrcSpan
getSrcSpan Name
name)

{-
************************************************************************
*                                                                      *
                Looking up a family instance
*                                                                      *
************************************************************************

@lookupFamInstEnv@ looks up in a @FamInstEnv@, using a one-way match.
Multiple matches are only possible in case of type families (not data
families), and then, it doesn't matter which match we choose (as the
instances are guaranteed confluent).

We return the matching family instances and the type instance at which it
matches.  For example, if we lookup 'T [Int]' and have a family instance

  data instance T [a] = ..

desugared to

  data :R42T a = ..
  coe :Co:R42T a :: T [a] ~ :R42T a

we return the matching instance '(FamInst{.., fi_tycon = :R42T}, Int)'.
-}

-- when matching a type family application, we get a FamInst,
-- and the list of types the axiom should be applied to
data FamInstMatch = FamInstMatch { FamInstMatch -> FamInst
fim_instance :: FamInst
                                 , FamInstMatch -> [Type]
fim_tys      :: [Type]
                                 , FamInstMatch -> [Coercion]
fim_cos      :: [Coercion]
                                 }
  -- See Note [Over-saturated matches]

instance Outputable FamInstMatch where
  ppr :: FamInstMatch -> SDoc
ppr (FamInstMatch { fim_instance :: FamInstMatch -> FamInst
fim_instance = FamInst
inst
                    , fim_tys :: FamInstMatch -> [Type]
fim_tys      = [Type]
tys
                    , fim_cos :: FamInstMatch -> [Coercion]
fim_cos      = [Coercion]
cos })
    = String -> SDoc
text String
"match with" SDoc -> SDoc -> SDoc
<+> SDoc -> SDoc
parens (FamInst -> SDoc
forall a. Outputable a => a -> SDoc
ppr FamInst
inst) SDoc -> SDoc -> SDoc
<+> [Type] -> SDoc
forall a. Outputable a => a -> SDoc
ppr [Type]
tys SDoc -> SDoc -> SDoc
<+> [Coercion] -> SDoc
forall a. Outputable a => a -> SDoc
ppr [Coercion]
cos

lookupFamInstEnvByTyCon :: FamInstEnvs -> TyCon -> [FamInst]
lookupFamInstEnvByTyCon :: (FamInstEnv, FamInstEnv) -> TyCon -> [FamInst]
lookupFamInstEnvByTyCon (FamInstEnv
pkg_ie, FamInstEnv
home_ie) TyCon
fam_tc
  = FamInstEnv -> [FamInst]
get FamInstEnv
pkg_ie [FamInst] -> [FamInst] -> [FamInst]
forall a. [a] -> [a] -> [a]
++ FamInstEnv -> [FamInst]
get FamInstEnv
home_ie
  where
    get :: FamInstEnv -> [FamInst]
get FamInstEnv
ie = case FamInstEnv -> TyCon -> Maybe FamilyInstEnv
forall key elt.
Uniquable key =>
UniqDFM key elt -> key -> Maybe elt
lookupUDFM FamInstEnv
ie TyCon
fam_tc of
               Maybe FamilyInstEnv
Nothing          -> []
               Just (FamIE [FamInst]
fis) -> [FamInst]
fis

lookupFamInstEnv
    :: FamInstEnvs
    -> TyCon -> [Type]          -- What we are looking for
    -> [FamInstMatch]           -- Successful matches
-- Precondition: the tycon is saturated (or over-saturated)

lookupFamInstEnv :: (FamInstEnv, FamInstEnv) -> TyCon -> [Type] -> [FamInstMatch]
lookupFamInstEnv
   = MatchFun
-> (FamInstEnv, FamInstEnv) -> TyCon -> [Type] -> [FamInstMatch]
lookup_fam_inst_env MatchFun
forall {p} {p}. p -> p -> [Type] -> [Type] -> Maybe TCvSubst
match
   where
     match :: p -> p -> [Type] -> [Type] -> Maybe TCvSubst
match p
_ p
_ [Type]
tpl_tys [Type]
tys = [Type] -> [Type] -> Maybe TCvSubst
tcMatchTys [Type]
tpl_tys [Type]
tys

lookupFamInstEnvConflicts
    :: FamInstEnvs
    -> FamInst          -- Putative new instance
    -> [FamInstMatch]   -- Conflicting matches (don't look at the fim_tys field)
-- E.g. when we are about to add
--    f : type instance F [a] = a->a
-- we do (lookupFamInstConflicts f [b])
-- to find conflicting matches
--
-- Precondition: the tycon is saturated (or over-saturated)

lookupFamInstEnvConflicts :: (FamInstEnv, FamInstEnv) -> FamInst -> [FamInstMatch]
lookupFamInstEnvConflicts (FamInstEnv, FamInstEnv)
envs fam_inst :: FamInst
fam_inst@(FamInst { fi_axiom :: FamInst -> CoAxiom Unbranched
fi_axiom = CoAxiom Unbranched
new_axiom })
  = MatchFun
-> (FamInstEnv, FamInstEnv) -> TyCon -> [Type] -> [FamInstMatch]
lookup_fam_inst_env MatchFun
my_unify (FamInstEnv, FamInstEnv)
envs TyCon
fam [Type]
tys
  where
    (TyCon
fam, [Type]
tys) = FamInst -> (TyCon, [Type])
famInstSplitLHS FamInst
fam_inst
        -- In example above,   fam tys' = F [b]

    my_unify :: MatchFun
my_unify (FamInst { fi_axiom :: FamInst -> CoAxiom Unbranched
fi_axiom = CoAxiom Unbranched
old_axiom }) VarSet
tpl_tvs [Type]
tpl_tys [Type]
_
       = ASSERT2( tyCoVarsOfTypes tys `disjointVarSet` tpl_tvs,
                  (ppr fam <+> ppr tys) $$
                  (ppr tpl_tvs <+> ppr tpl_tys) )
                -- Unification will break badly if the variables overlap
                -- They shouldn't because we allocate separate uniques for them
         if CoAxBranch -> CoAxBranch -> Bool
compatibleBranches (CoAxiom Unbranched -> CoAxBranch
coAxiomSingleBranch CoAxiom Unbranched
old_axiom) CoAxBranch
new_branch
           then Maybe TCvSubst
forall a. Maybe a
Nothing
           else TCvSubst -> Maybe TCvSubst
forall a. a -> Maybe a
Just TCvSubst
forall {a}. a
noSubst
      -- Note [Family instance overlap conflicts]

    noSubst :: a
noSubst = String -> a
forall a. String -> a
panic String
"lookupFamInstEnvConflicts noSubst"
    new_branch :: CoAxBranch
new_branch = CoAxiom Unbranched -> CoAxBranch
coAxiomSingleBranch CoAxiom Unbranched
new_axiom

--------------------------------------------------------------------------------
--                 Type family injectivity checking bits                      --
--------------------------------------------------------------------------------

{- Note [Verifying injectivity annotation]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

Injectivity means that the RHS of a type family uniquely determines the LHS (see
Note [Type inference for type families with injectivity]).  The user informs us about
injectivity using an injectivity annotation and it is GHC's task to verify that
this annotation is correct w.r.t. type family equations. Whenever we see a new
equation of a type family we need to make sure that adding this equation to the
already known equations of a type family does not violate the injectivity annotation
supplied by the user (see Note [Injectivity annotation]).  Of course if the type
family has no injectivity annotation then no check is required.  But if a type
family has injectivity annotation we need to make sure that the following
conditions hold:

1. For each pair of *different* equations of a type family, one of the following
   conditions holds:

   A:  RHSs are different. (Check done in GHC.Core.FamInstEnv.injectiveBranches)

   B1: OPEN TYPE FAMILIES: If the RHSs can be unified under some substitution
       then it must be possible to unify the LHSs under the same substitution.
       Example:

          type family FunnyId a = r | r -> a
          type instance FunnyId Int = Int
          type instance FunnyId a = a

       RHSs of these two equations unify under [ a |-> Int ] substitution.
       Under this substitution LHSs are equal therefore these equations don't
       violate injectivity annotation. (Check done in GHC.Core.FamInstEnv.injectiveBranches)

   B2: CLOSED TYPE FAMILIES: If the RHSs can be unified under some
       substitution then either the LHSs unify under the same substitution or
       the LHS of the latter equation is overlapped by earlier equations.
       Example 1:

          type family SwapIntChar a = r | r -> a where
              SwapIntChar Int  = Char
              SwapIntChar Char = Int
              SwapIntChar a    = a

       Say we are checking the last two equations. RHSs unify under [ a |->
       Int ] substitution but LHSs don't. So we apply the substitution to LHS
       of last equation and check whether it is overlapped by any of previous
       equations. Since it is overlapped by the first equation we conclude
       that pair of last two equations does not violate injectivity
       annotation. (Check done in GHC.Tc.Validity.checkValidCoAxiom#gather_conflicts)

   A special case of B is when RHSs unify with an empty substitution ie. they
   are identical.

   If any of the above two conditions holds we conclude that the pair of
   equations does not violate injectivity annotation. But if we find a pair
   of equations where neither of the above holds we report that this pair
   violates injectivity annotation because for a given RHS we don't have a
   unique LHS. (Note that (B) actually implies (A).)

   Note that we only take into account these LHS patterns that were declared
   as injective.

2. If an RHS of a type family equation is a bare type variable then
   all LHS variables (including implicit kind variables) also have to be bare.
   In other words, this has to be a sole equation of that type family and it has
   to cover all possible patterns.  So for example this definition will be
   rejected:

      type family W1 a = r | r -> a
      type instance W1 [a] = a

   If it were accepted we could call `W1 [W1 Int]`, which would reduce to
   `W1 Int` and then by injectivity we could conclude that `[W1 Int] ~ Int`,
   which is bogus. Checked FamInst.bareTvInRHSViolated.

3. If the RHS of a type family equation is a type family application then the type
   family is rejected as not injective. This is checked by FamInst.isTFHeaded.

4. If a LHS type variable that is declared as injective is not mentioned in an
   injective position in the RHS then the type family is rejected as not
   injective.  "Injective position" means either an argument to a type
   constructor or argument to a type family on injective position.
   There are subtleties here. See Note [Coverage condition for injective type families]
   in GHC.Tc.Instance.Family.

Check (1) must be done for all family instances (transitively) imported. Other
checks (2-4) should be done just for locally written equations, as they are checks
involving just a single equation, not about interactions. Doing the other checks for
imported equations led to #17405, as the behavior of check (4) depends on
-XUndecidableInstances (see Note [Coverage condition for injective type families] in
FamInst), which may vary between modules.

See also Note [Injective type families] in GHC.Core.TyCon
-}


-- | Check whether an open type family equation can be added to already existing
-- instance environment without causing conflicts with supplied injectivity
-- annotations.  Returns list of conflicting axioms (type instance
-- declarations).
lookupFamInstEnvInjectivityConflicts
    :: [Bool]         -- injectivity annotation for this type family instance
                      -- INVARIANT: list contains at least one True value
    ->  FamInstEnvs   -- all type instances seens so far
    ->  FamInst       -- new type instance that we're checking
    -> [CoAxBranch]   -- conflicting instance declarations
lookupFamInstEnvInjectivityConflicts :: [Bool] -> (FamInstEnv, FamInstEnv) -> FamInst -> [CoAxBranch]
lookupFamInstEnvInjectivityConflicts [Bool]
injList (FamInstEnv
pkg_ie, FamInstEnv
home_ie)
                             fam_inst :: FamInst
fam_inst@(FamInst { fi_axiom :: FamInst -> CoAxiom Unbranched
fi_axiom = CoAxiom Unbranched
new_axiom })
  -- See Note [Verifying injectivity annotation]. This function implements
  -- check (1.B1) for open type families described there.
  = FamInstEnv -> [CoAxBranch]
lookup_inj_fam_conflicts FamInstEnv
home_ie [CoAxBranch] -> [CoAxBranch] -> [CoAxBranch]
forall a. [a] -> [a] -> [a]
++ FamInstEnv -> [CoAxBranch]
lookup_inj_fam_conflicts FamInstEnv
pkg_ie
    where
      fam :: TyCon
fam        = FamInst -> TyCon
famInstTyCon FamInst
fam_inst
      new_branch :: CoAxBranch
new_branch = CoAxiom Unbranched -> CoAxBranch
coAxiomSingleBranch CoAxiom Unbranched
new_axiom

      -- filtering function used by `lookup_inj_fam_conflicts` to check whether
      -- a pair of equations conflicts with the injectivity annotation.
      isInjConflict :: FamInst -> Bool
isInjConflict (FamInst { fi_axiom :: FamInst -> CoAxiom Unbranched
fi_axiom = CoAxiom Unbranched
old_axiom })
          | InjectivityCheckResult
InjectivityAccepted <-
            [Bool] -> CoAxBranch -> CoAxBranch -> InjectivityCheckResult
injectiveBranches [Bool]
injList (CoAxiom Unbranched -> CoAxBranch
coAxiomSingleBranch CoAxiom Unbranched
old_axiom) CoAxBranch
new_branch
          = Bool
False -- no conflict
          | Bool
otherwise = Bool
True

      lookup_inj_fam_conflicts :: FamInstEnv -> [CoAxBranch]
lookup_inj_fam_conflicts FamInstEnv
ie
          | TyCon -> Bool
isOpenFamilyTyCon TyCon
fam, Just (FamIE [FamInst]
insts) <- FamInstEnv -> TyCon -> Maybe FamilyInstEnv
forall key elt.
Uniquable key =>
UniqDFM key elt -> key -> Maybe elt
lookupUDFM FamInstEnv
ie TyCon
fam
          = (FamInst -> CoAxBranch) -> [FamInst] -> [CoAxBranch]
forall a b. (a -> b) -> [a] -> [b]
map (CoAxiom Unbranched -> CoAxBranch
coAxiomSingleBranch (CoAxiom Unbranched -> CoAxBranch)
-> (FamInst -> CoAxiom Unbranched) -> FamInst -> CoAxBranch
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FamInst -> CoAxiom Unbranched
fi_axiom) ([FamInst] -> [CoAxBranch]) -> [FamInst] -> [CoAxBranch]
forall a b. (a -> b) -> a -> b
$
            (FamInst -> Bool) -> [FamInst] -> [FamInst]
forall a. (a -> Bool) -> [a] -> [a]
filter FamInst -> Bool
isInjConflict [FamInst]
insts
          | Bool
otherwise = []


--------------------------------------------------------------------------------
--                    Type family overlap checking bits                       --
--------------------------------------------------------------------------------

{-
Note [Family instance overlap conflicts]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
- In the case of data family instances, any overlap is fundamentally a
  conflict (as these instances imply injective type mappings).

- In the case of type family instances, overlap is admitted as long as
  the right-hand sides of the overlapping rules coincide under the
  overlap substitution.  eg
       type instance F a Int = a
       type instance F Int b = b
  These two overlap on (F Int Int) but then both RHSs are Int,
  so all is well. We require that they are syntactically equal;
  anything else would be difficult to test for at this stage.
-}

------------------------------------------------------------
-- Might be a one-way match or a unifier
type MatchFun =  FamInst                -- The FamInst template
              -> TyVarSet -> [Type]     --   fi_tvs, fi_tys of that FamInst
              -> [Type]                 -- Target to match against
              -> Maybe TCvSubst

lookup_fam_inst_env'          -- The worker, local to this module
    :: MatchFun
    -> FamInstEnv
    -> TyCon -> [Type]        -- What we are looking for
    -> [FamInstMatch]
lookup_fam_inst_env' :: MatchFun -> FamInstEnv -> TyCon -> [Type] -> [FamInstMatch]
lookup_fam_inst_env' MatchFun
match_fun FamInstEnv
ie TyCon
fam [Type]
match_tys
  | TyCon -> Bool
isOpenFamilyTyCon TyCon
fam
  , Just (FamIE [FamInst]
insts) <- FamInstEnv -> TyCon -> Maybe FamilyInstEnv
forall key elt.
Uniquable key =>
UniqDFM key elt -> key -> Maybe elt
lookupUDFM FamInstEnv
ie TyCon
fam
  = [FamInst] -> [FamInstMatch]
find [FamInst]
insts    -- The common case
  | Bool
otherwise = []
  where

    find :: [FamInst] -> [FamInstMatch]
find [] = []
    find (item :: FamInst
item@(FamInst { fi_tcs :: FamInst -> [Maybe Name]
fi_tcs = [Maybe Name]
mb_tcs, fi_tvs :: FamInst -> [TyVar]
fi_tvs = [TyVar]
tpl_tvs, fi_cvs :: FamInst -> [TyVar]
fi_cvs = [TyVar]
tpl_cvs
                        , fi_tys :: FamInst -> [Type]
fi_tys = [Type]
tpl_tys }) : [FamInst]
rest)
        -- Fast check for no match, uses the "rough match" fields
      | [Maybe Name] -> [Maybe Name] -> Bool
instanceCantMatch [Maybe Name]
rough_tcs [Maybe Name]
mb_tcs
      = [FamInst] -> [FamInstMatch]
find [FamInst]
rest

        -- Proper check
      | Just TCvSubst
subst <- MatchFun
match_fun FamInst
item ([TyVar] -> VarSet
mkVarSet [TyVar]
tpl_tvs) [Type]
tpl_tys [Type]
match_tys1
      = (FamInstMatch :: FamInst -> [Type] -> [Coercion] -> FamInstMatch
FamInstMatch { fim_instance :: FamInst
fim_instance = FamInst
item
                      , fim_tys :: [Type]
fim_tys      = TCvSubst -> [TyVar] -> [Type]
substTyVars TCvSubst
subst [TyVar]
tpl_tvs [Type] -> [Type] -> [Type]
forall a. [a] -> [a] -> [a]
`chkAppend` [Type]
match_tys2
                      , fim_cos :: [Coercion]
fim_cos      = ASSERT( all (isJust . lookupCoVar subst) tpl_cvs )
                                       TCvSubst -> [TyVar] -> [Coercion]
substCoVars TCvSubst
subst [TyVar]
tpl_cvs
                      })
        FamInstMatch -> [FamInstMatch] -> [FamInstMatch]
forall a. a -> [a] -> [a]
: [FamInst] -> [FamInstMatch]
find [FamInst]
rest

        -- No match => try next
      | Bool
otherwise
      = [FamInst] -> [FamInstMatch]
find [FamInst]
rest
      where
        ([Maybe Name]
rough_tcs, [Type]
match_tys1, [Type]
match_tys2) = [Type] -> ([Maybe Name], [Type], [Type])
split_tys [Type]
tpl_tys

      -- Precondition: the tycon is saturated (or over-saturated)

    -- Deal with over-saturation
    -- See Note [Over-saturated matches]
    split_tys :: [Type] -> ([Maybe Name], [Type], [Type])
split_tys [Type]
tpl_tys
      | TyCon -> Bool
isTypeFamilyTyCon TyCon
fam
      = ([Maybe Name], [Type], [Type])
pre_rough_split_tys

      | Bool
otherwise
      = let ([Type]
match_tys1, [Type]
match_tys2) = [Type] -> [Type] -> ([Type], [Type])
forall b a. [b] -> [a] -> ([a], [a])
splitAtList [Type]
tpl_tys [Type]
match_tys
            rough_tcs :: [Maybe Name]
rough_tcs = [Type] -> [Maybe Name]
roughMatchTcs [Type]
match_tys1
        in ([Maybe Name]
rough_tcs, [Type]
match_tys1, [Type]
match_tys2)

    ([Type]
pre_match_tys1, [Type]
pre_match_tys2) = Arity -> [Type] -> ([Type], [Type])
forall a. Arity -> [a] -> ([a], [a])
splitAt (TyCon -> Arity
tyConArity TyCon
fam) [Type]
match_tys
    pre_rough_split_tys :: ([Maybe Name], [Type], [Type])
pre_rough_split_tys
      = ([Type] -> [Maybe Name]
roughMatchTcs [Type]
pre_match_tys1, [Type]
pre_match_tys1, [Type]
pre_match_tys2)

lookup_fam_inst_env           -- The worker, local to this module
    :: MatchFun
    -> FamInstEnvs
    -> TyCon -> [Type]        -- What we are looking for
    -> [FamInstMatch]         -- Successful matches

-- Precondition: the tycon is saturated (or over-saturated)

lookup_fam_inst_env :: MatchFun
-> (FamInstEnv, FamInstEnv) -> TyCon -> [Type] -> [FamInstMatch]
lookup_fam_inst_env MatchFun
match_fun (FamInstEnv
pkg_ie, FamInstEnv
home_ie) TyCon
fam [Type]
tys
  =  MatchFun -> FamInstEnv -> TyCon -> [Type] -> [FamInstMatch]
lookup_fam_inst_env' MatchFun
match_fun FamInstEnv
home_ie TyCon
fam [Type]
tys
  [FamInstMatch] -> [FamInstMatch] -> [FamInstMatch]
forall a. [a] -> [a] -> [a]
++ MatchFun -> FamInstEnv -> TyCon -> [Type] -> [FamInstMatch]
lookup_fam_inst_env' MatchFun
match_fun FamInstEnv
pkg_ie  TyCon
fam [Type]
tys

{-
Note [Over-saturated matches]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
It's ok to look up an over-saturated type constructor.  E.g.
     type family F a :: * -> *
     type instance F (a,b) = Either (a->b)

The type instance gives rise to a newtype TyCon (at a higher kind
which you can't do in Haskell!):
     newtype FPair a b = FP (Either (a->b))

Then looking up (F (Int,Bool) Char) will return a FamInstMatch
     (FPair, [Int,Bool,Char])
The "extra" type argument [Char] just stays on the end.

We handle data families and type families separately here:

 * For type families, all instances of a type family must have the
   same arity, so we can precompute the split between the match_tys
   and the overflow tys. This is done in pre_rough_split_tys.

 * For data family instances, though, we need to re-split for each
   instance, because the breakdown might be different for each
   instance.  Why?  Because of eta reduction; see
   Note [Eta reduction for data families] in GHC.Core.Coercion.Axiom.
-}

-- checks if one LHS is dominated by a list of other branches
-- in other words, if an application would match the first LHS, it is guaranteed
-- to match at least one of the others. The RHSs are ignored.
-- This algorithm is conservative:
--   True -> the LHS is definitely covered by the others
--   False -> no information
-- It is currently (Oct 2012) used only for generating errors for
-- inaccessible branches. If these errors go unreported, no harm done.
-- This is defined here to avoid a dependency from CoAxiom to Unify
isDominatedBy :: CoAxBranch -> [CoAxBranch] -> Bool
isDominatedBy :: CoAxBranch -> [CoAxBranch] -> Bool
isDominatedBy CoAxBranch
branch [CoAxBranch]
branches
  = [Bool] -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
or ([Bool] -> Bool) -> [Bool] -> Bool
forall a b. (a -> b) -> a -> b
$ (CoAxBranch -> Bool) -> [CoAxBranch] -> [Bool]
forall a b. (a -> b) -> [a] -> [b]
map CoAxBranch -> Bool
match [CoAxBranch]
branches
    where
      lhs :: [Type]
lhs = CoAxBranch -> [Type]
coAxBranchLHS CoAxBranch
branch
      match :: CoAxBranch -> Bool
match (CoAxBranch { cab_lhs :: CoAxBranch -> [Type]
cab_lhs = [Type]
tys })
        = Maybe TCvSubst -> Bool
forall a. Maybe a -> Bool
isJust (Maybe TCvSubst -> Bool) -> Maybe TCvSubst -> Bool
forall a b. (a -> b) -> a -> b
$ [Type] -> [Type] -> Maybe TCvSubst
tcMatchTys [Type]
tys [Type]
lhs

{-
************************************************************************
*                                                                      *
                Choosing an axiom application
*                                                                      *
************************************************************************

The lookupFamInstEnv function does a nice job for *open* type families,
but we also need to handle closed ones when normalising a type:
-}

reduceTyFamApp_maybe :: FamInstEnvs
                     -> Role              -- Desired role of result coercion
                     -> TyCon -> [Type]
                     -> Maybe (Coercion, Type)
-- Attempt to do a *one-step* reduction of a type-family application
--    but *not* newtypes
-- Works on type-synonym families always; data-families only if
--     the role we seek is representational
-- It does *not* normalise the type arguments first, so this may not
--     go as far as you want. If you want normalised type arguments,
--     use topReduceTyFamApp_maybe
--
-- The TyCon can be oversaturated.
-- Works on both open and closed families
--
-- Always returns a *homogeneous* coercion -- type family reductions are always
-- homogeneous
reduceTyFamApp_maybe :: (FamInstEnv, FamInstEnv)
-> Role -> TyCon -> [Type] -> Maybe (Coercion, Type)
reduceTyFamApp_maybe (FamInstEnv, FamInstEnv)
envs Role
role TyCon
tc [Type]
tys
  | Role
Phantom <- Role
role
  = Maybe (Coercion, Type)
forall a. Maybe a
Nothing

  | case Role
role of
      Role
Representational -> TyCon -> Bool
isOpenFamilyTyCon     TyCon
tc
      Role
_                -> TyCon -> Bool
isOpenTypeFamilyTyCon TyCon
tc
       -- If we seek a representational coercion
       -- (e.g. the call in topNormaliseType_maybe) then we can
       -- unwrap data families as well as type-synonym families;
       -- otherwise only type-synonym families
  , FamInstMatch { fim_instance :: FamInstMatch -> FamInst
fim_instance = FamInst { fi_axiom :: FamInst -> CoAxiom Unbranched
fi_axiom = CoAxiom Unbranched
ax }
                 , fim_tys :: FamInstMatch -> [Type]
fim_tys      = [Type]
inst_tys
                 , fim_cos :: FamInstMatch -> [Coercion]
fim_cos      = [Coercion]
inst_cos } : [FamInstMatch]
_ <- (FamInstEnv, FamInstEnv) -> TyCon -> [Type] -> [FamInstMatch]
lookupFamInstEnv (FamInstEnv, FamInstEnv)
envs TyCon
tc [Type]
tys
      -- NB: Allow multiple matches because of compatible overlap

  = let co :: Coercion
co = Role -> CoAxiom Unbranched -> [Type] -> [Coercion] -> Coercion
mkUnbranchedAxInstCo Role
role CoAxiom Unbranched
ax [Type]
inst_tys [Coercion]
inst_cos
        ty :: Type
ty = Coercion -> Type
coercionRKind Coercion
co
    in (Coercion, Type) -> Maybe (Coercion, Type)
forall a. a -> Maybe a
Just (Coercion
co, Type
ty)

  | Just CoAxiom Branched
ax <- TyCon -> Maybe (CoAxiom Branched)
isClosedSynFamilyTyConWithAxiom_maybe TyCon
tc
  , Just (Arity
ind, [Type]
inst_tys, [Coercion]
inst_cos) <- CoAxiom Branched -> [Type] -> Maybe (Arity, [Type], [Coercion])
chooseBranch CoAxiom Branched
ax [Type]
tys
  = let co :: Coercion
co = Role
-> CoAxiom Branched -> Arity -> [Type] -> [Coercion] -> Coercion
forall (br :: BranchFlag).
Role -> CoAxiom br -> Arity -> [Type] -> [Coercion] -> Coercion
mkAxInstCo Role
role CoAxiom Branched
ax Arity
ind [Type]
inst_tys [Coercion]
inst_cos
        ty :: Type
ty = Coercion -> Type
coercionRKind Coercion
co
    in (Coercion, Type) -> Maybe (Coercion, Type)
forall a. a -> Maybe a
Just (Coercion
co, Type
ty)

  | Just BuiltInSynFamily
ax           <- TyCon -> Maybe BuiltInSynFamily
isBuiltInSynFamTyCon_maybe TyCon
tc
  , Just (CoAxiomRule
coax,[Type]
ts,Type
ty) <- BuiltInSynFamily -> [Type] -> Maybe (CoAxiomRule, [Type], Type)
sfMatchFam BuiltInSynFamily
ax [Type]
tys
  = let co :: Coercion
co = CoAxiomRule -> [Coercion] -> Coercion
mkAxiomRuleCo CoAxiomRule
coax ((Role -> Type -> Coercion) -> [Role] -> [Type] -> [Coercion]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith Role -> Type -> Coercion
mkReflCo (CoAxiomRule -> [Role]
coaxrAsmpRoles CoAxiomRule
coax) [Type]
ts)
    in (Coercion, Type) -> Maybe (Coercion, Type)
forall a. a -> Maybe a
Just (Coercion
co, Type
ty)

  | Bool
otherwise
  = Maybe (Coercion, Type)
forall a. Maybe a
Nothing

-- The axiom can be oversaturated. (Closed families only.)
chooseBranch :: CoAxiom Branched -> [Type]
             -> Maybe (BranchIndex, [Type], [Coercion])  -- found match, with args
chooseBranch :: CoAxiom Branched -> [Type] -> Maybe (Arity, [Type], [Coercion])
chooseBranch CoAxiom Branched
axiom [Type]
tys
  = do { let num_pats :: Arity
num_pats = CoAxiom Branched -> Arity
forall (br :: BranchFlag). CoAxiom br -> Arity
coAxiomNumPats CoAxiom Branched
axiom
             ([Type]
target_tys, [Type]
extra_tys) = Arity -> [Type] -> ([Type], [Type])
forall a. Arity -> [a] -> ([a], [a])
splitAt Arity
num_pats [Type]
tys
             branches :: Branches Branched
branches = CoAxiom Branched -> Branches Branched
forall (br :: BranchFlag). CoAxiom br -> Branches br
coAxiomBranches CoAxiom Branched
axiom
       ; (Arity
ind, [Type]
inst_tys, [Coercion]
inst_cos)
           <- Array Arity CoAxBranch
-> [Type] -> Maybe (Arity, [Type], [Coercion])
findBranch (Branches Branched -> Array Arity CoAxBranch
forall (br :: BranchFlag). Branches br -> Array Arity CoAxBranch
unMkBranches Branches Branched
branches) [Type]
target_tys
       ; (Arity, [Type], [Coercion]) -> Maybe (Arity, [Type], [Coercion])
forall (m :: * -> *) a. Monad m => a -> m a
return ( Arity
ind, [Type]
inst_tys [Type] -> [Type] -> [Type]
forall a. [a] -> [a] -> [a]
`chkAppend` [Type]
extra_tys, [Coercion]
inst_cos ) }

-- The axiom must *not* be oversaturated
findBranch :: Array BranchIndex CoAxBranch
           -> [Type]
           -> Maybe (BranchIndex, [Type], [Coercion])
    -- coercions relate requested types to returned axiom LHS at role N
findBranch :: Array Arity CoAxBranch
-> [Type] -> Maybe (Arity, [Type], [Coercion])
findBranch Array Arity CoAxBranch
branches [Type]
target_tys
  = ((Arity, CoAxBranch)
 -> Maybe (Arity, [Type], [Coercion])
 -> Maybe (Arity, [Type], [Coercion]))
-> Maybe (Arity, [Type], [Coercion])
-> [(Arity, CoAxBranch)]
-> Maybe (Arity, [Type], [Coercion])
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (Arity, CoAxBranch)
-> Maybe (Arity, [Type], [Coercion])
-> Maybe (Arity, [Type], [Coercion])
go Maybe (Arity, [Type], [Coercion])
forall a. Maybe a
Nothing (Array Arity CoAxBranch -> [(Arity, CoAxBranch)]
forall i e. Ix i => Array i e -> [(i, e)]
assocs Array Arity CoAxBranch
branches)
  where
    go :: (BranchIndex, CoAxBranch)
       -> Maybe (BranchIndex, [Type], [Coercion])
       -> Maybe (BranchIndex, [Type], [Coercion])
    go :: (Arity, CoAxBranch)
-> Maybe (Arity, [Type], [Coercion])
-> Maybe (Arity, [Type], [Coercion])
go (Arity
index, CoAxBranch
branch) Maybe (Arity, [Type], [Coercion])
other
      = let (CoAxBranch { cab_tvs :: CoAxBranch -> [TyVar]
cab_tvs = [TyVar]
tpl_tvs, cab_cvs :: CoAxBranch -> [TyVar]
cab_cvs = [TyVar]
tpl_cvs
                        , cab_lhs :: CoAxBranch -> [Type]
cab_lhs = [Type]
tpl_lhs
                        , cab_incomps :: CoAxBranch -> [CoAxBranch]
cab_incomps = [CoAxBranch]
incomps }) = CoAxBranch
branch
            in_scope :: InScopeSet
in_scope = VarSet -> InScopeSet
mkInScopeSet ([VarSet] -> VarSet
unionVarSets ([VarSet] -> VarSet) -> [VarSet] -> VarSet
forall a b. (a -> b) -> a -> b
$
                            (CoAxBranch -> VarSet) -> [CoAxBranch] -> [VarSet]
forall a b. (a -> b) -> [a] -> [b]
map ([Type] -> VarSet
tyCoVarsOfTypes ([Type] -> VarSet)
-> (CoAxBranch -> [Type]) -> CoAxBranch -> VarSet
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CoAxBranch -> [Type]
coAxBranchLHS) [CoAxBranch]
incomps)
            -- See Note [Flattening] below
            flattened_target :: [Type]
flattened_target = InScopeSet -> [Type] -> [Type]
flattenTys InScopeSet
in_scope [Type]
target_tys
        in case [Type] -> [Type] -> Maybe TCvSubst
tcMatchTys [Type]
tpl_lhs [Type]
target_tys of
        Just TCvSubst
subst -- matching worked. now, check for apartness.
          |  [Type] -> CoAxBranch -> Bool
apartnessCheck [Type]
flattened_target CoAxBranch
branch
          -> -- matching worked & we're apart from all incompatible branches.
             -- success
             ASSERT( all (isJust . lookupCoVar subst) tpl_cvs )
             (Arity, [Type], [Coercion]) -> Maybe (Arity, [Type], [Coercion])
forall a. a -> Maybe a
Just (Arity
index, TCvSubst -> [TyVar] -> [Type]
substTyVars TCvSubst
subst [TyVar]
tpl_tvs, TCvSubst -> [TyVar] -> [Coercion]
substCoVars TCvSubst
subst [TyVar]
tpl_cvs)

        -- failure. keep looking
        Maybe TCvSubst
_ -> Maybe (Arity, [Type], [Coercion])
other

-- | Do an apartness check, as described in the "Closed Type Families" paper
-- (POPL '14). This should be used when determining if an equation
-- ('CoAxBranch') of a closed type family can be used to reduce a certain target
-- type family application.
apartnessCheck :: [Type]     -- ^ /flattened/ target arguments. Make sure
                             -- they're flattened! See Note [Flattening].
                             -- (NB: This "flat" is a different
                             -- "flat" than is used in GHC.Tc.Solver.Flatten.)
               -> CoAxBranch -- ^ the candidate equation we wish to use
                             -- Precondition: this matches the target
               -> Bool       -- ^ True <=> equation can fire
apartnessCheck :: [Type] -> CoAxBranch -> Bool
apartnessCheck [Type]
flattened_target (CoAxBranch { cab_incomps :: CoAxBranch -> [CoAxBranch]
cab_incomps = [CoAxBranch]
incomps })
  = (CoAxBranch -> Bool) -> [CoAxBranch] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (UnifyResult -> Bool
forall {a}. UnifyResultM a -> Bool
isSurelyApart
         (UnifyResult -> Bool)
-> (CoAxBranch -> UnifyResult) -> CoAxBranch -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (TyVar -> BindFlag) -> [Type] -> [Type] -> UnifyResult
tcUnifyTysFG (BindFlag -> TyVar -> BindFlag
forall a b. a -> b -> a
const BindFlag
BindMe) [Type]
flattened_target
         ([Type] -> UnifyResult)
-> (CoAxBranch -> [Type]) -> CoAxBranch -> UnifyResult
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CoAxBranch -> [Type]
coAxBranchLHS) [CoAxBranch]
incomps
  where
    isSurelyApart :: UnifyResultM a -> Bool
isSurelyApart UnifyResultM a
SurelyApart = Bool
True
    isSurelyApart UnifyResultM a
_           = Bool
False

{-
************************************************************************
*                                                                      *
                Looking up a family instance
*                                                                      *
************************************************************************

Note [Normalising types]
~~~~~~~~~~~~~~~~~~~~~~~~
The topNormaliseType function removes all occurrences of type families
and newtypes from the top-level structure of a type. normaliseTcApp does
the type family lookup and is fairly straightforward. normaliseType is
a little more involved.

The complication comes from the fact that a type family might be used in the
kind of a variable bound in a forall. We wish to remove this type family
application, but that means coming up with a fresh variable (with the new
kind). Thus, we need a substitution to be built up as we recur through the
type. However, an ordinary TCvSubst just won't do: when we hit a type variable
whose kind has changed during normalisation, we need both the new type
variable *and* the coercion. We could conjure up a new VarEnv with just this
property, but a usable substitution environment already exists:
LiftingContexts from the liftCoSubst family of functions, defined in GHC.Core.Coercion.
A LiftingContext maps a type variable to a coercion and a coercion variable to
a pair of coercions. Let's ignore coercion variables for now. Because the
coercion a type variable maps to contains the destination type (via
coercionKind), we don't need to store that destination type separately. Thus,
a LiftingContext has what we need: a map from type variables to (Coercion,
Type) pairs.

We also benefit because we can piggyback on the liftCoSubstVarBndr function to
deal with binders. However, I had to modify that function to work with this
application. Thus, we now have liftCoSubstVarBndrUsing, which takes
a function used to process the kind of the binder. We don't wish
to lift the kind, but instead normalise it. So, we pass in a callback function
that processes the kind of the binder.

After that brilliant explanation of all this, I'm sure you've forgotten the
dangling reference to coercion variables. What do we do with those? Nothing at
all. The point of normalising types is to remove type family applications, but
there's no sense in removing these from coercions. We would just get back a
new coercion witnessing the equality between the same types as the original
coercion. Because coercions are irrelevant anyway, there is no point in doing
this. So, whenever we encounter a coercion, we just say that it won't change.
That's what the CoercionTy case is doing within normalise_type.

Note [Normalisation and type synonyms]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
We need to be a bit careful about normalising in the presence of type
synonyms (#13035).  Suppose S is a type synonym, and we have
   S t1 t2
If S is family-free (on its RHS) we can just normalise t1 and t2 and
reconstruct (S t1' t2').   Expanding S could not reveal any new redexes
because type families are saturated.

But if S has a type family on its RHS we expand /before/ normalising
the args t1, t2.  If we normalise t1, t2 first, we'll re-normalise them
after expansion, and that can lead to /exponential/ behaviour; see #13035.

Notice, though, that expanding first can in principle duplicate t1,t2,
which might contain redexes. I'm sure you could conjure up an exponential
case by that route too, but it hasn't happened in practice yet!
-}

topNormaliseType :: FamInstEnvs -> Type -> Type
topNormaliseType :: (FamInstEnv, FamInstEnv) -> Type -> Type
topNormaliseType (FamInstEnv, FamInstEnv)
env Type
ty = case (FamInstEnv, FamInstEnv) -> Type -> Maybe (Coercion, Type)
topNormaliseType_maybe (FamInstEnv, FamInstEnv)
env Type
ty of
                            Just (Coercion
_co, Type
ty') -> Type
ty'
                            Maybe (Coercion, Type)
Nothing         -> Type
ty

topNormaliseType_maybe :: FamInstEnvs -> Type -> Maybe (Coercion, Type)

-- ^ Get rid of *outermost* (or toplevel)
--      * type function redex
--      * data family redex
--      * newtypes
-- returning an appropriate Representational coercion.  Specifically, if
--   topNormaliseType_maybe env ty = Just (co, ty')
-- then
--   (a) co :: ty ~R ty'
--   (b) ty' is not a newtype, and is not a type-family or data-family redex
--
-- However, ty' can be something like (Maybe (F ty)), where
-- (F ty) is a redex.
--
-- Always operates homogeneously: the returned type has the same kind as the
-- original type, and the returned coercion is always homogeneous.
topNormaliseType_maybe :: (FamInstEnv, FamInstEnv) -> Type -> Maybe (Coercion, Type)
topNormaliseType_maybe (FamInstEnv, FamInstEnv)
env Type
ty
  = do { ((Coercion
co, MCoercionN
mkind_co), Type
nty) <- NormaliseStepper (Coercion, MCoercionN)
-> ((Coercion, MCoercionN)
    -> (Coercion, MCoercionN) -> (Coercion, MCoercionN))
-> Type
-> Maybe ((Coercion, MCoercionN), Type)
forall ev.
NormaliseStepper ev -> (ev -> ev -> ev) -> Type -> Maybe (ev, Type)
topNormaliseTypeX NormaliseStepper (Coercion, MCoercionN)
stepper (Coercion, MCoercionN)
-> (Coercion, MCoercionN) -> (Coercion, MCoercionN)
combine Type
ty
       ; (Coercion, Type) -> Maybe (Coercion, Type)
forall (m :: * -> *) a. Monad m => a -> m a
return ((Coercion, Type) -> Maybe (Coercion, Type))
-> (Coercion, Type) -> Maybe (Coercion, Type)
forall a b. (a -> b) -> a -> b
$ case MCoercionN
mkind_co of
           MCoercionN
MRefl       -> (Coercion
co, Type
nty)
           MCo Coercion
kind_co -> let nty_casted :: Type
nty_casted = Type
nty Type -> Coercion -> Type
`mkCastTy` Coercion -> Coercion
mkSymCo Coercion
kind_co
                              final_co :: Coercion
final_co   = Role -> Type -> Coercion -> Coercion -> Coercion
mkCoherenceRightCo Role
Representational Type
nty
                                                              (Coercion -> Coercion
mkSymCo Coercion
kind_co) Coercion
co
                          in (Coercion
final_co, Type
nty_casted) }
  where
    stepper :: NormaliseStepper (Coercion, MCoercionN)
stepper = NormaliseStepper (Coercion, MCoercionN)
unwrapNewTypeStepper' NormaliseStepper (Coercion, MCoercionN)
-> NormaliseStepper (Coercion, MCoercionN)
-> NormaliseStepper (Coercion, MCoercionN)
forall ev.
NormaliseStepper ev -> NormaliseStepper ev -> NormaliseStepper ev
`composeSteppers` NormaliseStepper (Coercion, MCoercionN)
tyFamStepper

    combine :: (Coercion, MCoercionN)
-> (Coercion, MCoercionN) -> (Coercion, MCoercionN)
combine (Coercion
c1, MCoercionN
mc1) (Coercion
c2, MCoercionN
mc2) = (Coercion
c1 Coercion -> Coercion -> Coercion
`mkTransCo` Coercion
c2, MCoercionN
mc1 MCoercionN -> MCoercionN -> MCoercionN
`mkTransMCo` MCoercionN
mc2)

    unwrapNewTypeStepper' :: NormaliseStepper (Coercion, MCoercionN)
    unwrapNewTypeStepper' :: NormaliseStepper (Coercion, MCoercionN)
unwrapNewTypeStepper' RecTcChecker
rec_nts TyCon
tc [Type]
tys
      = (Coercion -> (Coercion, MCoercionN))
-> NormaliseStepResult Coercion
-> NormaliseStepResult (Coercion, MCoercionN)
forall ev1 ev2.
(ev1 -> ev2) -> NormaliseStepResult ev1 -> NormaliseStepResult ev2
mapStepResult (, MCoercionN
MRefl) (NormaliseStepResult Coercion
 -> NormaliseStepResult (Coercion, MCoercionN))
-> NormaliseStepResult Coercion
-> NormaliseStepResult (Coercion, MCoercionN)
forall a b. (a -> b) -> a -> b
$ NormaliseStepper Coercion
unwrapNewTypeStepper RecTcChecker
rec_nts TyCon
tc [Type]
tys

      -- second coercion below is the kind coercion relating the original type's kind
      -- to the normalised type's kind
    tyFamStepper :: NormaliseStepper (Coercion, MCoercionN)
    tyFamStepper :: NormaliseStepper (Coercion, MCoercionN)
tyFamStepper RecTcChecker
rec_nts TyCon
tc [Type]
tys  -- Try to step a type/data family
      = case (FamInstEnv, FamInstEnv)
-> TyCon -> [Type] -> Maybe (Coercion, Type, Coercion)
topReduceTyFamApp_maybe (FamInstEnv, FamInstEnv)
env TyCon
tc [Type]
tys of
          Just (Coercion
co, Type
rhs, Coercion
res_co) -> RecTcChecker
-> Type
-> (Coercion, MCoercionN)
-> NormaliseStepResult (Coercion, MCoercionN)
forall ev. RecTcChecker -> Type -> ev -> NormaliseStepResult ev
NS_Step RecTcChecker
rec_nts Type
rhs (Coercion
co, Coercion -> MCoercionN
MCo Coercion
res_co)
          Maybe (Coercion, Type, Coercion)
_                      -> NormaliseStepResult (Coercion, MCoercionN)
forall ev. NormaliseStepResult ev
NS_Done

---------------
normaliseTcApp :: FamInstEnvs -> Role -> TyCon -> [Type] -> (Coercion, Type)
-- See comments on normaliseType for the arguments of this function
normaliseTcApp :: (FamInstEnv, FamInstEnv)
-> Role -> TyCon -> [Type] -> (Coercion, Type)
normaliseTcApp (FamInstEnv, FamInstEnv)
env Role
role TyCon
tc [Type]
tys
  = (FamInstEnv, FamInstEnv)
-> Role -> VarSet -> NormM (Coercion, Type) -> (Coercion, Type)
forall a.
(FamInstEnv, FamInstEnv) -> Role -> VarSet -> NormM a -> a
initNormM (FamInstEnv, FamInstEnv)
env Role
role ([Type] -> VarSet
tyCoVarsOfTypes [Type]
tys) (NormM (Coercion, Type) -> (Coercion, Type))
-> NormM (Coercion, Type) -> (Coercion, Type)
forall a b. (a -> b) -> a -> b
$
    TyCon -> [Type] -> NormM (Coercion, Type)
normalise_tc_app TyCon
tc [Type]
tys

-- See Note [Normalising types] about the LiftingContext
normalise_tc_app :: TyCon -> [Type] -> NormM (Coercion, Type)
normalise_tc_app :: TyCon -> [Type] -> NormM (Coercion, Type)
normalise_tc_app TyCon
tc [Type]
tys
  | Just ([(TyVar, Type)]
tenv, Type
rhs, [Type]
tys') <- TyCon -> [Type] -> Maybe ([(TyVar, Type)], Type, [Type])
forall tyco.
TyCon -> [tyco] -> Maybe ([(TyVar, tyco)], Type, [tyco])
expandSynTyCon_maybe TyCon
tc [Type]
tys
  , Bool -> Bool
not (TyCon -> Bool
isFamFreeTyCon TyCon
tc)  -- Expand and try again
  = -- A synonym with type families in the RHS
    -- Expand and try again
    -- See Note [Normalisation and type synonyms]
    Type -> NormM (Coercion, Type)
normalise_type (Type -> [Type] -> Type
mkAppTys (HasCallStack => TCvSubst -> Type -> Type
TCvSubst -> Type -> Type
substTy ([(TyVar, Type)] -> TCvSubst
mkTvSubstPrs [(TyVar, Type)]
tenv) Type
rhs) [Type]
tys')

  | TyCon -> Bool
isFamilyTyCon TyCon
tc
  = -- A type-family application
    do { (FamInstEnv, FamInstEnv)
env <- NormM (FamInstEnv, FamInstEnv)
getEnv
       ; Role
role <- NormM Role
getRole
       ; (Coercion
args_co, [Type]
ntys, Coercion
res_co) <- TyCon -> [Type] -> NormM (Coercion, [Type], Coercion)
normalise_tc_args TyCon
tc [Type]
tys
       ; case (FamInstEnv, FamInstEnv)
-> Role -> TyCon -> [Type] -> Maybe (Coercion, Type)
reduceTyFamApp_maybe (FamInstEnv, FamInstEnv)
env Role
role TyCon
tc [Type]
ntys of
           Just (Coercion
first_co, Type
ty')
             -> do { (Coercion
rest_co,Type
nty) <- Type -> NormM (Coercion, Type)
normalise_type Type
ty'
                   ; (Coercion, Type) -> NormM (Coercion, Type)
forall (m :: * -> *) a. Monad m => a -> m a
return (Role -> Type -> Coercion -> Coercion -> (Coercion, Type)
assemble_result Role
role Type
nty
                                             (Coercion
args_co Coercion -> Coercion -> Coercion
`mkTransCo` Coercion
first_co Coercion -> Coercion -> Coercion
`mkTransCo` Coercion
rest_co)
                                             Coercion
res_co) }
           Maybe (Coercion, Type)
_ -> -- No unique matching family instance exists;
                -- we do not do anything
                (Coercion, Type) -> NormM (Coercion, Type)
forall (m :: * -> *) a. Monad m => a -> m a
return (Role -> Type -> Coercion -> Coercion -> (Coercion, Type)
assemble_result Role
role (TyCon -> [Type] -> Type
mkTyConApp TyCon
tc [Type]
ntys) Coercion
args_co Coercion
res_co) }

  | Bool
otherwise
  = -- A synonym with no type families in the RHS; or data type etc
    -- Just normalise the arguments and rebuild
    do { (Coercion
args_co, [Type]
ntys, Coercion
res_co) <- TyCon -> [Type] -> NormM (Coercion, [Type], Coercion)
normalise_tc_args TyCon
tc [Type]
tys
       ; Role
role <- NormM Role
getRole
       ; (Coercion, Type) -> NormM (Coercion, Type)
forall (m :: * -> *) a. Monad m => a -> m a
return (Role -> Type -> Coercion -> Coercion -> (Coercion, Type)
assemble_result Role
role (TyCon -> [Type] -> Type
mkTyConApp TyCon
tc [Type]
ntys) Coercion
args_co Coercion
res_co) }

  where
    assemble_result :: Role       -- r, ambient role in NormM monad
                    -> Type       -- nty, result type, possibly of changed kind
                    -> Coercion   -- orig_ty ~r nty, possibly heterogeneous
                    -> CoercionN  -- typeKind(orig_ty) ~N typeKind(nty)
                    -> (Coercion, Type)   -- (co :: orig_ty ~r nty_casted, nty_casted)
                                          -- where nty_casted has same kind as orig_ty
    assemble_result :: Role -> Type -> Coercion -> Coercion -> (Coercion, Type)
assemble_result Role
r Type
nty Coercion
orig_to_nty Coercion
kind_co
      = ( Coercion
final_co, Type
nty_old_kind )
      where
        nty_old_kind :: Type
nty_old_kind = Type
nty Type -> Coercion -> Type
`mkCastTy` Coercion -> Coercion
mkSymCo Coercion
kind_co
        final_co :: Coercion
final_co     = Role -> Type -> Coercion -> Coercion -> Coercion
mkCoherenceRightCo Role
r Type
nty (Coercion -> Coercion
mkSymCo Coercion
kind_co) Coercion
orig_to_nty

---------------
-- | Try to simplify a type-family application, by *one* step
-- If topReduceTyFamApp_maybe env r F tys = Just (co, rhs, res_co)
-- then    co     :: F tys ~R# rhs
--         res_co :: typeKind(F tys) ~ typeKind(rhs)
-- Type families and data families; always Representational role
topReduceTyFamApp_maybe :: FamInstEnvs -> TyCon -> [Type]
                        -> Maybe (Coercion, Type, Coercion)
topReduceTyFamApp_maybe :: (FamInstEnv, FamInstEnv)
-> TyCon -> [Type] -> Maybe (Coercion, Type, Coercion)
topReduceTyFamApp_maybe (FamInstEnv, FamInstEnv)
envs TyCon
fam_tc [Type]
arg_tys
  | TyCon -> Bool
isFamilyTyCon TyCon
fam_tc   -- type families and data families
  , Just (Coercion
co, Type
rhs) <- (FamInstEnv, FamInstEnv)
-> Role -> TyCon -> [Type] -> Maybe (Coercion, Type)
reduceTyFamApp_maybe (FamInstEnv, FamInstEnv)
envs Role
role TyCon
fam_tc [Type]
ntys
  = (Coercion, Type, Coercion) -> Maybe (Coercion, Type, Coercion)
forall a. a -> Maybe a
Just (Coercion
args_co Coercion -> Coercion -> Coercion
`mkTransCo` Coercion
co, Type
rhs, Coercion
res_co)
  | Bool
otherwise
  = Maybe (Coercion, Type, Coercion)
forall a. Maybe a
Nothing
  where
    role :: Role
role = Role
Representational
    (Coercion
args_co, [Type]
ntys, Coercion
res_co) = (FamInstEnv, FamInstEnv)
-> Role
-> VarSet
-> NormM (Coercion, [Type], Coercion)
-> (Coercion, [Type], Coercion)
forall a.
(FamInstEnv, FamInstEnv) -> Role -> VarSet -> NormM a -> a
initNormM (FamInstEnv, FamInstEnv)
envs Role
role ([Type] -> VarSet
tyCoVarsOfTypes [Type]
arg_tys) (NormM (Coercion, [Type], Coercion)
 -> (Coercion, [Type], Coercion))
-> NormM (Coercion, [Type], Coercion)
-> (Coercion, [Type], Coercion)
forall a b. (a -> b) -> a -> b
$
                              TyCon -> [Type] -> NormM (Coercion, [Type], Coercion)
normalise_tc_args TyCon
fam_tc [Type]
arg_tys

normalise_tc_args :: TyCon -> [Type]             -- tc tys
                  -> NormM (Coercion, [Type], CoercionN)
                  -- (co, new_tys), where
                  -- co :: tc tys ~ tc new_tys; might not be homogeneous
                  -- res_co :: typeKind(tc tys) ~N typeKind(tc new_tys)
normalise_tc_args :: TyCon -> [Type] -> NormM (Coercion, [Type], Coercion)
normalise_tc_args TyCon
tc [Type]
tys
  = do { Role
role <- NormM Role
getRole
       ; ([Coercion]
args_cos, [Type]
nargs, Coercion
res_co) <- Type -> [Role] -> [Type] -> NormM ([Coercion], [Type], Coercion)
normalise_args (TyCon -> Type
tyConKind TyCon
tc) (Role -> TyCon -> [Role]
tyConRolesX Role
role TyCon
tc) [Type]
tys
       ; (Coercion, [Type], Coercion) -> NormM (Coercion, [Type], Coercion)
forall (m :: * -> *) a. Monad m => a -> m a
return (HasDebugCallStack => Role -> TyCon -> [Coercion] -> Coercion
Role -> TyCon -> [Coercion] -> Coercion
mkTyConAppCo Role
role TyCon
tc [Coercion]
args_cos, [Type]
nargs, Coercion
res_co) }

---------------
normaliseType :: FamInstEnvs
              -> Role  -- desired role of coercion
              -> Type -> (Coercion, Type)
normaliseType :: (FamInstEnv, FamInstEnv) -> Role -> Type -> (Coercion, Type)
normaliseType (FamInstEnv, FamInstEnv)
env Role
role Type
ty
  = (FamInstEnv, FamInstEnv)
-> Role -> VarSet -> NormM (Coercion, Type) -> (Coercion, Type)
forall a.
(FamInstEnv, FamInstEnv) -> Role -> VarSet -> NormM a -> a
initNormM (FamInstEnv, FamInstEnv)
env Role
role (Type -> VarSet
tyCoVarsOfType Type
ty) (NormM (Coercion, Type) -> (Coercion, Type))
-> NormM (Coercion, Type) -> (Coercion, Type)
forall a b. (a -> b) -> a -> b
$ Type -> NormM (Coercion, Type)
normalise_type Type
ty

normalise_type :: Type                     -- old type
               -> NormM (Coercion, Type)   -- (coercion, new type), where
                                           -- co :: old-type ~ new_type
-- Normalise the input type, by eliminating *all* type-function redexes
-- but *not* newtypes (which are visible to the programmer)
-- Returns with Refl if nothing happens
-- Does nothing to newtypes
-- The returned coercion *must* be *homogeneous*
-- See Note [Normalising types]
-- Try not to disturb type synonyms if possible

normalise_type :: Type -> NormM (Coercion, Type)
normalise_type Type
ty
  = Type -> NormM (Coercion, Type)
go Type
ty
  where
    go :: Type -> NormM (Coercion, Type)
go (TyConApp TyCon
tc [Type]
tys) = TyCon -> [Type] -> NormM (Coercion, Type)
normalise_tc_app TyCon
tc [Type]
tys
    go ty :: Type
ty@(LitTy {})     = do { Role
r <- NormM Role
getRole
                              ; (Coercion, Type) -> NormM (Coercion, Type)
forall (m :: * -> *) a. Monad m => a -> m a
return (Role -> Type -> Coercion
mkReflCo Role
r Type
ty, Type
ty) }
    go (AppTy Type
ty1 Type
ty2) = Type -> [Type] -> NormM (Coercion, Type)
go_app_tys Type
ty1 [Type
ty2]

    go ty :: Type
ty@(FunTy { ft_mult :: Type -> Type
ft_mult = Type
w, ft_arg :: Type -> Type
ft_arg = Type
ty1, ft_res :: Type -> Type
ft_res = Type
ty2 })
      = do { (Coercion
co1, Type
nty1) <- Type -> NormM (Coercion, Type)
go Type
ty1
           ; (Coercion
co2, Type
nty2) <- Type -> NormM (Coercion, Type)
go Type
ty2
           ; (Coercion
wco, Type
wty) <- Role -> NormM (Coercion, Type) -> NormM (Coercion, Type)
forall a. Role -> NormM a -> NormM a
withRole Role
Nominal (NormM (Coercion, Type) -> NormM (Coercion, Type))
-> NormM (Coercion, Type) -> NormM (Coercion, Type)
forall a b. (a -> b) -> a -> b
$ Type -> NormM (Coercion, Type)
go Type
w
           ; Role
r <- NormM Role
getRole
           ; (Coercion, Type) -> NormM (Coercion, Type)
forall (m :: * -> *) a. Monad m => a -> m a
return (Role -> Coercion -> Coercion -> Coercion -> Coercion
mkFunCo Role
r Coercion
wco Coercion
co1 Coercion
co2, Type
ty { ft_mult :: Type
ft_mult = Type
wty, ft_arg :: Type
ft_arg = Type
nty1, ft_res :: Type
ft_res = Type
nty2 }) }
    go (ForAllTy (Bndr TyVar
tcvar ArgFlag
vis) Type
ty)
      = do { (LiftingContext
lc', TyVar
tv', Coercion
h, Type
ki') <- TyVar -> NormM (LiftingContext, TyVar, Coercion, Type)
normalise_var_bndr TyVar
tcvar
           ; (Coercion
co, Type
nty)          <- LiftingContext -> NormM (Coercion, Type) -> NormM (Coercion, Type)
forall a. LiftingContext -> NormM a -> NormM a
withLC LiftingContext
lc' (NormM (Coercion, Type) -> NormM (Coercion, Type))
-> NormM (Coercion, Type) -> NormM (Coercion, Type)
forall a b. (a -> b) -> a -> b
$ Type -> NormM (Coercion, Type)
normalise_type Type
ty
           ; let tv2 :: TyVar
tv2 = TyVar -> Type -> TyVar
setTyVarKind TyVar
tv' Type
ki'
           ; (Coercion, Type) -> NormM (Coercion, Type)
forall (m :: * -> *) a. Monad m => a -> m a
return (TyVar -> Coercion -> Coercion -> Coercion
mkForAllCo TyVar
tv' Coercion
h Coercion
co, VarBndr TyVar ArgFlag -> Type -> Type
ForAllTy (TyVar -> ArgFlag -> VarBndr TyVar ArgFlag
forall var argf. var -> argf -> VarBndr var argf
Bndr TyVar
tv2 ArgFlag
vis) Type
nty) }
    go (TyVarTy TyVar
tv)    = TyVar -> NormM (Coercion, Type)
normalise_tyvar TyVar
tv
    go (CastTy Type
ty Coercion
co)
      = do { (Coercion
nco, Type
nty) <- Type -> NormM (Coercion, Type)
go Type
ty
           ; LiftingContext
lc <- NormM LiftingContext
getLC
           ; let co' :: Coercion
co' = LiftingContext -> Coercion -> Coercion
substRightCo LiftingContext
lc Coercion
co
           ; (Coercion, Type) -> NormM (Coercion, Type)
forall (m :: * -> *) a. Monad m => a -> m a
return (Coercion
-> Role -> Type -> Type -> Coercion -> Coercion -> Coercion
castCoercionKind2 Coercion
nco Role
Nominal Type
ty Type
nty Coercion
co Coercion
co'
                    , Type -> Coercion -> Type
mkCastTy Type
nty Coercion
co') }
    go (CoercionTy Coercion
co)
      = do { LiftingContext
lc <- NormM LiftingContext
getLC
           ; Role
r <- NormM Role
getRole
           ; let right_co :: Coercion
right_co = LiftingContext -> Coercion -> Coercion
substRightCo LiftingContext
lc Coercion
co
           ; (Coercion, Type) -> NormM (Coercion, Type)
forall (m :: * -> *) a. Monad m => a -> m a
return ( Role -> Coercion -> Coercion -> Coercion -> Coercion
mkProofIrrelCo Role
r
                         (HasDebugCallStack => Role -> LiftingContext -> Type -> Coercion
Role -> LiftingContext -> Type -> Coercion
liftCoSubst Role
Nominal LiftingContext
lc (Coercion -> Type
coercionType Coercion
co))
                         Coercion
co Coercion
right_co
                    , Coercion -> Type
mkCoercionTy Coercion
right_co ) }

    go_app_tys :: Type   -- function
               -> [Type] -- args
               -> NormM (Coercion, Type)
    -- cf. GHC.Tc.Solver.Flatten.flatten_app_ty_args
    go_app_tys :: Type -> [Type] -> NormM (Coercion, Type)
go_app_tys (AppTy Type
ty1 Type
ty2) [Type]
tys = Type -> [Type] -> NormM (Coercion, Type)
go_app_tys Type
ty1 (Type
ty2 Type -> [Type] -> [Type]
forall a. a -> [a] -> [a]
: [Type]
tys)
    go_app_tys Type
fun_ty [Type]
arg_tys
      = do { (Coercion
fun_co, Type
nfun) <- Type -> NormM (Coercion, Type)
go Type
fun_ty
           ; case HasCallStack => Type -> Maybe (TyCon, [Type])
Type -> Maybe (TyCon, [Type])
tcSplitTyConApp_maybe Type
nfun of
               Just (TyCon
tc, [Type]
xis) ->
                 do { (Coercion
second_co, Type
nty) <- Type -> NormM (Coercion, Type)
go (TyCon -> [Type] -> Type
mkTyConApp TyCon
tc ([Type]
xis [Type] -> [Type] -> [Type]
forall a. [a] -> [a] -> [a]
++ [Type]
arg_tys))
                   -- flatten_app_ty_args avoids redundantly processing the xis,
                   -- but that's a much more performance-sensitive function.
                   -- This type normalisation is not called in a loop.
                    ; (Coercion, Type) -> NormM (Coercion, Type)
forall (m :: * -> *) a. Monad m => a -> m a
return (Coercion -> [Coercion] -> Coercion
mkAppCos Coercion
fun_co ((Type -> Coercion) -> [Type] -> [Coercion]
forall a b. (a -> b) -> [a] -> [b]
map Type -> Coercion
mkNomReflCo [Type]
arg_tys) Coercion -> Coercion -> Coercion
`mkTransCo` Coercion
second_co, Type
nty) }
               Maybe (TyCon, [Type])
Nothing ->
                 do { ([Coercion]
args_cos, [Type]
nargs, Coercion
res_co) <- Type -> [Role] -> [Type] -> NormM ([Coercion], [Type], Coercion)
normalise_args (HasDebugCallStack => Type -> Type
Type -> Type
typeKind Type
nfun)
                                                                  (Role -> [Role]
forall a. a -> [a]
repeat Role
Nominal)
                                                                  [Type]
arg_tys
                    ; Role
role <- NormM Role
getRole
                    ; let nty :: Type
nty = Type -> [Type] -> Type
mkAppTys Type
nfun [Type]
nargs
                          nco :: Coercion
nco = Coercion -> [Coercion] -> Coercion
mkAppCos Coercion
fun_co [Coercion]
args_cos
                          nty_casted :: Type
nty_casted = Type
nty Type -> Coercion -> Type
`mkCastTy` Coercion -> Coercion
mkSymCo Coercion
res_co
                          final_co :: Coercion
final_co = Role -> Type -> Coercion -> Coercion -> Coercion
mkCoherenceRightCo Role
role Type
nty (Coercion -> Coercion
mkSymCo Coercion
res_co) Coercion
nco
                    ; (Coercion, Type) -> NormM (Coercion, Type)
forall (m :: * -> *) a. Monad m => a -> m a
return (Coercion
final_co, Type
nty_casted) } }

normalise_args :: Kind    -- of the function
               -> [Role]  -- roles at which to normalise args
               -> [Type]  -- args
               -> NormM ([Coercion], [Type], Coercion)
-- returns (cos, xis, res_co), where each xi is the normalised
-- version of the corresponding type, each co is orig_arg ~ xi,
-- and the res_co :: kind(f orig_args) ~ kind(f xis)
-- NB: The xis might *not* have the same kinds as the input types,
-- but the resulting application *will* be well-kinded
-- cf. GHC.Tc.Solver.Flatten.flatten_args_slow
normalise_args :: Type -> [Role] -> [Type] -> NormM ([Coercion], [Type], Coercion)
normalise_args Type
fun_ki [Role]
roles [Type]
args
  = do { [(Type, Coercion)]
normed_args <- (Role -> Type -> NormM (Type, Coercion))
-> [Role] -> [Type] -> NormM [(Type, Coercion)]
forall (m :: * -> *) a b c.
Applicative m =>
(a -> b -> m c) -> [a] -> [b] -> m [c]
zipWithM Role -> Type -> NormM (Type, Coercion)
normalise1 [Role]
roles [Type]
args
       ; let ([Type]
xis, [Coercion]
cos, Coercion
res_co) = [TyCoBinder]
-> Type
-> VarSet
-> [Role]
-> [(Type, Coercion)]
-> ([Type], [Coercion], Coercion)
simplifyArgsWorker [TyCoBinder]
ki_binders Type
inner_ki VarSet
fvs [Role]
roles [(Type, Coercion)]
normed_args
       ; ([Coercion], [Type], Coercion)
-> NormM ([Coercion], [Type], Coercion)
forall (m :: * -> *) a. Monad m => a -> m a
return ((Coercion -> Coercion) -> [Coercion] -> [Coercion]
forall a b. (a -> b) -> [a] -> [b]
map Coercion -> Coercion
mkSymCo [Coercion]
cos, [Type]
xis, Coercion -> Coercion
mkSymCo Coercion
res_co) }
  where
    ([TyCoBinder]
ki_binders, Type
inner_ki) = Type -> ([TyCoBinder], Type)
splitPiTys Type
fun_ki
    fvs :: VarSet
fvs = [Type] -> VarSet
tyCoVarsOfTypes [Type]
args

    -- flattener conventions are different from ours
    impedance_match :: NormM (Coercion, Type) -> NormM (Type, Coercion)
    impedance_match :: NormM (Coercion, Type) -> NormM (Type, Coercion)
impedance_match NormM (Coercion, Type)
action = do { (Coercion
co, Type
ty) <- NormM (Coercion, Type)
action
                                ; (Type, Coercion) -> NormM (Type, Coercion)
forall (m :: * -> *) a. Monad m => a -> m a
return (Type
ty, Coercion -> Coercion
mkSymCo Coercion
co) }

    normalise1 :: Role -> Type -> NormM (Type, Coercion)
normalise1 Role
role Type
ty
      = NormM (Coercion, Type) -> NormM (Type, Coercion)
impedance_match (NormM (Coercion, Type) -> NormM (Type, Coercion))
-> NormM (Coercion, Type) -> NormM (Type, Coercion)
forall a b. (a -> b) -> a -> b
$ Role -> NormM (Coercion, Type) -> NormM (Coercion, Type)
forall a. Role -> NormM a -> NormM a
withRole Role
role (NormM (Coercion, Type) -> NormM (Coercion, Type))
-> NormM (Coercion, Type) -> NormM (Coercion, Type)
forall a b. (a -> b) -> a -> b
$ Type -> NormM (Coercion, Type)
normalise_type Type
ty

normalise_tyvar :: TyVar -> NormM (Coercion, Type)
normalise_tyvar :: TyVar -> NormM (Coercion, Type)
normalise_tyvar TyVar
tv
  = ASSERT( isTyVar tv )
    do { LiftingContext
lc <- NormM LiftingContext
getLC
       ; Role
r  <- NormM Role
getRole
       ; (Coercion, Type) -> NormM (Coercion, Type)
forall (m :: * -> *) a. Monad m => a -> m a
return ((Coercion, Type) -> NormM (Coercion, Type))
-> (Coercion, Type) -> NormM (Coercion, Type)
forall a b. (a -> b) -> a -> b
$ case LiftingContext -> Role -> TyVar -> Maybe Coercion
liftCoSubstTyVar LiftingContext
lc Role
r TyVar
tv of
           Just Coercion
co -> (Coercion
co, Coercion -> Type
coercionRKind Coercion
co)
           Maybe Coercion
Nothing -> (Role -> Type -> Coercion
mkReflCo Role
r Type
ty, Type
ty) }
  where ty :: Type
ty = TyVar -> Type
mkTyVarTy TyVar
tv

normalise_var_bndr :: TyCoVar -> NormM (LiftingContext, TyCoVar, Coercion, Kind)
normalise_var_bndr :: TyVar -> NormM (LiftingContext, TyVar, Coercion, Type)
normalise_var_bndr TyVar
tcvar
  -- works for both tvar and covar
  = do { LiftingContext
lc1 <- NormM LiftingContext
getLC
       ; (FamInstEnv, FamInstEnv)
env <- NormM (FamInstEnv, FamInstEnv)
getEnv
       ; let callback :: LiftingContext -> Type -> (Coercion, Type)
callback LiftingContext
lc Type
ki = NormM (Coercion, Type)
-> (FamInstEnv, FamInstEnv)
-> LiftingContext
-> Role
-> (Coercion, Type)
forall a.
NormM a -> (FamInstEnv, FamInstEnv) -> LiftingContext -> Role -> a
runNormM (Type -> NormM (Coercion, Type)
normalise_type Type
ki) (FamInstEnv, FamInstEnv)
env LiftingContext
lc Role
Nominal
       ; (LiftingContext, TyVar, Coercion, Type)
-> NormM (LiftingContext, TyVar, Coercion, Type)
forall (m :: * -> *) a. Monad m => a -> m a
return ((LiftingContext, TyVar, Coercion, Type)
 -> NormM (LiftingContext, TyVar, Coercion, Type))
-> (LiftingContext, TyVar, Coercion, Type)
-> NormM (LiftingContext, TyVar, Coercion, Type)
forall a b. (a -> b) -> a -> b
$ (LiftingContext -> Type -> (Coercion, Type))
-> LiftingContext
-> TyVar
-> (LiftingContext, TyVar, Coercion, Type)
forall a.
(LiftingContext -> Type -> (Coercion, a))
-> LiftingContext -> TyVar -> (LiftingContext, TyVar, Coercion, a)
liftCoSubstVarBndrUsing LiftingContext -> Type -> (Coercion, Type)
callback LiftingContext
lc1 TyVar
tcvar }

-- | a monad for the normalisation functions, reading 'FamInstEnvs',
-- a 'LiftingContext', and a 'Role'.
newtype NormM a = NormM { forall a.
NormM a -> (FamInstEnv, FamInstEnv) -> LiftingContext -> Role -> a
runNormM ::
                            FamInstEnvs -> LiftingContext -> Role -> a }
    deriving ((forall a b. (a -> b) -> NormM a -> NormM b)
-> (forall a b. a -> NormM b -> NormM a) -> Functor NormM
forall a b. a -> NormM b -> NormM a
forall a b. (a -> b) -> NormM a -> NormM b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
<$ :: forall a b. a -> NormM b -> NormM a
$c<$ :: forall a b. a -> NormM b -> NormM a
fmap :: forall a b. (a -> b) -> NormM a -> NormM b
$cfmap :: forall a b. (a -> b) -> NormM a -> NormM b
Functor)

initNormM :: FamInstEnvs -> Role
          -> TyCoVarSet   -- the in-scope variables
          -> NormM a -> a
initNormM :: forall a.
(FamInstEnv, FamInstEnv) -> Role -> VarSet -> NormM a -> a
initNormM (FamInstEnv, FamInstEnv)
env Role
role VarSet
vars (NormM (FamInstEnv, FamInstEnv) -> LiftingContext -> Role -> a
thing_inside)
  = (FamInstEnv, FamInstEnv) -> LiftingContext -> Role -> a
thing_inside (FamInstEnv, FamInstEnv)
env LiftingContext
lc Role
role
  where
    in_scope :: InScopeSet
in_scope = VarSet -> InScopeSet
mkInScopeSet VarSet
vars
    lc :: LiftingContext
lc       = InScopeSet -> LiftingContext
emptyLiftingContext InScopeSet
in_scope

getRole :: NormM Role
getRole :: NormM Role
getRole = ((FamInstEnv, FamInstEnv) -> LiftingContext -> Role -> Role)
-> NormM Role
forall a.
((FamInstEnv, FamInstEnv) -> LiftingContext -> Role -> a)
-> NormM a
NormM (\ (FamInstEnv, FamInstEnv)
_ LiftingContext
_ Role
r -> Role
r)

getLC :: NormM LiftingContext
getLC :: NormM LiftingContext
getLC = ((FamInstEnv, FamInstEnv)
 -> LiftingContext -> Role -> LiftingContext)
-> NormM LiftingContext
forall a.
((FamInstEnv, FamInstEnv) -> LiftingContext -> Role -> a)
-> NormM a
NormM (\ (FamInstEnv, FamInstEnv)
_ LiftingContext
lc Role
_ -> LiftingContext
lc)

getEnv :: NormM FamInstEnvs
getEnv :: NormM (FamInstEnv, FamInstEnv)
getEnv = ((FamInstEnv, FamInstEnv)
 -> LiftingContext -> Role -> (FamInstEnv, FamInstEnv))
-> NormM (FamInstEnv, FamInstEnv)
forall a.
((FamInstEnv, FamInstEnv) -> LiftingContext -> Role -> a)
-> NormM a
NormM (\ (FamInstEnv, FamInstEnv)
env LiftingContext
_ Role
_ -> (FamInstEnv, FamInstEnv)
env)

withRole :: Role -> NormM a -> NormM a
withRole :: forall a. Role -> NormM a -> NormM a
withRole Role
r NormM a
thing = ((FamInstEnv, FamInstEnv) -> LiftingContext -> Role -> a)
-> NormM a
forall a.
((FamInstEnv, FamInstEnv) -> LiftingContext -> Role -> a)
-> NormM a
NormM (((FamInstEnv, FamInstEnv) -> LiftingContext -> Role -> a)
 -> NormM a)
-> ((FamInstEnv, FamInstEnv) -> LiftingContext -> Role -> a)
-> NormM a
forall a b. (a -> b) -> a -> b
$ \ (FamInstEnv, FamInstEnv)
envs LiftingContext
lc Role
_old_r -> NormM a -> (FamInstEnv, FamInstEnv) -> LiftingContext -> Role -> a
forall a.
NormM a -> (FamInstEnv, FamInstEnv) -> LiftingContext -> Role -> a
runNormM NormM a
thing (FamInstEnv, FamInstEnv)
envs LiftingContext
lc Role
r

withLC :: LiftingContext -> NormM a -> NormM a
withLC :: forall a. LiftingContext -> NormM a -> NormM a
withLC LiftingContext
lc NormM a
thing = ((FamInstEnv, FamInstEnv) -> LiftingContext -> Role -> a)
-> NormM a
forall a.
((FamInstEnv, FamInstEnv) -> LiftingContext -> Role -> a)
-> NormM a
NormM (((FamInstEnv, FamInstEnv) -> LiftingContext -> Role -> a)
 -> NormM a)
-> ((FamInstEnv, FamInstEnv) -> LiftingContext -> Role -> a)
-> NormM a
forall a b. (a -> b) -> a -> b
$ \ (FamInstEnv, FamInstEnv)
envs LiftingContext
_old_lc Role
r -> NormM a -> (FamInstEnv, FamInstEnv) -> LiftingContext -> Role -> a
forall a.
NormM a -> (FamInstEnv, FamInstEnv) -> LiftingContext -> Role -> a
runNormM NormM a
thing (FamInstEnv, FamInstEnv)
envs LiftingContext
lc Role
r

instance Monad NormM where
  NormM a
ma >>= :: forall a b. NormM a -> (a -> NormM b) -> NormM b
>>= a -> NormM b
fmb = ((FamInstEnv, FamInstEnv) -> LiftingContext -> Role -> b)
-> NormM b
forall a.
((FamInstEnv, FamInstEnv) -> LiftingContext -> Role -> a)
-> NormM a
NormM (((FamInstEnv, FamInstEnv) -> LiftingContext -> Role -> b)
 -> NormM b)
-> ((FamInstEnv, FamInstEnv) -> LiftingContext -> Role -> b)
-> NormM b
forall a b. (a -> b) -> a -> b
$ \(FamInstEnv, FamInstEnv)
env LiftingContext
lc Role
r ->
               let a :: a
a = NormM a -> (FamInstEnv, FamInstEnv) -> LiftingContext -> Role -> a
forall a.
NormM a -> (FamInstEnv, FamInstEnv) -> LiftingContext -> Role -> a
runNormM NormM a
ma (FamInstEnv, FamInstEnv)
env LiftingContext
lc Role
r in
               NormM b -> (FamInstEnv, FamInstEnv) -> LiftingContext -> Role -> b
forall a.
NormM a -> (FamInstEnv, FamInstEnv) -> LiftingContext -> Role -> a
runNormM (a -> NormM b
fmb a
a) (FamInstEnv, FamInstEnv)
env LiftingContext
lc Role
r

instance Applicative NormM where
  pure :: forall a. a -> NormM a
pure a
x = ((FamInstEnv, FamInstEnv) -> LiftingContext -> Role -> a)
-> NormM a
forall a.
((FamInstEnv, FamInstEnv) -> LiftingContext -> Role -> a)
-> NormM a
NormM (((FamInstEnv, FamInstEnv) -> LiftingContext -> Role -> a)
 -> NormM a)
-> ((FamInstEnv, FamInstEnv) -> LiftingContext -> Role -> a)
-> NormM a
forall a b. (a -> b) -> a -> b
$ \ (FamInstEnv, FamInstEnv)
_ LiftingContext
_ Role
_ -> a
x
  <*> :: forall a b. NormM (a -> b) -> NormM a -> NormM b
(<*>)  = NormM (a -> b) -> NormM a -> NormM b
forall (m :: * -> *) a b. Monad m => m (a -> b) -> m a -> m b
ap

{-
************************************************************************
*                                                                      *
              Flattening
*                                                                      *
************************************************************************

Note [Flattening]
~~~~~~~~~~~~~~~~~
As described in "Closed type families with overlapping equations"
http://research.microsoft.com/en-us/um/people/simonpj/papers/ext-f/axioms-extended.pdf
we need to flatten core types before unifying them, when checking for "surely-apart"
against earlier equations of a closed type family.
Flattening means replacing all top-level uses of type functions with
fresh variables, *taking care to preserve sharing*. That is, the type
(Either (F a b) (F a b)) should flatten to (Either c c), never (Either
c d).

Here is a nice example of why it's all necessary:

  type family F a b where
    F Int Bool = Char
    F a   b    = Double
  type family G a         -- open, no instances

How do we reduce (F (G Float) (G Float))? The first equation clearly doesn't match,
while the second equation does. But, before reducing, we must make sure that the
target can never become (F Int Bool). Well, no matter what G Float becomes, it
certainly won't become *both* Int and Bool, so indeed we're safe reducing
(F (G Float) (G Float)) to Double.

This is necessary not only to get more reductions (which we might be
willing to give up on), but for substitutivity. If we have (F x x), we
can see that (F x x) can reduce to Double. So, it had better be the
case that (F blah blah) can reduce to Double, no matter what (blah)
is!  Flattening as done below ensures this.

The algorithm works by building up a TypeMap TyVar, mapping
type family applications to fresh variables. This mapping must
be threaded through all the function calls, as any entry in
the mapping must be propagated to all future nodes in the tree.

The algorithm also must track the set of in-scope variables, in
order to make fresh variables as it flattens. (We are far from a
source of fresh Uniques.) See Wrinkle 2, below.

There are wrinkles, of course:

1. The flattening algorithm must account for the possibility
   of inner `forall`s. (A `forall` seen here can happen only
   because of impredicativity. However, the flattening operation
   is an algorithm in Core, which is impredicative.)
   Suppose we have (forall b. F b) -> (forall b. F b). Of course,
   those two bs are entirely unrelated, and so we should certainly
   not flatten the two calls F b to the same variable. Instead, they
   must be treated separately. We thus carry a substitution that
   freshens variables; we must apply this substitution (in
   `coreFlattenTyFamApp`) before looking up an application in the environment.
   Note that the range of the substitution contains only TyVars, never anything
   else.

   For the sake of efficiency, we only apply this substitution when absolutely
   necessary. Namely:

   * We do not perform the substitution at all if it is empty.
   * We only need to worry about the arguments of a type family that are within
     the arity of said type family, so we can get away with not applying the
     substitution to any oversaturated type family arguments.
   * Importantly, we do /not/ achieve this substitution by recursively
     flattening the arguments, as this would be wrong. Consider `F (G a)`,
     where F and G are type families. We might decide that `F (G a)` flattens
     to `beta`. Later, the substitution is non-empty (but does not map `a`) and
     so we flatten `G a` to `gamma` and try to flatten `F gamma`. Of course,
     `F gamma` is unknown, and so we flatten it to `delta`, but it really
     should have been `beta`! Argh!

     Moral of the story: instead of flattening the arguments, just substitute
     them directly.

2. There are two different reasons we might add a variable
   to the in-scope set as we work:

     A. We have just invented a new flattening variable.
     B. We have entered a `forall`.

   Annoying here is that in-scope variable source (A) must be
   threaded through the calls. For example, consider (F b -> forall c. F c).
   Suppose that, when flattening F b, we invent a fresh variable c.
   Now, when we encounter (forall c. F c), we need to know c is already in
   scope so that we locally rename c to c'. However, if we don't thread through
   the in-scope set from one argument of (->) to the other, we won't know this
   and might get very confused.

   In contrast, source (B) increases only as we go deeper, as in-scope sets
   normally do. However, even here we must be careful. The TypeMap TyVar that
   contains mappings from type family applications to freshened variables will
   be threaded through both sides of (forall b. F b) -> (forall b. F b). We
   thus must make sure that the two `b`s don't get renamed to the same b1. (If
   they did, then looking up `F b1` would yield the same flatten var for
   each.) So, even though `forall`-bound variables should really be in the
   in-scope set only when they are in scope, we retain these variables even
   outside of their scope. This ensures that, if we encounter a fresh
   `forall`-bound b, we will rename it to b2, not b1. Note that keeping a
   larger in-scope set than strictly necessary is always OK, as in-scope sets
   are only ever used to avoid collisions.

   Sadly, the freshening substitution described in (1) really mustn't bind
   variables outside of their scope: note that its domain is the *unrenamed*
   variables. This means that the substitution gets "pushed down" (like a
   reader monad) while the in-scope set gets threaded (like a state monad).
   Because a TCvSubst contains its own in-scope set, we don't carry a TCvSubst;
   instead, we just carry a TvSubstEnv down, tying it to the InScopeSet
   traveling separately as necessary.

3. Consider `F ty_1 ... ty_n`, where F is a type family with arity k:

     type family F ty_1 ... ty_k :: res_k

   It's tempting to just flatten `F ty_1 ... ty_n` to `alpha`, where alpha is a
   flattening skolem. But we must instead flatten it to
   `alpha ty_(k+1) ... ty_n`—that is, by only flattening up to the arity of the
   type family.

   Why is this better? Consider the following concrete example from #16995:

     type family Param :: Type -> Type

     type family LookupParam (a :: Type) :: Type where
       LookupParam (f Char) = Bool
       LookupParam x        = Int

     foo :: LookupParam (Param ())
     foo = 42

   In order for `foo` to typecheck, `LookupParam (Param ())` must reduce to
   `Int`. But if we flatten `Param ()` to `alpha`, then GHC can't be sure if
   `alpha` is apart from `f Char`, so it won't fall through to the second
   equation. But since the `Param` type family has arity 0, we can instead
   flatten `Param ()` to `alpha ()`, about which GHC knows with confidence is
   apart from `f Char`, permitting the second equation to be reached.

   Not only does this allow more programs to be accepted, it's also important
   for correctness. Not doing this was the root cause of the Core Lint error
   in #16995.

flattenTys is defined here because of module dependencies.
-}

data FlattenEnv
  = FlattenEnv { FlattenEnv -> TypeMap TyVar
fe_type_map :: TypeMap TyVar
                 -- domain: exactly-saturated type family applications
                 -- range: fresh variables
               , FlattenEnv -> InScopeSet
fe_in_scope :: InScopeSet }
                 -- See Note [Flattening]

emptyFlattenEnv :: InScopeSet -> FlattenEnv
emptyFlattenEnv :: InScopeSet -> FlattenEnv
emptyFlattenEnv InScopeSet
in_scope
  = FlattenEnv :: TypeMap TyVar -> InScopeSet -> FlattenEnv
FlattenEnv { fe_type_map :: TypeMap TyVar
fe_type_map = TypeMap TyVar
forall a. TypeMap a
emptyTypeMap
               , fe_in_scope :: InScopeSet
fe_in_scope = InScopeSet
in_scope }

updateInScopeSet :: FlattenEnv -> (InScopeSet -> InScopeSet) -> FlattenEnv
updateInScopeSet :: FlattenEnv -> (InScopeSet -> InScopeSet) -> FlattenEnv
updateInScopeSet FlattenEnv
env InScopeSet -> InScopeSet
upd = FlattenEnv
env { fe_in_scope :: InScopeSet
fe_in_scope = InScopeSet -> InScopeSet
upd (FlattenEnv -> InScopeSet
fe_in_scope FlattenEnv
env) }

flattenTys :: InScopeSet -> [Type] -> [Type]
-- See Note [Flattening]
-- NB: the returned types may mention fresh type variables,
--     arising from the flattening.  We don't return the
--     mapping from those fresh vars to the ty-fam
--     applications they stand for (we could, but no need)
flattenTys :: InScopeSet -> [Type] -> [Type]
flattenTys InScopeSet
in_scope [Type]
tys
  = (FlattenEnv, [Type]) -> [Type]
forall a b. (a, b) -> b
snd ((FlattenEnv, [Type]) -> [Type]) -> (FlattenEnv, [Type]) -> [Type]
forall a b. (a -> b) -> a -> b
$ TvSubstEnv -> FlattenEnv -> [Type] -> (FlattenEnv, [Type])
coreFlattenTys TvSubstEnv
emptyTvSubstEnv (InScopeSet -> FlattenEnv
emptyFlattenEnv InScopeSet
in_scope) [Type]
tys

coreFlattenTys :: TvSubstEnv -> FlattenEnv
               -> [Type] -> (FlattenEnv, [Type])
coreFlattenTys :: TvSubstEnv -> FlattenEnv -> [Type] -> (FlattenEnv, [Type])
coreFlattenTys TvSubstEnv
subst = (FlattenEnv -> Type -> (FlattenEnv, Type))
-> FlattenEnv -> [Type] -> (FlattenEnv, [Type])
forall (t :: * -> *) s a b.
Traversable t =>
(s -> a -> (s, b)) -> s -> t a -> (s, t b)
mapAccumL (TvSubstEnv -> FlattenEnv -> Type -> (FlattenEnv, Type)
coreFlattenTy TvSubstEnv
subst)

coreFlattenTy :: TvSubstEnv -> FlattenEnv
              -> Type -> (FlattenEnv, Type)
coreFlattenTy :: TvSubstEnv -> FlattenEnv -> Type -> (FlattenEnv, Type)
coreFlattenTy TvSubstEnv
subst = FlattenEnv -> Type -> (FlattenEnv, Type)
go
  where
    go :: FlattenEnv -> Type -> (FlattenEnv, Type)
go FlattenEnv
env Type
ty | Just Type
ty' <- Type -> Maybe Type
coreView Type
ty = FlattenEnv -> Type -> (FlattenEnv, Type)
go FlattenEnv
env Type
ty'

    go FlattenEnv
env (TyVarTy TyVar
tv)
      | Just Type
ty <- TvSubstEnv -> TyVar -> Maybe Type
forall a. VarEnv a -> TyVar -> Maybe a
lookupVarEnv TvSubstEnv
subst TyVar
tv = (FlattenEnv
env, Type
ty)
      | Bool
otherwise                        = let (FlattenEnv
env', Type
ki) = FlattenEnv -> Type -> (FlattenEnv, Type)
go FlattenEnv
env (TyVar -> Type
tyVarKind TyVar
tv) in
                                           (FlattenEnv
env', TyVar -> Type
mkTyVarTy (TyVar -> Type) -> TyVar -> Type
forall a b. (a -> b) -> a -> b
$ TyVar -> Type -> TyVar
setTyVarKind TyVar
tv Type
ki)
    go FlattenEnv
env (AppTy Type
ty1 Type
ty2) = let (FlattenEnv
env1, Type
ty1') = FlattenEnv -> Type -> (FlattenEnv, Type)
go FlattenEnv
env  Type
ty1
                                 (FlattenEnv
env2, Type
ty2') = FlattenEnv -> Type -> (FlattenEnv, Type)
go FlattenEnv
env1 Type
ty2 in
                             (FlattenEnv
env2, Type -> Type -> Type
AppTy Type
ty1' Type
ty2')
    go FlattenEnv
env (TyConApp TyCon
tc [Type]
tys)
         -- NB: Don't just check if isFamilyTyCon: this catches *data* families,
         -- which are generative and thus can be preserved during flattening
      | Bool -> Bool
not (TyCon -> Role -> Bool
isGenerativeTyCon TyCon
tc Role
Nominal)
      = TvSubstEnv -> FlattenEnv -> TyCon -> [Type] -> (FlattenEnv, Type)
coreFlattenTyFamApp TvSubstEnv
subst FlattenEnv
env TyCon
tc [Type]
tys

      | Bool
otherwise
      = let (FlattenEnv
env', [Type]
tys') = TvSubstEnv -> FlattenEnv -> [Type] -> (FlattenEnv, [Type])
coreFlattenTys TvSubstEnv
subst FlattenEnv
env [Type]
tys in
        (FlattenEnv
env', TyCon -> [Type] -> Type
mkTyConApp TyCon
tc [Type]
tys')

    go FlattenEnv
env ty :: Type
ty@(FunTy { ft_mult :: Type -> Type
ft_mult = Type
mult, ft_arg :: Type -> Type
ft_arg = Type
ty1, ft_res :: Type -> Type
ft_res = Type
ty2 })
      = let (FlattenEnv
env1, Type
ty1') = FlattenEnv -> Type -> (FlattenEnv, Type)
go FlattenEnv
env  Type
ty1
            (FlattenEnv
env2, Type
ty2') = FlattenEnv -> Type -> (FlattenEnv, Type)
go FlattenEnv
env1 Type
ty2
            (FlattenEnv
env3, Type
mult') = FlattenEnv -> Type -> (FlattenEnv, Type)
go FlattenEnv
env2 Type
mult in
        (FlattenEnv
env3, Type
ty { ft_mult :: Type
ft_mult = Type
mult', ft_arg :: Type
ft_arg = Type
ty1', ft_res :: Type
ft_res = Type
ty2' })

    go FlattenEnv
env (ForAllTy (Bndr TyVar
tv ArgFlag
vis) Type
ty)
      = let (FlattenEnv
env1, TvSubstEnv
subst', TyVar
tv') = TvSubstEnv
-> FlattenEnv -> TyVar -> (FlattenEnv, TvSubstEnv, TyVar)
coreFlattenVarBndr TvSubstEnv
subst FlattenEnv
env TyVar
tv
            (FlattenEnv
env2, Type
ty') = TvSubstEnv -> FlattenEnv -> Type -> (FlattenEnv, Type)
coreFlattenTy TvSubstEnv
subst' FlattenEnv
env1 Type
ty in
        (FlattenEnv
env2, VarBndr TyVar ArgFlag -> Type -> Type
ForAllTy (TyVar -> ArgFlag -> VarBndr TyVar ArgFlag
forall var argf. var -> argf -> VarBndr var argf
Bndr TyVar
tv' ArgFlag
vis) Type
ty')

    go FlattenEnv
env ty :: Type
ty@(LitTy {}) = (FlattenEnv
env, Type
ty)

    go FlattenEnv
env (CastTy Type
ty Coercion
co)
      = let (FlattenEnv
env1, Type
ty') = FlattenEnv -> Type -> (FlattenEnv, Type)
go FlattenEnv
env Type
ty
            (FlattenEnv
env2, Coercion
co') = TvSubstEnv -> FlattenEnv -> Coercion -> (FlattenEnv, Coercion)
coreFlattenCo TvSubstEnv
subst FlattenEnv
env1 Coercion
co in
        (FlattenEnv
env2, Type -> Coercion -> Type
CastTy Type
ty' Coercion
co')

    go FlattenEnv
env (CoercionTy Coercion
co)
      = let (FlattenEnv
env', Coercion
co') = TvSubstEnv -> FlattenEnv -> Coercion -> (FlattenEnv, Coercion)
coreFlattenCo TvSubstEnv
subst FlattenEnv
env Coercion
co in
        (FlattenEnv
env', Coercion -> Type
CoercionTy Coercion
co')


-- when flattening, we don't care about the contents of coercions.
-- so, just return a fresh variable of the right (flattened) type
coreFlattenCo :: TvSubstEnv -> FlattenEnv
              -> Coercion -> (FlattenEnv, Coercion)
coreFlattenCo :: TvSubstEnv -> FlattenEnv -> Coercion -> (FlattenEnv, Coercion)
coreFlattenCo TvSubstEnv
subst FlattenEnv
env Coercion
co
  = (FlattenEnv
env2, TyVar -> Coercion
mkCoVarCo TyVar
covar)
  where
    (FlattenEnv
env1, Type
kind') = TvSubstEnv -> FlattenEnv -> Type -> (FlattenEnv, Type)
coreFlattenTy TvSubstEnv
subst FlattenEnv
env (Coercion -> Type
coercionType Coercion
co)
    covar :: TyVar
covar         = InScopeSet -> Type -> TyVar
mkFlattenFreshCoVar (FlattenEnv -> InScopeSet
fe_in_scope FlattenEnv
env1) Type
kind'
    -- Add the covar to the FlattenEnv's in-scope set.
    -- See Note [Flattening], wrinkle 2A.
    env2 :: FlattenEnv
env2          = FlattenEnv -> (InScopeSet -> InScopeSet) -> FlattenEnv
updateInScopeSet FlattenEnv
env1 ((InScopeSet -> TyVar -> InScopeSet)
-> TyVar -> InScopeSet -> InScopeSet
forall a b c. (a -> b -> c) -> b -> a -> c
flip InScopeSet -> TyVar -> InScopeSet
extendInScopeSet TyVar
covar)

coreFlattenVarBndr :: TvSubstEnv -> FlattenEnv
                   -> TyCoVar -> (FlattenEnv, TvSubstEnv, TyVar)
coreFlattenVarBndr :: TvSubstEnv
-> FlattenEnv -> TyVar -> (FlattenEnv, TvSubstEnv, TyVar)
coreFlattenVarBndr TvSubstEnv
subst FlattenEnv
env TyVar
tv
  = (FlattenEnv
env2, TvSubstEnv
subst', TyVar
tv')
  where
    -- See Note [Flattening], wrinkle 2B.
    kind :: Type
kind          = TyVar -> Type
varType TyVar
tv
    (FlattenEnv
env1, Type
kind') = TvSubstEnv -> FlattenEnv -> Type -> (FlattenEnv, Type)
coreFlattenTy TvSubstEnv
subst FlattenEnv
env Type
kind
    tv' :: TyVar
tv'           = InScopeSet -> TyVar -> TyVar
uniqAway (FlattenEnv -> InScopeSet
fe_in_scope FlattenEnv
env1) (TyVar -> Type -> TyVar
setVarType TyVar
tv Type
kind')
    subst' :: TvSubstEnv
subst'        = TvSubstEnv -> TyVar -> Type -> TvSubstEnv
forall a. VarEnv a -> TyVar -> a -> VarEnv a
extendVarEnv TvSubstEnv
subst TyVar
tv (TyVar -> Type
mkTyVarTy TyVar
tv')
    env2 :: FlattenEnv
env2          = FlattenEnv -> (InScopeSet -> InScopeSet) -> FlattenEnv
updateInScopeSet FlattenEnv
env1 ((InScopeSet -> TyVar -> InScopeSet)
-> TyVar -> InScopeSet -> InScopeSet
forall a b c. (a -> b -> c) -> b -> a -> c
flip InScopeSet -> TyVar -> InScopeSet
extendInScopeSet TyVar
tv')

coreFlattenTyFamApp :: TvSubstEnv -> FlattenEnv
                    -> TyCon         -- type family tycon
                    -> [Type]        -- args, already flattened
                    -> (FlattenEnv, Type)
coreFlattenTyFamApp :: TvSubstEnv -> FlattenEnv -> TyCon -> [Type] -> (FlattenEnv, Type)
coreFlattenTyFamApp TvSubstEnv
tv_subst FlattenEnv
env TyCon
fam_tc [Type]
fam_args
  = case TypeMap TyVar -> Type -> Maybe TyVar
forall a. TypeMap a -> Type -> Maybe a
lookupTypeMap TypeMap TyVar
type_map Type
fam_ty of
      Just TyVar
tv -> (FlattenEnv
env', Type -> [Type] -> Type
mkAppTys (TyVar -> Type
mkTyVarTy TyVar
tv) [Type]
leftover_args')
      Maybe TyVar
Nothing -> let tyvar_name :: Name
tyvar_name = TyCon -> Name
forall a. Uniquable a => a -> Name
mkFlattenFreshTyName TyCon
fam_tc
                     tv :: TyVar
tv         = InScopeSet -> TyVar -> TyVar
uniqAway InScopeSet
in_scope (TyVar -> TyVar) -> TyVar -> TyVar
forall a b. (a -> b) -> a -> b
$
                                  Name -> Type -> TyVar
mkTyVar Name
tyvar_name (HasDebugCallStack => Type -> Type
Type -> Type
typeKind Type
fam_ty)

                     ty' :: Type
ty'   = Type -> [Type] -> Type
mkAppTys (TyVar -> Type
mkTyVarTy TyVar
tv) [Type]
leftover_args'
                     env'' :: FlattenEnv
env'' = FlattenEnv
env' { fe_type_map :: TypeMap TyVar
fe_type_map = TypeMap TyVar -> Type -> TyVar -> TypeMap TyVar
forall a. TypeMap a -> Type -> a -> TypeMap a
extendTypeMap TypeMap TyVar
type_map Type
fam_ty TyVar
tv
                                  , fe_in_scope :: InScopeSet
fe_in_scope = InScopeSet -> TyVar -> InScopeSet
extendInScopeSet InScopeSet
in_scope TyVar
tv }
                 in (FlattenEnv
env'', Type
ty')
  where
    arity :: Arity
arity = TyCon -> Arity
tyConArity TyCon
fam_tc
    tcv_subst :: TCvSubst
tcv_subst = InScopeSet -> TvSubstEnv -> CvSubstEnv -> TCvSubst
TCvSubst (FlattenEnv -> InScopeSet
fe_in_scope FlattenEnv
env) TvSubstEnv
tv_subst CvSubstEnv
forall a. VarEnv a
emptyVarEnv
    ([Type]
sat_fam_args, [Type]
leftover_args) = ASSERT( arity <= length fam_args )
                                    Arity -> [Type] -> ([Type], [Type])
forall a. Arity -> [a] -> ([a], [a])
splitAt Arity
arity [Type]
fam_args
    -- Apply the substitution before looking up an application in the
    -- environment. See Note [Flattening], wrinkle 1.
    -- NB: substTys short-cuts the common case when the substitution is empty.
    sat_fam_args' :: [Type]
sat_fam_args' = HasCallStack => TCvSubst -> [Type] -> [Type]
TCvSubst -> [Type] -> [Type]
substTys TCvSubst
tcv_subst [Type]
sat_fam_args
    (FlattenEnv
env', [Type]
leftover_args') = TvSubstEnv -> FlattenEnv -> [Type] -> (FlattenEnv, [Type])
coreFlattenTys TvSubstEnv
tv_subst FlattenEnv
env [Type]
leftover_args
    -- `fam_tc` may be over-applied to `fam_args` (see Note [Flattening],
    -- wrinkle 3), so we split it into the arguments needed to saturate it
    -- (sat_fam_args') and the rest (leftover_args')
    fam_ty :: Type
fam_ty = TyCon -> [Type] -> Type
mkTyConApp TyCon
fam_tc [Type]
sat_fam_args'
    FlattenEnv { fe_type_map :: FlattenEnv -> TypeMap TyVar
fe_type_map = TypeMap TyVar
type_map
               , fe_in_scope :: FlattenEnv -> InScopeSet
fe_in_scope = InScopeSet
in_scope } = FlattenEnv
env'

mkFlattenFreshTyName :: Uniquable a => a -> Name
mkFlattenFreshTyName :: forall a. Uniquable a => a -> Name
mkFlattenFreshTyName a
unq
  = Unique -> FastString -> Name
mkSysTvName (a -> Unique
forall a. Uniquable a => a -> Unique
getUnique a
unq) (String -> FastString
fsLit String
"flt")

mkFlattenFreshCoVar :: InScopeSet -> Kind -> CoVar
mkFlattenFreshCoVar :: InScopeSet -> Type -> TyVar
mkFlattenFreshCoVar InScopeSet
in_scope Type
kind
  = let uniq :: Unique
uniq = InScopeSet -> Unique
unsafeGetFreshLocalUnique InScopeSet
in_scope
        name :: Name
name = Unique -> FastString -> Name
mkSystemVarName Unique
uniq (String -> FastString
fsLit String
"flc")
    in Name -> Type -> TyVar
mkCoVar Name
name Type
kind