-- The @FamInst@ type: family instance heads

{-# LANGUAGE CPP, GADTs #-}

module FamInst (
        FamInstEnvs, tcGetFamInstEnvs,
        checkFamInstConsistency, tcExtendLocalFamInstEnv,
        tcLookupDataFamInst, tcLookupDataFamInst_maybe,
        tcInstNewTyCon_maybe, tcTopNormaliseNewTypeTF_maybe,
        newFamInst,

        -- * Injectivity
        makeInjectivityErrors, injTyVarsOfType, injTyVarsOfTypes
    ) where

import GhcPrelude

import HscTypes
import FamInstEnv
import InstEnv( roughMatchTcs )
import Coercion
import CoreLint
import TcEvidence
import LoadIface
import TcRnMonad
import SrcLoc
import TyCon
import TcType
import CoAxiom
import DynFlags
import Module
import Outputable
import Util
import RdrName
import DataCon ( dataConName )
import Maybes
import Type
import TyCoRep
import TcMType
import Name
import Pair
import Panic
import VarSet
import Bag( Bag, unionBags, unitBag )
import Control.Monad

#include "HsVersions.h"

{- Note [The type family instance consistency story]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

To preserve type safety we must ensure that for any given module, all
the type family instances used either in that module or in any module
it directly or indirectly imports are consistent. For example, consider

  module F where
    type family F a

  module A where
    import F( F )
    type instance F Int = Bool
    f :: F Int -> Bool
    f x = x

  module B where
    import F( F )
    type instance F Int = Char
    g :: Char -> F Int
    g x = x

  module Bad where
    import A( f )
    import B( g )
    bad :: Char -> Int
    bad c = f (g c)

Even though module Bad never mentions the type family F at all, by
combining the functions f and g that were type checked in contradictory
type family instance environments, the function bad is able to coerce
from one type to another. So when we type check Bad we must verify that
the type family instances defined in module A are consistent with those
defined in module B.

How do we ensure that we maintain the necessary consistency?

* Call a module which defines at least one type family instance a
  "family instance module". This flag `mi_finsts` is recorded in the
  interface file.

* For every module we calculate the set of all of its direct and
  indirect dependencies that are family instance modules. This list
  `dep_finsts` is also recorded in the interface file so we can compute
  this list for a module from the lists for its direct dependencies.

* When type checking a module M we check consistency of all the type
  family instances that are either provided by its `dep_finsts` or
  defined in the module M itself. This is a pairwise check, i.e., for
  every pair of instances we must check that they are consistent.

  - For family instances coming from `dep_finsts`, this is checked in
    checkFamInstConsistency, called from tcRnImports. See Note
    [Checking family instance consistency] for details on this check
    (and in particular how we avoid having to do all these checks for
    every module we compile).

  - That leaves checking the family instances defined in M itself
    against instances defined in either M or its `dep_finsts`. This is
    checked in `tcExtendLocalFamInstEnv'.

There are four subtle points in this scheme which have not been
addressed yet.

* We have checked consistency of the family instances *defined* by M
  or its imports, but this is not by definition the same thing as the
  family instances *used* by M or its imports.  Specifically, we need to
  ensure when we use a type family instance while compiling M that this
  instance was really defined from either M or one of its imports,
  rather than being an instance that we happened to know about from
  reading an interface file in the course of compiling an unrelated
  module. Otherwise, we'll end up with no record of the fact that M
  depends on this family instance and type safety will be compromised.
  See #13102.

* It can also happen that M uses a function defined in another module
  which is not transitively imported by M. Examples include the
  desugaring of various overloaded constructs, and references inserted
  by Template Haskell splices. If that function's definition makes use
  of type family instances which are not checked against those visible
  from M, type safety can again be compromised. See #13251.

* When a module C imports a boot module B.hs-boot, we check that C's
  type family instances are compatible with those visible from
  B.hs-boot. However, C will eventually be linked against a different
  module B.hs, which might define additional type family instances which
  are inconsistent with C's. This can also lead to loss of type safety.
  See #9562.

* The call to checkFamConsistency for imported functions occurs very
  early (in tcRnImports) and that causes problems if the imported
  instances use type declared in the module being compiled.
  See Note [Loading your own hi-boot file] in LoadIface.
-}

{-
************************************************************************
*                                                                      *
                 Making a FamInst
*                                                                      *
************************************************************************
-}

-- All type variables in a FamInst must be fresh. This function
-- creates the fresh variables and applies the necessary substitution
-- It is defined here to avoid a dependency from FamInstEnv on the monad
-- code.

newFamInst :: FamFlavor -> CoAxiom Unbranched -> TcM FamInst
-- Freshen the type variables of the FamInst branches
newFamInst :: FamFlavor -> CoAxiom Unbranched -> TcM FamInst
newFamInst flavor :: FamFlavor
flavor axiom :: CoAxiom Unbranched
axiom@(CoAxiom { co_ax_tc :: forall (br :: BranchFlag). CoAxiom br -> TyCon
co_ax_tc = TyCon
fam_tc })
  = ASSERT2( tyCoVarsOfTypes lhs `subVarSet` tcv_set, text "lhs" <+> pp_ax )
    ASSERT2( tyCoVarsOfType  rhs `subVarSet` tcv_set, text "rhs" <+> pp_ax )
    ASSERT2( lhs_kind `eqType` rhs_kind, text "kind" <+> pp_ax $$ ppr lhs_kind $$ ppr rhs_kind )
    do { (subst :: TCvSubst
subst, tvs' :: [TyVar]
tvs') <- [TyVar] -> TcM (TCvSubst, [TyVar])
freshenTyVarBndrs [TyVar]
tvs
       ; (subst :: TCvSubst
subst, cvs' :: [TyVar]
cvs') <- TCvSubst -> [TyVar] -> TcM (TCvSubst, [TyVar])
freshenCoVarBndrsX TCvSubst
subst [TyVar]
cvs
       ; DynFlags
dflags <- IOEnv (Env TcGblEnv TcLclEnv) DynFlags
forall (m :: * -> *). HasDynFlags m => m DynFlags
getDynFlags
       ; let lhs' :: [Type]
lhs'     = HasCallStack => TCvSubst -> [Type] -> [Type]
TCvSubst -> [Type] -> [Type]
substTys TCvSubst
subst [Type]
lhs
             rhs' :: Type
rhs'     = HasCallStack => TCvSubst -> Type -> Type
TCvSubst -> Type -> Type
substTy  TCvSubst
subst Type
rhs
             tcvs' :: [TyVar]
tcvs'    = [TyVar]
tvs' [TyVar] -> [TyVar] -> [TyVar]
forall a. [a] -> [a] -> [a]
++ [TyVar]
cvs'
       ; TcRn () -> TcRn () -> TcRn ()
forall r. TcRn r -> TcRn r -> TcRn r
ifErrsM (() -> TcRn ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()) (TcRn () -> TcRn ()) -> TcRn () -> TcRn ()
forall a b. (a -> b) -> a -> b
$ -- Don't lint when there are errors, because
                               -- errors might mean TcTyCons.
                               -- See Note [Recover from validity error] in TcTyClsDecls
         Bool -> TcRn () -> TcRn ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (GeneralFlag -> DynFlags -> Bool
gopt GeneralFlag
Opt_DoCoreLinting DynFlags
dflags) (TcRn () -> TcRn ()) -> TcRn () -> TcRn ()
forall a b. (a -> b) -> a -> b
$
           -- Check that the types involved in this instance are well formed.
           -- Do /not/ expand type synonyms, for the reasons discussed in
           -- Note [Linting type synonym applications].
           case DynFlags -> [TyVar] -> [Type] -> Maybe SDoc
lintTypes DynFlags
dflags [TyVar]
tcvs' (Type
rhs'Type -> [Type] -> [Type]
forall a. a -> [a] -> [a]
:[Type]
lhs') of
             Nothing       -> () -> TcRn ()
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
             Just fail_msg :: SDoc
fail_msg -> String -> SDoc -> TcRn ()
forall a. HasCallStack => String -> SDoc -> a
pprPanic "Core Lint error" ([SDoc] -> SDoc
vcat [ SDoc
fail_msg
                                                               , TyCon -> SDoc
forall a. Outputable a => a -> SDoc
ppr TyCon
fam_tc
                                                               , TCvSubst -> SDoc
forall a. Outputable a => a -> SDoc
ppr TCvSubst
subst
                                                               , [TyVar] -> SDoc
forall a. Outputable a => a -> SDoc
ppr [TyVar]
tvs'
                                                               , [TyVar] -> SDoc
forall a. Outputable a => a -> SDoc
ppr [TyVar]
cvs'
                                                               , [Type] -> SDoc
forall a. Outputable a => a -> SDoc
ppr [Type]
lhs'
                                                               , Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
rhs' ])
       ; FamInst -> TcM FamInst
forall (m :: * -> *) a. Monad m => a -> m a
return (FamInst :: CoAxiom Unbranched
-> FamFlavor
-> Name
-> [Maybe Name]
-> [TyVar]
-> [TyVar]
-> [Type]
-> Type
-> FamInst
FamInst { fi_fam :: Name
fi_fam      = TyCon -> Name
tyConName TyCon
fam_tc
                         , fi_flavor :: FamFlavor
fi_flavor   = FamFlavor
flavor
                         , fi_tcs :: [Maybe Name]
fi_tcs      = [Type] -> [Maybe Name]
roughMatchTcs [Type]
lhs
                         , fi_tvs :: [TyVar]
fi_tvs      = [TyVar]
tvs'
                         , fi_cvs :: [TyVar]
fi_cvs      = [TyVar]
cvs'
                         , fi_tys :: [Type]
fi_tys      = [Type]
lhs'
                         , fi_rhs :: Type
fi_rhs      = Type
rhs'
                         , fi_axiom :: CoAxiom Unbranched
fi_axiom    = CoAxiom Unbranched
axiom }) }
  where
    lhs_kind :: Type
lhs_kind = HasDebugCallStack => Type -> Type
Type -> Type
tcTypeKind (TyCon -> [Type] -> Type
mkTyConApp TyCon
fam_tc [Type]
lhs)
    rhs_kind :: Type
rhs_kind = HasDebugCallStack => Type -> Type
Type -> Type
tcTypeKind Type
rhs
    tcv_set :: TyCoVarSet
tcv_set  = [TyVar] -> TyCoVarSet
mkVarSet ([TyVar]
tvs [TyVar] -> [TyVar] -> [TyVar]
forall a. [a] -> [a] -> [a]
++ [TyVar]
cvs)
    pp_ax :: SDoc
pp_ax    = CoAxiom Unbranched -> SDoc
forall (br :: BranchFlag). CoAxiom br -> SDoc
pprCoAxiom CoAxiom Unbranched
axiom
    CoAxBranch { cab_tvs :: CoAxBranch -> [TyVar]
cab_tvs = [TyVar]
tvs
               , cab_cvs :: CoAxBranch -> [TyVar]
cab_cvs = [TyVar]
cvs
               , cab_lhs :: CoAxBranch -> [Type]
cab_lhs = [Type]
lhs
               , cab_rhs :: CoAxBranch -> Type
cab_rhs = Type
rhs } = CoAxiom Unbranched -> CoAxBranch
coAxiomSingleBranch CoAxiom Unbranched
axiom


{-
************************************************************************
*                                                                      *
        Optimised overlap checking for family instances
*                                                                      *
************************************************************************

Note [Checking family instance consistency]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
For any two family instance modules that we import directly or indirectly, we
check whether the instances in the two modules are consistent, *unless* we can
be certain that the instances of the two modules have already been checked for
consistency during the compilation of modules that we import.

Why do we need to check?  Consider
   module X1 where                module X2 where
    data T1                         data T2
    type instance F T1 b = Int      type instance F a T2 = Char
    f1 :: F T1 a -> Int             f2 :: Char -> F a T2
    f1 x = x                        f2 x = x

Now if we import both X1 and X2 we could make (f2 . f1) :: Int -> Char.
Notice that neither instance is an orphan.

How do we know which pairs of modules have already been checked? For each
module M we directly import, we look up the family instance modules that M
imports (directly or indirectly), say F1, ..., FN. For any two modules
among M, F1, ..., FN, we know that the family instances defined in those
two modules are consistent--because we checked that when we compiled M.

For every other pair of family instance modules we import (directly or
indirectly), we check that they are consistent now. (So that we can be
certain that the modules in our `HscTypes.dep_finsts' are consistent.)

There is some fancy footwork regarding hs-boot module loops, see
Note [Don't check hs-boot type family instances too early]

Note [Checking family instance optimization]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
As explained in Note [Checking family instance consistency]
we need to ensure that every pair of transitive imports that define type family
instances is consistent.

Let's define df(A) = transitive imports of A that define type family instances
+ A, if A defines type family instances

Then for every direct import A, df(A) is already consistent.

Let's name the current module M.

We want to make sure that df(M) is consistent.
df(M) = df(D_1) U df(D_2) U ... U df(D_i) where D_1 .. D_i are direct imports.

We perform the check iteratively, maintaining a set of consistent modules 'C'
and trying to add df(D_i) to it.

The key part is how to ensure that the union C U df(D_i) is consistent.

Let's consider two modules: A and B from C U df(D_i).
There are nine possible ways to choose A and B from C U df(D_i):

             | A in C only      | A in C and B in df(D_i) | A in df(D_i) only
--------------------------------------------------------------------------------
B in C only  | Already checked  | Already checked         | Needs to be checked
             | when checking C  | when checking C         |
--------------------------------------------------------------------------------
B in C and   | Already checked  | Already checked         | Already checked when
B in df(D_i) | when checking C  | when checking C         | checking df(D_i)
--------------------------------------------------------------------------------
B in df(D_i) | Needs to be      | Already checked         | Already checked when
only         | checked          | when checking df(D_i)   | checking df(D_i)

That means to ensure that C U df(D_i) is consistent we need to check every
module from C - df(D_i) against every module from df(D_i) - C and
every module from df(D_i) - C against every module from C - df(D_i).
But since the checks are symmetric it suffices to pick A from C - df(D_i)
and B from df(D_i) - C.

In other words these are the modules we need to check:
  [ (m1, m2) | m1 <- C, m1 not in df(D_i)
             , m2 <- df(D_i), m2 not in C ]

One final thing to note here is that if there's lot of overlap between
subsequent df(D_i)'s then we expect those set differences to be small.
That situation should be pretty common in practice, there's usually
a set of utility modules that every module imports directly or indirectly.

This is basically the idea from #13092, comment:14.
-}

-- This function doesn't check ALL instances for consistency,
-- only ones that aren't involved in recursive knot-tying
-- loops; see Note [Don't check hs-boot type family instances too early].
-- We don't need to check the current module, this is done in
-- tcExtendLocalFamInstEnv.
-- See Note [The type family instance consistency story].
checkFamInstConsistency :: [Module] -> TcM ()
checkFamInstConsistency :: [Module] -> TcRn ()
checkFamInstConsistency directlyImpMods :: [Module]
directlyImpMods
  = do { DynFlags
dflags     <- IOEnv (Env TcGblEnv TcLclEnv) DynFlags
forall (m :: * -> *). HasDynFlags m => m DynFlags
getDynFlags
       ; (eps :: ExternalPackageState
eps, hpt :: HomePackageTable
hpt) <- TcRnIf TcGblEnv TcLclEnv (ExternalPackageState, HomePackageTable)
forall gbl lcl.
TcRnIf gbl lcl (ExternalPackageState, HomePackageTable)
getEpsAndHpt
       ; String -> SDoc -> TcRn ()
traceTc "checkFamInstConsistency" ([Module] -> SDoc
forall a. Outputable a => a -> SDoc
ppr [Module]
directlyImpMods)
       ; let { -- Fetch the iface of a given module.  Must succeed as
               -- all directly imported modules must already have been loaded.
               modIface :: Module -> ModIface
modIface mod :: Module
mod =
                 case DynFlags
-> HomePackageTable
-> PackageIfaceTable
-> Module
-> Maybe ModIface
lookupIfaceByModule DynFlags
dflags HomePackageTable
hpt (ExternalPackageState -> PackageIfaceTable
eps_PIT ExternalPackageState
eps) Module
mod of
                   Nothing    -> String -> SDoc -> ModIface
forall a. String -> SDoc -> a
panicDoc "FamInst.checkFamInstConsistency"
                                          (Module -> SDoc
forall a. Outputable a => a -> SDoc
ppr Module
mod SDoc -> SDoc -> SDoc
$$ HomePackageTable -> SDoc
pprHPT HomePackageTable
hpt)
                   Just iface :: ModIface
iface -> ModIface
iface

               -- Which family instance modules were checked for consistency
               -- when we compiled `mod`?
               -- Itself (if a family instance module) and its dep_finsts.
               -- This is df(D_i) from
               -- Note [Checking family instance optimization]
             ; modConsistent :: Module -> [Module]
             ; modConsistent :: Module -> [Module]
modConsistent mod :: Module
mod =
                 if ModIface -> Bool
mi_finsts (Module -> ModIface
modIface Module
mod) then Module
modModule -> [Module] -> [Module]
forall a. a -> [a] -> [a]
:[Module]
deps else [Module]
deps
                 where
                 deps :: [Module]
deps = Dependencies -> [Module]
dep_finsts (Dependencies -> [Module])
-> (Module -> Dependencies) -> Module -> [Module]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ModIface -> Dependencies
mi_deps (ModIface -> Dependencies)
-> (Module -> ModIface) -> Module -> Dependencies
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Module -> ModIface
modIface (Module -> [Module]) -> Module -> [Module]
forall a b. (a -> b) -> a -> b
$ Module
mod

             ; hmiModule :: HomeModInfo -> Module
hmiModule     = ModIface -> Module
mi_module (ModIface -> Module)
-> (HomeModInfo -> ModIface) -> HomeModInfo -> Module
forall b c a. (b -> c) -> (a -> b) -> a -> c
. HomeModInfo -> ModIface
hm_iface
             ; hmiFamInstEnv :: HomeModInfo -> FamInstEnv
hmiFamInstEnv = FamInstEnv -> [FamInst] -> FamInstEnv
extendFamInstEnvList FamInstEnv
emptyFamInstEnv
                               ([FamInst] -> FamInstEnv)
-> (HomeModInfo -> [FamInst]) -> HomeModInfo -> FamInstEnv
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ModDetails -> [FamInst]
md_fam_insts (ModDetails -> [FamInst])
-> (HomeModInfo -> ModDetails) -> HomeModInfo -> [FamInst]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. HomeModInfo -> ModDetails
hm_details
             ; hpt_fam_insts :: ModuleEnv FamInstEnv
hpt_fam_insts = [(Module, FamInstEnv)] -> ModuleEnv FamInstEnv
forall a. [(Module, a)] -> ModuleEnv a
mkModuleEnv [ (HomeModInfo -> Module
hmiModule HomeModInfo
hmi, HomeModInfo -> FamInstEnv
hmiFamInstEnv HomeModInfo
hmi)
                                           | HomeModInfo
hmi <- HomePackageTable -> [HomeModInfo]
eltsHpt HomePackageTable
hpt]

             }

       ; ModuleEnv FamInstEnv -> (Module -> [Module]) -> [Module] -> TcRn ()
checkMany ModuleEnv FamInstEnv
hpt_fam_insts Module -> [Module]
modConsistent [Module]
directlyImpMods
       }
  where
    -- See Note [Checking family instance optimization]
    checkMany
      :: ModuleEnv FamInstEnv   -- home package family instances
      -> (Module -> [Module])   -- given A, modules checked when A was checked
      -> [Module]               -- modules to process
      -> TcM ()
    checkMany :: ModuleEnv FamInstEnv -> (Module -> [Module]) -> [Module] -> TcRn ()
checkMany hpt_fam_insts :: ModuleEnv FamInstEnv
hpt_fam_insts modConsistent :: Module -> [Module]
modConsistent mods :: [Module]
mods = [Module] -> ModuleSet -> [Module] -> TcRn ()
go [] ModuleSet
emptyModuleSet [Module]
mods
      where
      go :: [Module] -- list of consistent modules
         -> ModuleSet -- set of consistent modules, same elements as the
                      -- list above
         -> [Module] -- modules to process
         -> TcM ()
      go :: [Module] -> ModuleSet -> [Module] -> TcRn ()
go _ _ [] = () -> TcRn ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
      go consistent :: [Module]
consistent consistent_set :: ModuleSet
consistent_set (mod :: Module
mod:mods :: [Module]
mods) = do
        [TcRn ()] -> TcRn ()
forall (t :: * -> *) (m :: * -> *) a.
(Foldable t, Monad m) =>
t (m a) -> m ()
sequence_
          [ ModuleEnv FamInstEnv -> Module -> Module -> TcRn ()
check ModuleEnv FamInstEnv
hpt_fam_insts Module
m1 Module
m2
          | Module
m1 <- [Module]
to_check_from_mod
            -- loop over toCheckFromMod first, it's usually smaller,
            -- it may even be empty
          , Module
m2 <- [Module]
to_check_from_consistent
          ]
        [Module] -> ModuleSet -> [Module] -> TcRn ()
go [Module]
consistent' ModuleSet
consistent_set' [Module]
mods
        where
        mod_deps_consistent :: [Module]
mod_deps_consistent =  Module -> [Module]
modConsistent Module
mod
        mod_deps_consistent_set :: ModuleSet
mod_deps_consistent_set = [Module] -> ModuleSet
mkModuleSet [Module]
mod_deps_consistent
        consistent' :: [Module]
consistent' = [Module]
to_check_from_mod [Module] -> [Module] -> [Module]
forall a. [a] -> [a] -> [a]
++ [Module]
consistent
        consistent_set' :: ModuleSet
consistent_set' =
          ModuleSet -> [Module] -> ModuleSet
extendModuleSetList ModuleSet
consistent_set [Module]
to_check_from_mod
        to_check_from_consistent :: [Module]
to_check_from_consistent =
          (Module -> Bool) -> [Module] -> [Module]
forall a. (a -> Bool) -> [a] -> [a]
filterOut (Module -> ModuleSet -> Bool
`elemModuleSet` ModuleSet
mod_deps_consistent_set) [Module]
consistent
        to_check_from_mod :: [Module]
to_check_from_mod =
          (Module -> Bool) -> [Module] -> [Module]
forall a. (a -> Bool) -> [a] -> [a]
filterOut (Module -> ModuleSet -> Bool
`elemModuleSet` ModuleSet
consistent_set) [Module]
mod_deps_consistent
        -- Why don't we just minusModuleSet here?
        -- We could, but doing so means one of two things:
        --
        --   1. When looping over the cartesian product we convert
        --   a set into a non-deterministicly ordered list. Which
        --   happens to be fine for interface file determinism
        --   in this case, today, because the order only
        --   determines the order of deferred checks. But such
        --   invariants are hard to keep.
        --
        --   2. When looping over the cartesian product we convert
        --   a set into a deterministically ordered list - this
        --   adds some additional cost of sorting for every
        --   direct import.
        --
        --   That also explains why we need to keep both 'consistent'
        --   and 'consistentSet'.
        --
        --   See also Note [ModuleEnv performance and determinism].
    check :: ModuleEnv FamInstEnv -> Module -> Module -> TcRn ()
check hpt_fam_insts :: ModuleEnv FamInstEnv
hpt_fam_insts m1 :: Module
m1 m2 :: Module
m2
      = do { FamInstEnv
env1' <- ModuleEnv FamInstEnv -> Module -> TcM FamInstEnv
getFamInsts ModuleEnv FamInstEnv
hpt_fam_insts Module
m1
           ; FamInstEnv
env2' <- ModuleEnv FamInstEnv -> Module -> TcM FamInstEnv
getFamInsts ModuleEnv FamInstEnv
hpt_fam_insts Module
m2
           -- We're checking each element of env1 against env2.
           -- The cost of that is dominated by the size of env1, because
           -- for each instance in env1 we look it up in the type family
           -- environment env2, and lookup is cheap.
           -- The code below ensures that env1 is the smaller environment.
           ; let sizeE1 :: Int
sizeE1 = FamInstEnv -> Int
famInstEnvSize FamInstEnv
env1'
                 sizeE2 :: Int
sizeE2 = FamInstEnv -> Int
famInstEnvSize FamInstEnv
env2'
                 (env1 :: FamInstEnv
env1, env2 :: FamInstEnv
env2) = if Int
sizeE1 Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
sizeE2 then (FamInstEnv
env1', FamInstEnv
env2')
                                                   else (FamInstEnv
env2', FamInstEnv
env1')
           -- Note [Don't check hs-boot type family instances too early]
           -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
           -- Family instance consistency checking involves checking that
           -- the family instances of our imported modules are consistent with
           -- one another; this might lead you to think that this process
           -- has nothing to do with the module we are about to typecheck.
           -- Not so!  Consider the following case:
           --
           --   -- A.hs-boot
           --   type family F a
           --
           --   -- B.hs
           --   import {-# SOURCE #-} A
           --   type instance F Int = Bool
           --
           --   -- A.hs
           --   import B
           --   type family F a
           --
           -- When typechecking A, we are NOT allowed to poke the TyThing
           -- for F until we have typechecked the family.  Thus, we
           -- can't do consistency checking for the instance in B
           -- (checkFamInstConsistency is called during renaming).
           -- Failing to defer the consistency check lead to #11062.
           --
           -- Additionally, we should also defer consistency checking when
           -- type from the hs-boot file of the current module occurs on
           -- the left hand side, as we will poke its TyThing when checking
           -- for overlap.
           --
           --   -- F.hs
           --   type family F a
           --
           --   -- A.hs-boot
           --   import F
           --   data T
           --
           --   -- B.hs
           --   import {-# SOURCE #-} A
           --   import F
           --   type instance F T = Int
           --
           --   -- A.hs
           --   import B
           --   data T = MkT
           --
           -- In fact, it is even necessary to defer for occurrences in
           -- the RHS, because we may test for *compatibility* in event
           -- of an overlap.
           --
           -- Why don't we defer ALL of the checks to later?  Well, many
           -- instances aren't involved in the recursive loop at all.  So
           -- we might as well check them immediately; and there isn't
           -- a good time to check them later in any case: every time
           -- we finish kind-checking a type declaration and add it to
           -- a context, we *then* consistency check all of the instances
           -- which mentioned that type.  We DO want to check instances
           -- as quickly as possible, so that we aren't typechecking
           -- values with inconsistent axioms in scope.
           --
           -- See also Note [Tying the knot]
           -- for why we are doing this at all.
           ; let check_now :: [FamInst]
check_now = FamInstEnv -> [FamInst]
famInstEnvElts FamInstEnv
env1
           ; (FamInst -> IOEnv (Env TcGblEnv TcLclEnv) Bool)
-> [FamInst] -> TcRn ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ ((FamInstEnv, FamInstEnv)
-> FamInst -> IOEnv (Env TcGblEnv TcLclEnv) Bool
checkForConflicts (FamInstEnv
emptyFamInstEnv, FamInstEnv
env2))           [FamInst]
check_now
           ; (FamInst -> IOEnv (Env TcGblEnv TcLclEnv) Bool)
-> [FamInst] -> TcRn ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ ((FamInstEnv, FamInstEnv)
-> FamInst -> IOEnv (Env TcGblEnv TcLclEnv) Bool
checkForInjectivityConflicts (FamInstEnv
emptyFamInstEnv,FamInstEnv
env2)) [FamInst]
check_now
 }

getFamInsts :: ModuleEnv FamInstEnv -> Module -> TcM FamInstEnv
getFamInsts :: ModuleEnv FamInstEnv -> Module -> TcM FamInstEnv
getFamInsts hpt_fam_insts :: ModuleEnv FamInstEnv
hpt_fam_insts mod :: Module
mod
  | Just env :: FamInstEnv
env <- ModuleEnv FamInstEnv -> Module -> Maybe FamInstEnv
forall a. ModuleEnv a -> Module -> Maybe a
lookupModuleEnv ModuleEnv FamInstEnv
hpt_fam_insts Module
mod = FamInstEnv -> TcM FamInstEnv
forall (m :: * -> *) a. Monad m => a -> m a
return FamInstEnv
env
  | Bool
otherwise = do { ModIface
_ <- IfG ModIface -> TcRn ModIface
forall a. IfG a -> TcRn a
initIfaceTcRn (SDoc -> Module -> IfG ModIface
forall lcl. SDoc -> Module -> IfM lcl ModIface
loadSysInterface SDoc
doc Module
mod)
                   ; ExternalPackageState
eps <- TcRnIf TcGblEnv TcLclEnv ExternalPackageState
forall gbl lcl. TcRnIf gbl lcl ExternalPackageState
getEps
                   ; FamInstEnv -> TcM FamInstEnv
forall (m :: * -> *) a. Monad m => a -> m a
return (String -> Maybe FamInstEnv -> FamInstEnv
forall a. HasCallStack => String -> Maybe a -> a
expectJust "checkFamInstConsistency" (Maybe FamInstEnv -> FamInstEnv) -> Maybe FamInstEnv -> FamInstEnv
forall a b. (a -> b) -> a -> b
$
                             ModuleEnv FamInstEnv -> Module -> Maybe FamInstEnv
forall a. ModuleEnv a -> Module -> Maybe a
lookupModuleEnv (ExternalPackageState -> ModuleEnv FamInstEnv
eps_mod_fam_inst_env ExternalPackageState
eps) Module
mod) }
  where
    doc :: SDoc
doc = Module -> SDoc
forall a. Outputable a => a -> SDoc
ppr Module
mod SDoc -> SDoc -> SDoc
<+> String -> SDoc
text "is a family-instance module"

{-
************************************************************************
*                                                                      *
        Lookup
*                                                                      *
************************************************************************

-}

-- | If @co :: T ts ~ rep_ty@ then:
--
-- > instNewTyCon_maybe T ts = Just (rep_ty, co)
--
-- Checks for a newtype, and for being saturated
-- Just like Coercion.instNewTyCon_maybe, but returns a TcCoercion
tcInstNewTyCon_maybe :: TyCon -> [TcType] -> Maybe (TcType, TcCoercion)
tcInstNewTyCon_maybe :: TyCon -> [Type] -> Maybe (Type, TcCoercion)
tcInstNewTyCon_maybe = TyCon -> [Type] -> Maybe (Type, TcCoercion)
instNewTyCon_maybe

-- | Like 'tcLookupDataFamInst_maybe', but returns the arguments back if
-- there is no data family to unwrap.
-- Returns a Representational coercion
tcLookupDataFamInst :: FamInstEnvs -> TyCon -> [TcType]
                    -> (TyCon, [TcType], Coercion)
tcLookupDataFamInst :: (FamInstEnv, FamInstEnv)
-> TyCon -> [Type] -> (TyCon, [Type], TcCoercion)
tcLookupDataFamInst fam_inst_envs :: (FamInstEnv, FamInstEnv)
fam_inst_envs tc :: TyCon
tc tc_args :: [Type]
tc_args
  | Just (rep_tc :: TyCon
rep_tc, rep_args :: [Type]
rep_args, co :: TcCoercion
co)
      <- (FamInstEnv, FamInstEnv)
-> TyCon -> [Type] -> Maybe (TyCon, [Type], TcCoercion)
tcLookupDataFamInst_maybe (FamInstEnv, FamInstEnv)
fam_inst_envs TyCon
tc [Type]
tc_args
  = (TyCon
rep_tc, [Type]
rep_args, TcCoercion
co)
  | Bool
otherwise
  = (TyCon
tc, [Type]
tc_args, Type -> TcCoercion
mkRepReflCo (TyCon -> [Type] -> Type
mkTyConApp TyCon
tc [Type]
tc_args))

tcLookupDataFamInst_maybe :: FamInstEnvs -> TyCon -> [TcType]
                          -> Maybe (TyCon, [TcType], Coercion)
-- ^ Converts a data family type (eg F [a]) to its representation type (eg FList a)
-- and returns a coercion between the two: co :: F [a] ~R FList a.
tcLookupDataFamInst_maybe :: (FamInstEnv, FamInstEnv)
-> TyCon -> [Type] -> Maybe (TyCon, [Type], TcCoercion)
tcLookupDataFamInst_maybe fam_inst_envs :: (FamInstEnv, FamInstEnv)
fam_inst_envs tc :: TyCon
tc tc_args :: [Type]
tc_args
  | TyCon -> Bool
isDataFamilyTyCon TyCon
tc
  , match :: FamInstMatch
match : _ <- (FamInstEnv, FamInstEnv) -> TyCon -> [Type] -> [FamInstMatch]
lookupFamInstEnv (FamInstEnv, FamInstEnv)
fam_inst_envs TyCon
tc [Type]
tc_args
  , FamInstMatch { fim_instance :: FamInstMatch -> FamInst
fim_instance = rep_fam :: FamInst
rep_fam@(FamInst { fi_axiom :: FamInst -> CoAxiom Unbranched
fi_axiom = CoAxiom Unbranched
ax
                                                   , fi_cvs :: FamInst -> [TyVar]
fi_cvs   = [TyVar]
cvs })
                 , fim_tys :: FamInstMatch -> [Type]
fim_tys      = [Type]
rep_args
                 , fim_cos :: FamInstMatch -> [TcCoercion]
fim_cos      = [TcCoercion]
rep_cos } <- FamInstMatch
match
  , let rep_tc :: TyCon
rep_tc = FamInst -> TyCon
dataFamInstRepTyCon FamInst
rep_fam
        co :: TcCoercion
co     = Role -> CoAxiom Unbranched -> [Type] -> [TcCoercion] -> TcCoercion
mkUnbranchedAxInstCo Role
Representational CoAxiom Unbranched
ax [Type]
rep_args
                                      ([TyVar] -> [TcCoercion]
mkCoVarCos [TyVar]
cvs)
  = ASSERT( null rep_cos ) -- See Note [Constrained family instances] in FamInstEnv
    (TyCon, [Type], TcCoercion) -> Maybe (TyCon, [Type], TcCoercion)
forall a. a -> Maybe a
Just (TyCon
rep_tc, [Type]
rep_args, TcCoercion
co)

  | Bool
otherwise
  = Maybe (TyCon, [Type], TcCoercion)
forall a. Maybe a
Nothing

-- | 'tcTopNormaliseNewTypeTF_maybe' gets rid of top-level newtypes,
-- potentially looking through newtype /instances/.
--
-- It is only used by the type inference engine (specifically, when
-- solving representational equality), and hence it is careful to unwrap
-- only if the relevant data constructor is in scope.  That's why
-- it get a GlobalRdrEnv argument.
--
-- It is careful not to unwrap data/newtype instances if it can't
-- continue unwrapping.  Such care is necessary for proper error
-- messages.
--
-- It does not look through type families.
-- It does not normalise arguments to a tycon.
--
-- If the result is Just (rep_ty, (co, gres), rep_ty), then
--    co : ty ~R rep_ty
--    gres are the GREs for the data constructors that
--                          had to be in scope
tcTopNormaliseNewTypeTF_maybe :: FamInstEnvs
                              -> GlobalRdrEnv
                              -> Type
                              -> Maybe ((Bag GlobalRdrElt, TcCoercion), Type)
tcTopNormaliseNewTypeTF_maybe :: (FamInstEnv, FamInstEnv)
-> GlobalRdrEnv
-> Type
-> Maybe ((Bag GlobalRdrElt, TcCoercion), Type)
tcTopNormaliseNewTypeTF_maybe faminsts :: (FamInstEnv, FamInstEnv)
faminsts rdr_env :: GlobalRdrEnv
rdr_env ty :: Type
ty
-- cf. FamInstEnv.topNormaliseType_maybe and Coercion.topNormaliseNewType_maybe
  = NormaliseStepper (Bag GlobalRdrElt, TcCoercion)
-> ((Bag GlobalRdrElt, TcCoercion)
    -> (Bag GlobalRdrElt, TcCoercion)
    -> (Bag GlobalRdrElt, TcCoercion))
-> Type
-> Maybe ((Bag GlobalRdrElt, TcCoercion), Type)
forall ev.
NormaliseStepper ev -> (ev -> ev -> ev) -> Type -> Maybe (ev, Type)
topNormaliseTypeX NormaliseStepper (Bag GlobalRdrElt, TcCoercion)
stepper (Bag GlobalRdrElt, TcCoercion)
-> (Bag GlobalRdrElt, TcCoercion) -> (Bag GlobalRdrElt, TcCoercion)
plus Type
ty
  where
    plus :: (Bag GlobalRdrElt, TcCoercion) -> (Bag GlobalRdrElt, TcCoercion)
         -> (Bag GlobalRdrElt, TcCoercion)
    plus :: (Bag GlobalRdrElt, TcCoercion)
-> (Bag GlobalRdrElt, TcCoercion) -> (Bag GlobalRdrElt, TcCoercion)
plus (gres1 :: Bag GlobalRdrElt
gres1, co1 :: TcCoercion
co1) (gres2 :: Bag GlobalRdrElt
gres2, co2 :: TcCoercion
co2) = ( Bag GlobalRdrElt
gres1 Bag GlobalRdrElt -> Bag GlobalRdrElt -> Bag GlobalRdrElt
forall a. Bag a -> Bag a -> Bag a
`unionBags` Bag GlobalRdrElt
gres2
                                     , TcCoercion
co1 TcCoercion -> TcCoercion -> TcCoercion
`mkTransCo` TcCoercion
co2 )

    stepper :: NormaliseStepper (Bag GlobalRdrElt, TcCoercion)
    stepper :: NormaliseStepper (Bag GlobalRdrElt, TcCoercion)
stepper = NormaliseStepper (Bag GlobalRdrElt, TcCoercion)
unwrap_newtype NormaliseStepper (Bag GlobalRdrElt, TcCoercion)
-> NormaliseStepper (Bag GlobalRdrElt, TcCoercion)
-> NormaliseStepper (Bag GlobalRdrElt, TcCoercion)
forall ev.
NormaliseStepper ev -> NormaliseStepper ev -> NormaliseStepper ev
`composeSteppers` NormaliseStepper (Bag GlobalRdrElt, TcCoercion)
unwrap_newtype_instance

    -- For newtype instances we take a double step or nothing, so that
    -- we don't return the representation type of the newtype instance,
    -- which would lead to terrible error messages
    unwrap_newtype_instance :: NormaliseStepper (Bag GlobalRdrElt, TcCoercion)
unwrap_newtype_instance rec_nts :: RecTcChecker
rec_nts tc :: TyCon
tc tys :: [Type]
tys
      | Just (tc' :: TyCon
tc', tys' :: [Type]
tys', co :: TcCoercion
co) <- (FamInstEnv, FamInstEnv)
-> TyCon -> [Type] -> Maybe (TyCon, [Type], TcCoercion)
tcLookupDataFamInst_maybe (FamInstEnv, FamInstEnv)
faminsts TyCon
tc [Type]
tys
      = ((Bag GlobalRdrElt, TcCoercion) -> (Bag GlobalRdrElt, TcCoercion))
-> NormaliseStepResult (Bag GlobalRdrElt, TcCoercion)
-> NormaliseStepResult (Bag GlobalRdrElt, TcCoercion)
forall ev1 ev2.
(ev1 -> ev2) -> NormaliseStepResult ev1 -> NormaliseStepResult ev2
mapStepResult (\(gres :: Bag GlobalRdrElt
gres, co1 :: TcCoercion
co1) -> (Bag GlobalRdrElt
gres, TcCoercion
co TcCoercion -> TcCoercion -> TcCoercion
`mkTransCo` TcCoercion
co1)) (NormaliseStepResult (Bag GlobalRdrElt, TcCoercion)
 -> NormaliseStepResult (Bag GlobalRdrElt, TcCoercion))
-> NormaliseStepResult (Bag GlobalRdrElt, TcCoercion)
-> NormaliseStepResult (Bag GlobalRdrElt, TcCoercion)
forall a b. (a -> b) -> a -> b
$
        NormaliseStepper (Bag GlobalRdrElt, TcCoercion)
unwrap_newtype RecTcChecker
rec_nts TyCon
tc' [Type]
tys'
      | Bool
otherwise = NormaliseStepResult (Bag GlobalRdrElt, TcCoercion)
forall ev. NormaliseStepResult ev
NS_Done

    unwrap_newtype :: NormaliseStepper (Bag GlobalRdrElt, TcCoercion)
unwrap_newtype rec_nts :: RecTcChecker
rec_nts tc :: TyCon
tc tys :: [Type]
tys
      | Just con :: DataCon
con <- TyCon -> Maybe DataCon
newTyConDataCon_maybe TyCon
tc
      , Just gre :: GlobalRdrElt
gre <- GlobalRdrEnv -> Name -> Maybe GlobalRdrElt
lookupGRE_Name GlobalRdrEnv
rdr_env (DataCon -> Name
dataConName DataCon
con)
           -- This is where we check that the
           -- data constructor is in scope
      = (TcCoercion -> (Bag GlobalRdrElt, TcCoercion))
-> NormaliseStepResult TcCoercion
-> NormaliseStepResult (Bag GlobalRdrElt, TcCoercion)
forall ev1 ev2.
(ev1 -> ev2) -> NormaliseStepResult ev1 -> NormaliseStepResult ev2
mapStepResult (\co :: TcCoercion
co -> (GlobalRdrElt -> Bag GlobalRdrElt
forall a. a -> Bag a
unitBag GlobalRdrElt
gre, TcCoercion
co)) (NormaliseStepResult TcCoercion
 -> NormaliseStepResult (Bag GlobalRdrElt, TcCoercion))
-> NormaliseStepResult TcCoercion
-> NormaliseStepResult (Bag GlobalRdrElt, TcCoercion)
forall a b. (a -> b) -> a -> b
$
        NormaliseStepper TcCoercion
unwrapNewTypeStepper RecTcChecker
rec_nts TyCon
tc [Type]
tys

      | Bool
otherwise
      = NormaliseStepResult (Bag GlobalRdrElt, TcCoercion)
forall ev. NormaliseStepResult ev
NS_Done

{-
************************************************************************
*                                                                      *
        Extending the family instance environment
*                                                                      *
************************************************************************
-}

-- Add new locally-defined family instances, checking consistency with
-- previous locally-defined family instances as well as all instances
-- available from imported modules. This requires loading all of our
-- imports that define family instances (if we haven't loaded them already).
tcExtendLocalFamInstEnv :: [FamInst] -> TcM a -> TcM a

-- If we weren't actually given any instances to add, then we don't want
-- to go to the bother of loading family instance module dependencies.
tcExtendLocalFamInstEnv :: [FamInst] -> TcM a -> TcM a
tcExtendLocalFamInstEnv [] thing_inside :: TcM a
thing_inside = TcM a
thing_inside

-- Otherwise proceed...
tcExtendLocalFamInstEnv fam_insts :: [FamInst]
fam_insts thing_inside :: TcM a
thing_inside
 = do { -- Load family-instance modules "below" this module, so that
        -- allLocalFamInst can check for consistency with them
        -- See Note [The type family instance consistency story]
        [FamInst] -> TcRn ()
loadDependentFamInstModules [FamInst]
fam_insts

        -- Now add the instances one by one
      ; TcGblEnv
env <- TcRnIf TcGblEnv TcLclEnv TcGblEnv
forall gbl lcl. TcRnIf gbl lcl gbl
getGblEnv
      ; (inst_env' :: FamInstEnv
inst_env', fam_insts' :: [FamInst]
fam_insts') <- ((FamInstEnv, [FamInst])
 -> FamInst
 -> IOEnv (Env TcGblEnv TcLclEnv) (FamInstEnv, [FamInst]))
-> (FamInstEnv, [FamInst])
-> [FamInst]
-> IOEnv (Env TcGblEnv TcLclEnv) (FamInstEnv, [FamInst])
forall (m :: * -> *) a b.
Monad m =>
(a -> b -> m a) -> a -> [b] -> m a
foldlM (FamInstEnv, [FamInst])
-> FamInst -> IOEnv (Env TcGblEnv TcLclEnv) (FamInstEnv, [FamInst])
addLocalFamInst
                                       (TcGblEnv -> FamInstEnv
tcg_fam_inst_env TcGblEnv
env, TcGblEnv -> [FamInst]
tcg_fam_insts TcGblEnv
env)
                                       [FamInst]
fam_insts

      ; let env' :: TcGblEnv
env' = TcGblEnv
env { tcg_fam_insts :: [FamInst]
tcg_fam_insts    = [FamInst]
fam_insts'
                       , tcg_fam_inst_env :: FamInstEnv
tcg_fam_inst_env = FamInstEnv
inst_env' }
      ; TcGblEnv -> TcM a -> TcM a
forall gbl lcl a. gbl -> TcRnIf gbl lcl a -> TcRnIf gbl lcl a
setGblEnv TcGblEnv
env' TcM a
thing_inside
      }

loadDependentFamInstModules :: [FamInst] -> TcM ()
-- Load family-instance modules "below" this module, so that
-- allLocalFamInst can check for consistency with them
-- See Note [The type family instance consistency story]
loadDependentFamInstModules :: [FamInst] -> TcRn ()
loadDependentFamInstModules fam_insts :: [FamInst]
fam_insts
 = do { TcGblEnv
env <- TcRnIf TcGblEnv TcLclEnv TcGblEnv
forall gbl lcl. TcRnIf gbl lcl gbl
getGblEnv
      ; let this_mod :: Module
this_mod = TcGblEnv -> Module
tcg_mod TcGblEnv
env
            imports :: ImportAvails
imports  = TcGblEnv -> ImportAvails
tcg_imports TcGblEnv
env

            want_module :: Module -> Bool
want_module mod :: Module
mod  -- See Note [Home package family instances]
              | Module
mod Module -> Module -> Bool
forall a. Eq a => a -> a -> Bool
== Module
this_mod = Bool
False
              | Bool
home_fams_only  = Module -> UnitId
moduleUnitId Module
mod UnitId -> UnitId -> Bool
forall a. Eq a => a -> a -> Bool
== Module -> UnitId
moduleUnitId Module
this_mod
              | Bool
otherwise       = Bool
True
            home_fams_only :: Bool
home_fams_only = (FamInst -> Bool) -> [FamInst] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (Module -> Name -> Bool
nameIsHomePackage Module
this_mod (Name -> Bool) -> (FamInst -> Name) -> FamInst -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FamInst -> Name
fi_fam) [FamInst]
fam_insts

      ; SDoc -> [Module] -> TcRn ()
loadModuleInterfaces (String -> SDoc
text "Loading family-instance modules") ([Module] -> TcRn ()) -> [Module] -> TcRn ()
forall a b. (a -> b) -> a -> b
$
        (Module -> Bool) -> [Module] -> [Module]
forall a. (a -> Bool) -> [a] -> [a]
filter Module -> Bool
want_module (ImportAvails -> [Module]
imp_finsts ImportAvails
imports) }

{- Note [Home package family instances]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Optimization: If we're only defining type family instances
for type families *defined in the home package*, then we
only have to load interface files that belong to the home
package. The reason is that there's no recursion between
packages, so modules in other packages can't possibly define
instances for our type families.

(Within the home package, we could import a module M that
imports us via an hs-boot file, and thereby defines an
instance of a type family defined in this module. So we can't
apply the same logic to avoid reading any interface files at
all, when we define an instances for type family defined in
the current module.
-}

-- Check that the proposed new instance is OK,
-- and then add it to the home inst env
-- This must be lazy in the fam_inst arguments, see Note [Lazy axiom match]
-- in FamInstEnv.hs
addLocalFamInst :: (FamInstEnv,[FamInst])
                -> FamInst
                -> TcM (FamInstEnv, [FamInst])
addLocalFamInst :: (FamInstEnv, [FamInst])
-> FamInst -> IOEnv (Env TcGblEnv TcLclEnv) (FamInstEnv, [FamInst])
addLocalFamInst (home_fie :: FamInstEnv
home_fie, my_fis :: [FamInst]
my_fis) fam_inst :: FamInst
fam_inst
        -- home_fie includes home package and this module
        -- my_fies is just the ones from this module
  = do { String -> SDoc -> TcRn ()
traceTc "addLocalFamInst" (FamInst -> SDoc
forall a. Outputable a => a -> SDoc
ppr FamInst
fam_inst)

           -- Unlike the case of class instances, don't override existing
           -- instances in GHCi; it's unsound. See #7102.

       ; Module
mod <- IOEnv (Env TcGblEnv TcLclEnv) Module
forall (m :: * -> *). HasModule m => m Module
getModule
       ; String -> SDoc -> TcRn ()
traceTc "alfi" (Module -> SDoc
forall a. Outputable a => a -> SDoc
ppr Module
mod)

           -- Fetch imported instances, so that we report
           -- overlaps correctly.
           -- Really we ought to only check consistency with
           -- those instances which are transitively imported
           -- by the current module, rather than every instance
           -- we've ever seen. Fixing this is part of #13102.
       ; ExternalPackageState
eps <- TcRnIf TcGblEnv TcLclEnv ExternalPackageState
forall gbl lcl. TcRnIf gbl lcl ExternalPackageState
getEps
       ; let inst_envs :: (FamInstEnv, FamInstEnv)
inst_envs = (ExternalPackageState -> FamInstEnv
eps_fam_inst_env ExternalPackageState
eps, FamInstEnv
home_fie)
             home_fie' :: FamInstEnv
home_fie' = FamInstEnv -> FamInst -> FamInstEnv
extendFamInstEnv FamInstEnv
home_fie FamInst
fam_inst

           -- Check for conflicting instance decls and injectivity violations
       ; Bool
no_conflict    <- (FamInstEnv, FamInstEnv)
-> FamInst -> IOEnv (Env TcGblEnv TcLclEnv) Bool
checkForConflicts            (FamInstEnv, FamInstEnv)
inst_envs FamInst
fam_inst
       ; Bool
injectivity_ok <- (FamInstEnv, FamInstEnv)
-> FamInst -> IOEnv (Env TcGblEnv TcLclEnv) Bool
checkForInjectivityConflicts (FamInstEnv, FamInstEnv)
inst_envs FamInst
fam_inst

       ; if Bool
no_conflict Bool -> Bool -> Bool
&& Bool
injectivity_ok then
            (FamInstEnv, [FamInst])
-> IOEnv (Env TcGblEnv TcLclEnv) (FamInstEnv, [FamInst])
forall (m :: * -> *) a. Monad m => a -> m a
return (FamInstEnv
home_fie', FamInst
fam_inst FamInst -> [FamInst] -> [FamInst]
forall a. a -> [a] -> [a]
: [FamInst]
my_fis)
         else
            (FamInstEnv, [FamInst])
-> IOEnv (Env TcGblEnv TcLclEnv) (FamInstEnv, [FamInst])
forall (m :: * -> *) a. Monad m => a -> m a
return (FamInstEnv
home_fie,  [FamInst]
my_fis) }

{-
************************************************************************
*                                                                      *
        Checking an instance against conflicts with an instance env
*                                                                      *
************************************************************************

Check whether a single family instance conflicts with those in two instance
environments (one for the EPS and one for the HPT).
-}

checkForConflicts :: FamInstEnvs -> FamInst -> TcM Bool
checkForConflicts :: (FamInstEnv, FamInstEnv)
-> FamInst -> IOEnv (Env TcGblEnv TcLclEnv) Bool
checkForConflicts inst_envs :: (FamInstEnv, FamInstEnv)
inst_envs fam_inst :: FamInst
fam_inst
  = do { let conflicts :: [FamInstMatch]
conflicts = (FamInstEnv, FamInstEnv) -> FamInst -> [FamInstMatch]
lookupFamInstEnvConflicts (FamInstEnv, FamInstEnv)
inst_envs FamInst
fam_inst
       ; String -> SDoc -> TcRn ()
traceTc "checkForConflicts" (SDoc -> TcRn ()) -> SDoc -> TcRn ()
forall a b. (a -> b) -> a -> b
$
         [SDoc] -> SDoc
vcat [ [FamInst] -> SDoc
forall a. Outputable a => a -> SDoc
ppr ((FamInstMatch -> FamInst) -> [FamInstMatch] -> [FamInst]
forall a b. (a -> b) -> [a] -> [b]
map FamInstMatch -> FamInst
fim_instance [FamInstMatch]
conflicts)
              , FamInst -> SDoc
forall a. Outputable a => a -> SDoc
ppr FamInst
fam_inst
              -- , ppr inst_envs
         ]
       ; FamInst -> [FamInstMatch] -> TcRn ()
reportConflictInstErr FamInst
fam_inst [FamInstMatch]
conflicts
       ; Bool -> IOEnv (Env TcGblEnv TcLclEnv) Bool
forall (m :: * -> *) a. Monad m => a -> m a
return ([FamInstMatch] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [FamInstMatch]
conflicts) }

-- | Check whether a new open type family equation can be added without
-- violating injectivity annotation supplied by the user. Returns True when
-- this is possible and False if adding this equation would violate injectivity
-- annotation.
checkForInjectivityConflicts :: FamInstEnvs -> FamInst -> TcM Bool
checkForInjectivityConflicts :: (FamInstEnv, FamInstEnv)
-> FamInst -> IOEnv (Env TcGblEnv TcLclEnv) Bool
checkForInjectivityConflicts instEnvs :: (FamInstEnv, FamInstEnv)
instEnvs famInst :: FamInst
famInst
    | TyCon -> Bool
isTypeFamilyTyCon TyCon
tycon
    -- type family is injective in at least one argument
    , Injective inj :: [Bool]
inj <- TyCon -> Injectivity
tyConInjectivityInfo TyCon
tycon = do
    { let axiom :: CoAxBranch
axiom = CoAxiom Unbranched -> CoAxBranch
coAxiomSingleBranch CoAxiom Unbranched
fi_ax
          conflicts :: [CoAxBranch]
conflicts = [Bool] -> (FamInstEnv, FamInstEnv) -> FamInst -> [CoAxBranch]
lookupFamInstEnvInjectivityConflicts [Bool]
inj (FamInstEnv, FamInstEnv)
instEnvs FamInst
famInst
          -- see Note [Verifying injectivity annotation] in FamInstEnv
          errs :: [(SDoc, SrcSpan)]
errs = CoAxiom Unbranched
-> CoAxBranch -> [Bool] -> [CoAxBranch] -> [(SDoc, SrcSpan)]
forall (br :: BranchFlag).
CoAxiom br
-> CoAxBranch -> [Bool] -> [CoAxBranch] -> [(SDoc, SrcSpan)]
makeInjectivityErrors CoAxiom Unbranched
fi_ax CoAxBranch
axiom [Bool]
inj [CoAxBranch]
conflicts
    ; ((SDoc, SrcSpan) -> TcRn ()) -> [(SDoc, SrcSpan)] -> TcRn ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (\(err :: SDoc
err, span :: SrcSpan
span) -> SrcSpan -> TcRn () -> TcRn ()
forall a. SrcSpan -> TcRn a -> TcRn a
setSrcSpan SrcSpan
span (TcRn () -> TcRn ()) -> TcRn () -> TcRn ()
forall a b. (a -> b) -> a -> b
$ SDoc -> TcRn ()
addErr SDoc
err) [(SDoc, SrcSpan)]
errs
    ; Bool -> IOEnv (Env TcGblEnv TcLclEnv) Bool
forall (m :: * -> *) a. Monad m => a -> m a
return ([(SDoc, SrcSpan)] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [(SDoc, SrcSpan)]
errs)
    }

    -- if there was no injectivity annotation or tycon does not represent a
    -- type family we report no conflicts
    | Bool
otherwise = Bool -> IOEnv (Env TcGblEnv TcLclEnv) Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
    where tycon :: TyCon
tycon = FamInst -> TyCon
famInstTyCon FamInst
famInst
          fi_ax :: CoAxiom Unbranched
fi_ax = FamInst -> CoAxiom Unbranched
fi_axiom FamInst
famInst

-- | Build a list of injectivity errors together with their source locations.
makeInjectivityErrors
   :: CoAxiom br   -- ^ Type family for which we generate errors
   -> CoAxBranch   -- ^ Currently checked equation (represented by axiom)
   -> [Bool]       -- ^ Injectivity annotation
   -> [CoAxBranch] -- ^ List of injectivity conflicts
   -> [(SDoc, SrcSpan)]
makeInjectivityErrors :: CoAxiom br
-> CoAxBranch -> [Bool] -> [CoAxBranch] -> [(SDoc, SrcSpan)]
makeInjectivityErrors fi_ax :: CoAxiom br
fi_ax axiom :: CoAxBranch
axiom inj :: [Bool]
inj conflicts :: [CoAxBranch]
conflicts
  = ASSERT2( any id inj, text "No injective type variables" )
    let lhs :: [Type]
lhs             = CoAxBranch -> [Type]
coAxBranchLHS CoAxBranch
axiom
        rhs :: Type
rhs             = CoAxBranch -> Type
coAxBranchRHS CoAxBranch
axiom
        fam_tc :: TyCon
fam_tc          = CoAxiom br -> TyCon
forall (br :: BranchFlag). CoAxiom br -> TyCon
coAxiomTyCon CoAxiom br
fi_ax
        are_conflicts :: Bool
are_conflicts   = Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ [CoAxBranch] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [CoAxBranch]
conflicts
        unused_inj_tvs :: Pair TyCoVarSet
unused_inj_tvs  = TyCon -> [Bool] -> [Type] -> Type -> Pair TyCoVarSet
unusedInjTvsInRHS TyCon
fam_tc [Bool]
inj [Type]
lhs Type
rhs
        inj_tvs_unused :: Bool
inj_tvs_unused  = Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ Pair Bool -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
and (TyCoVarSet -> Bool
isEmptyVarSet (TyCoVarSet -> Bool) -> Pair TyCoVarSet -> Pair Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Pair TyCoVarSet
unused_inj_tvs)
        tf_headed :: Bool
tf_headed       = Type -> Bool
isTFHeaded Type
rhs
        bare_variables :: [Type]
bare_variables  = [Type] -> Type -> [Type]
bareTvInRHSViolated [Type]
lhs Type
rhs
        wrong_bare_rhs :: Bool
wrong_bare_rhs  = Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ [Type] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Type]
bare_variables

        err_builder :: SDoc -> [CoAxBranch] -> (SDoc, SrcSpan)
err_builder herald :: SDoc
herald eqns :: [CoAxBranch]
eqns
                        = ( SDoc -> Int -> SDoc -> SDoc
hang SDoc
herald
                               2 ([SDoc] -> SDoc
vcat ((CoAxBranch -> SDoc) -> [CoAxBranch] -> [SDoc]
forall a b. (a -> b) -> [a] -> [b]
map (TyCon -> CoAxBranch -> SDoc
pprCoAxBranchUser TyCon
fam_tc) [CoAxBranch]
eqns))
                          , CoAxBranch -> SrcSpan
coAxBranchSpan ([CoAxBranch] -> CoAxBranch
forall a. [a] -> a
head [CoAxBranch]
eqns) )
        errorIf :: Bool
-> ((SDoc -> [CoAxBranch] -> (SDoc, SrcSpan))
    -> CoAxBranch -> (SDoc, SrcSpan))
-> [(SDoc, SrcSpan)]
errorIf p :: Bool
p f :: (SDoc -> [CoAxBranch] -> (SDoc, SrcSpan))
-> CoAxBranch -> (SDoc, SrcSpan)
f     = if Bool
p then [(SDoc -> [CoAxBranch] -> (SDoc, SrcSpan))
-> CoAxBranch -> (SDoc, SrcSpan)
f SDoc -> [CoAxBranch] -> (SDoc, SrcSpan)
err_builder CoAxBranch
axiom] else []
     in    Bool
-> ((SDoc -> [CoAxBranch] -> (SDoc, SrcSpan))
    -> CoAxBranch -> (SDoc, SrcSpan))
-> [(SDoc, SrcSpan)]
errorIf Bool
are_conflicts  ([CoAxBranch]
-> (SDoc -> [CoAxBranch] -> (SDoc, SrcSpan))
-> CoAxBranch
-> (SDoc, SrcSpan)
conflictInjInstErr     [CoAxBranch]
conflicts     )
        [(SDoc, SrcSpan)] -> [(SDoc, SrcSpan)] -> [(SDoc, SrcSpan)]
forall a. [a] -> [a] -> [a]
++ Bool
-> ((SDoc -> [CoAxBranch] -> (SDoc, SrcSpan))
    -> CoAxBranch -> (SDoc, SrcSpan))
-> [(SDoc, SrcSpan)]
errorIf Bool
inj_tvs_unused (Pair TyCoVarSet
-> (SDoc -> [CoAxBranch] -> (SDoc, SrcSpan))
-> CoAxBranch
-> (SDoc, SrcSpan)
unusedInjectiveVarsErr Pair TyCoVarSet
unused_inj_tvs)
        [(SDoc, SrcSpan)] -> [(SDoc, SrcSpan)] -> [(SDoc, SrcSpan)]
forall a. [a] -> [a] -> [a]
++ Bool
-> ((SDoc -> [CoAxBranch] -> (SDoc, SrcSpan))
    -> CoAxBranch -> (SDoc, SrcSpan))
-> [(SDoc, SrcSpan)]
errorIf Bool
tf_headed       (SDoc -> [CoAxBranch] -> (SDoc, SrcSpan))
-> CoAxBranch -> (SDoc, SrcSpan)
tfHeadedErr
        [(SDoc, SrcSpan)] -> [(SDoc, SrcSpan)] -> [(SDoc, SrcSpan)]
forall a. [a] -> [a] -> [a]
++ Bool
-> ((SDoc -> [CoAxBranch] -> (SDoc, SrcSpan))
    -> CoAxBranch -> (SDoc, SrcSpan))
-> [(SDoc, SrcSpan)]
errorIf Bool
wrong_bare_rhs ([Type]
-> (SDoc -> [CoAxBranch] -> (SDoc, SrcSpan))
-> CoAxBranch
-> (SDoc, SrcSpan)
bareVariableInRHSErr   [Type]
bare_variables)


-- | Return a list of type variables that the function is injective in and that
-- do not appear on injective positions in the RHS of a family instance
-- declaration. The returned Pair includes invisible vars followed by visible ones
unusedInjTvsInRHS :: TyCon -> [Bool] -> [Type] -> Type -> Pair TyVarSet
-- INVARIANT: [Bool] list contains at least one True value
-- See Note [Verifying injectivity annotation]. This function implements fourth
-- check described there.
-- In theory, instead of implementing this whole check in this way, we could
-- attempt to unify equation with itself.  We would reject exactly the same
-- equations but this method gives us more precise error messages by returning
-- precise names of variables that are not mentioned in the RHS.
unusedInjTvsInRHS :: TyCon -> [Bool] -> [Type] -> Type -> Pair TyCoVarSet
unusedInjTvsInRHS tycon :: TyCon
tycon injList :: [Bool]
injList lhs :: [Type]
lhs rhs :: Type
rhs =
  (TyCoVarSet -> TyCoVarSet -> TyCoVarSet
`minusVarSet` TyCoVarSet
injRhsVars) (TyCoVarSet -> TyCoVarSet) -> Pair TyCoVarSet -> Pair TyCoVarSet
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Pair TyCoVarSet
injLHSVars
    where
      inj_pairs :: [(Type, ArgFlag)]
      -- All the injective arguments, paired with their visibility
      inj_pairs :: [(Type, ArgFlag)]
inj_pairs = ASSERT2( injList `equalLength` lhs
                         , ppr tycon $$ ppr injList $$ ppr lhs )
                  [Bool] -> [(Type, ArgFlag)] -> [(Type, ArgFlag)]
forall a. [Bool] -> [a] -> [a]
filterByList [Bool]
injList ([Type]
lhs [Type] -> [ArgFlag] -> [(Type, ArgFlag)]
forall a b. [a] -> [b] -> [(a, b)]
`zip` TyCon -> [Type] -> [ArgFlag]
tyConArgFlags TyCon
tycon [Type]
lhs)

      -- set of type and kind variables in which type family is injective
      invis_lhs, vis_lhs :: [Type]
      (invis_lhs :: [Type]
invis_lhs, vis_lhs :: [Type]
vis_lhs) = [(Type, ArgFlag)] -> ([Type], [Type])
forall a. [(a, ArgFlag)] -> ([a], [a])
partitionInvisibles [(Type, ArgFlag)]
inj_pairs

      invis_vars :: TyCoVarSet
invis_vars = [Type] -> TyCoVarSet
tyCoVarsOfTypes [Type]
invis_lhs
      Pair invis_vars' :: TyCoVarSet
invis_vars' vis_vars :: TyCoVarSet
vis_vars = [Type] -> Pair TyCoVarSet
splitVisVarsOfTypes [Type]
vis_lhs
      injLHSVars :: Pair TyCoVarSet
injLHSVars
        = TyCoVarSet -> TyCoVarSet -> Pair TyCoVarSet
forall a. a -> a -> Pair a
Pair (TyCoVarSet
invis_vars TyCoVarSet -> TyCoVarSet -> TyCoVarSet
`minusVarSet` TyCoVarSet
vis_vars TyCoVarSet -> TyCoVarSet -> TyCoVarSet
`unionVarSet` TyCoVarSet
invis_vars')
               TyCoVarSet
vis_vars

      -- set of type variables appearing in the RHS on an injective position.
      -- For all returned variables we assume their associated kind variables
      -- also appear in the RHS.
      injRhsVars :: TyCoVarSet
injRhsVars = Type -> TyCoVarSet
injTyVarsOfType Type
rhs

injTyVarsOfType :: TcTauType -> TcTyVarSet
-- Collect all type variables that are either arguments to a type
--   constructor or to /injective/ type families.
-- Determining the overall type determines thes variables
--
-- E.g.   Suppose F is injective in its second arg, but not its first
--        then injVarOfType (Either a (F [b] (a,c))) = {a,c}
--        Determining the overall type determines a,c but not b.
injTyVarsOfType :: Type -> TyCoVarSet
injTyVarsOfType ty :: Type
ty
  | Just ty' :: Type
ty' <- Type -> Maybe Type
coreView Type
ty -- #12430
  = Type -> TyCoVarSet
injTyVarsOfType Type
ty'
injTyVarsOfType (TyVarTy v :: TyVar
v)
  = TyVar -> TyCoVarSet
unitVarSet TyVar
v TyCoVarSet -> TyCoVarSet -> TyCoVarSet
`unionVarSet` Type -> TyCoVarSet
injTyVarsOfType (TyVar -> Type
tyVarKind TyVar
v)
injTyVarsOfType (TyConApp tc :: TyCon
tc tys :: [Type]
tys)
  | TyCon -> Bool
isTypeFamilyTyCon TyCon
tc
   = case TyCon -> Injectivity
tyConInjectivityInfo TyCon
tc of
        NotInjective  -> TyCoVarSet
emptyVarSet
        Injective inj :: [Bool]
inj -> [Type] -> TyCoVarSet
injTyVarsOfTypes ([Bool] -> [Type] -> [Type]
forall a. [Bool] -> [a] -> [a]
filterByList [Bool]
inj [Type]
tys)
  | Bool
otherwise
  = [Type] -> TyCoVarSet
injTyVarsOfTypes [Type]
tys
injTyVarsOfType (LitTy {})
  = TyCoVarSet
emptyVarSet
injTyVarsOfType (FunTy arg :: Type
arg res :: Type
res)
  = Type -> TyCoVarSet
injTyVarsOfType Type
arg TyCoVarSet -> TyCoVarSet -> TyCoVarSet
`unionVarSet` Type -> TyCoVarSet
injTyVarsOfType Type
res
injTyVarsOfType (AppTy fun :: Type
fun arg :: Type
arg)
  = Type -> TyCoVarSet
injTyVarsOfType Type
fun TyCoVarSet -> TyCoVarSet -> TyCoVarSet
`unionVarSet` Type -> TyCoVarSet
injTyVarsOfType Type
arg
-- No forall types in the RHS of a type family
injTyVarsOfType (CastTy ty :: Type
ty _)   = Type -> TyCoVarSet
injTyVarsOfType Type
ty
injTyVarsOfType (CoercionTy {}) = TyCoVarSet
emptyVarSet
injTyVarsOfType (ForAllTy {})    =
    String -> TyCoVarSet
forall a. String -> a
panic "unusedInjTvsInRHS.injTyVarsOfType"

injTyVarsOfTypes :: [Type] -> VarSet
injTyVarsOfTypes :: [Type] -> TyCoVarSet
injTyVarsOfTypes tys :: [Type]
tys = (Type -> TyCoVarSet) -> [Type] -> TyCoVarSet
forall a. (a -> TyCoVarSet) -> [a] -> TyCoVarSet
mapUnionVarSet Type -> TyCoVarSet
injTyVarsOfType [Type]
tys

-- | Is type headed by a type family application?
isTFHeaded :: Type -> Bool
-- See Note [Verifying injectivity annotation]. This function implements third
-- check described there.
isTFHeaded :: Type -> Bool
isTFHeaded ty :: Type
ty | Just ty' :: Type
ty' <- Type -> Maybe Type
coreView Type
ty
              = Type -> Bool
isTFHeaded Type
ty'
isTFHeaded ty :: Type
ty | (TyConApp tc :: TyCon
tc args :: [Type]
args) <- Type
ty
              , TyCon -> Bool
isTypeFamilyTyCon TyCon
tc
              = [Type]
args [Type] -> Int -> Bool
forall a. [a] -> Int -> Bool
`lengthIs` TyCon -> Int
tyConArity TyCon
tc
isTFHeaded _  = Bool
False


-- | If a RHS is a bare type variable return a set of LHS patterns that are not
-- bare type variables.
bareTvInRHSViolated :: [Type] -> Type -> [Type]
-- See Note [Verifying injectivity annotation]. This function implements second
-- check described there.
bareTvInRHSViolated :: [Type] -> Type -> [Type]
bareTvInRHSViolated pats :: [Type]
pats rhs :: Type
rhs | Type -> Bool
isTyVarTy Type
rhs
   = (Type -> Bool) -> [Type] -> [Type]
forall a. (a -> Bool) -> [a] -> [a]
filter (Bool -> Bool
not (Bool -> Bool) -> (Type -> Bool) -> Type -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Type -> Bool
isTyVarTy) [Type]
pats
bareTvInRHSViolated _ _ = []


-- | Type of functions that use error message and a list of axioms to build full
-- error message (with a source location) for injective type families.
type InjErrorBuilder = SDoc -> [CoAxBranch] -> (SDoc, SrcSpan)

-- | Build injecivity error herald common to all injectivity errors.
injectivityErrorHerald :: Bool -> SDoc
injectivityErrorHerald :: Bool -> SDoc
injectivityErrorHerald isSingular :: Bool
isSingular =
  String -> SDoc
text "Type family equation" SDoc -> SDoc -> SDoc
<> Bool -> SDoc
s Bool
isSingular SDoc -> SDoc -> SDoc
<+> String -> SDoc
text "violate" SDoc -> SDoc -> SDoc
<>
  Bool -> SDoc
s (Bool -> Bool
not Bool
isSingular) SDoc -> SDoc -> SDoc
<+> String -> SDoc
text "injectivity annotation" SDoc -> SDoc -> SDoc
<>
  if Bool
isSingular then SDoc
dot else SDoc
colon
  -- Above is an ugly hack.  We want this: "sentence. herald:" (note the dot and
  -- colon).  But if herald is empty we want "sentence:" (note the colon).  We
  -- can't test herald for emptiness so we rely on the fact that herald is empty
  -- only when isSingular is False.  If herald is non empty it must end with a
  -- colon.
    where
      s :: Bool -> SDoc
s False = String -> SDoc
text "s"
      s True  = SDoc
empty

-- | Build error message for a pair of equations violating an injectivity
-- annotation.
conflictInjInstErr :: [CoAxBranch] -> InjErrorBuilder -> CoAxBranch
                   -> (SDoc, SrcSpan)
conflictInjInstErr :: [CoAxBranch]
-> (SDoc -> [CoAxBranch] -> (SDoc, SrcSpan))
-> CoAxBranch
-> (SDoc, SrcSpan)
conflictInjInstErr conflictingEqns :: [CoAxBranch]
conflictingEqns errorBuilder :: SDoc -> [CoAxBranch] -> (SDoc, SrcSpan)
errorBuilder tyfamEqn :: CoAxBranch
tyfamEqn
  | confEqn :: CoAxBranch
confEqn : _ <- [CoAxBranch]
conflictingEqns
  = SDoc -> [CoAxBranch] -> (SDoc, SrcSpan)
errorBuilder (Bool -> SDoc
injectivityErrorHerald Bool
False) [CoAxBranch
confEqn, CoAxBranch
tyfamEqn]
  | Bool
otherwise
  = String -> (SDoc, SrcSpan)
forall a. String -> a
panic "conflictInjInstErr"

-- | Build error message for equation with injective type variables unused in
-- the RHS.
unusedInjectiveVarsErr :: Pair TyVarSet -> InjErrorBuilder -> CoAxBranch
                       -> (SDoc, SrcSpan)
unusedInjectiveVarsErr :: Pair TyCoVarSet
-> (SDoc -> [CoAxBranch] -> (SDoc, SrcSpan))
-> CoAxBranch
-> (SDoc, SrcSpan)
unusedInjectiveVarsErr (Pair invis_vars :: TyCoVarSet
invis_vars vis_vars :: TyCoVarSet
vis_vars) errorBuilder :: SDoc -> [CoAxBranch] -> (SDoc, SrcSpan)
errorBuilder tyfamEqn :: CoAxBranch
tyfamEqn
  = let (doc :: SDoc
doc, loc :: SrcSpan
loc) = SDoc -> [CoAxBranch] -> (SDoc, SrcSpan)
errorBuilder (Bool -> SDoc
injectivityErrorHerald Bool
True SDoc -> SDoc -> SDoc
$$ SDoc
msg)
                                  [CoAxBranch
tyfamEqn]
    in (Bool -> SDoc -> SDoc
pprWithExplicitKindsWhen Bool
has_kinds SDoc
doc, SrcSpan
loc)
    where
      tvs :: TyCoVarSet
tvs = TyCoVarSet
invis_vars TyCoVarSet -> TyCoVarSet -> TyCoVarSet
`unionVarSet` TyCoVarSet
vis_vars
      has_types :: Bool
has_types = Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ TyCoVarSet -> Bool
isEmptyVarSet TyCoVarSet
vis_vars
      has_kinds :: Bool
has_kinds = Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ TyCoVarSet -> Bool
isEmptyVarSet TyCoVarSet
invis_vars

      doc :: SDoc
doc = [SDoc] -> SDoc
sep [ SDoc
what SDoc -> SDoc -> SDoc
<+> String -> SDoc
text "variable" SDoc -> SDoc -> SDoc
<>
                  TyCoVarSet -> SDoc
pluralVarSet TyCoVarSet
tvs SDoc -> SDoc -> SDoc
<+> TyCoVarSet -> ([TyVar] -> SDoc) -> SDoc
pprVarSet TyCoVarSet
tvs ([TyVar] -> SDoc
forall a. Outputable a => [a] -> SDoc
pprQuotedList ([TyVar] -> SDoc) -> ([TyVar] -> [TyVar]) -> [TyVar] -> SDoc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [TyVar] -> [TyVar]
scopedSort)
                , String -> SDoc
text "cannot be inferred from the right-hand side." ]
      what :: SDoc
what = case (Bool
has_types, Bool
has_kinds) of
               (True, True)   -> String -> SDoc
text "Type and kind"
               (True, False)  -> String -> SDoc
text "Type"
               (False, True)  -> String -> SDoc
text "Kind"
               (False, False) -> String -> SDoc -> SDoc
forall a. HasCallStack => String -> SDoc -> a
pprPanic "mkUnusedInjectiveVarsErr" (SDoc -> SDoc) -> SDoc -> SDoc
forall a b. (a -> b) -> a -> b
$ TyCoVarSet -> SDoc
forall a. Outputable a => a -> SDoc
ppr TyCoVarSet
tvs
      msg :: SDoc
msg = SDoc
doc SDoc -> SDoc -> SDoc
$$ String -> SDoc
text "In the type family equation:"

-- | Build error message for equation that has a type family call at the top
-- level of RHS
tfHeadedErr :: InjErrorBuilder -> CoAxBranch
            -> (SDoc, SrcSpan)
tfHeadedErr :: (SDoc -> [CoAxBranch] -> (SDoc, SrcSpan))
-> CoAxBranch -> (SDoc, SrcSpan)
tfHeadedErr errorBuilder :: SDoc -> [CoAxBranch] -> (SDoc, SrcSpan)
errorBuilder famInst :: CoAxBranch
famInst
  = SDoc -> [CoAxBranch] -> (SDoc, SrcSpan)
errorBuilder (Bool -> SDoc
injectivityErrorHerald Bool
True SDoc -> SDoc -> SDoc
$$
                  String -> SDoc
text "RHS of injective type family equation cannot" SDoc -> SDoc -> SDoc
<+>
                  String -> SDoc
text "be a type family:") [CoAxBranch
famInst]

-- | Build error message for equation that has a bare type variable in the RHS
-- but LHS pattern is not a bare type variable.
bareVariableInRHSErr :: [Type] -> InjErrorBuilder -> CoAxBranch
                     -> (SDoc, SrcSpan)
bareVariableInRHSErr :: [Type]
-> (SDoc -> [CoAxBranch] -> (SDoc, SrcSpan))
-> CoAxBranch
-> (SDoc, SrcSpan)
bareVariableInRHSErr tys :: [Type]
tys errorBuilder :: SDoc -> [CoAxBranch] -> (SDoc, SrcSpan)
errorBuilder famInst :: CoAxBranch
famInst
  = SDoc -> [CoAxBranch] -> (SDoc, SrcSpan)
errorBuilder (Bool -> SDoc
injectivityErrorHerald Bool
True SDoc -> SDoc -> SDoc
$$
                  String -> SDoc
text "RHS of injective type family equation is a bare" SDoc -> SDoc -> SDoc
<+>
                  String -> SDoc
text "type variable" SDoc -> SDoc -> SDoc
$$
                  String -> SDoc
text "but these LHS type and kind patterns are not bare" SDoc -> SDoc -> SDoc
<+>
                  String -> SDoc
text "variables:" SDoc -> SDoc -> SDoc
<+> [Type] -> SDoc
forall a. Outputable a => [a] -> SDoc
pprQuotedList [Type]
tys) [CoAxBranch
famInst]


reportConflictInstErr :: FamInst -> [FamInstMatch] -> TcRn ()
reportConflictInstErr :: FamInst -> [FamInstMatch] -> TcRn ()
reportConflictInstErr _ []
  = () -> TcRn ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()  -- No conflicts
reportConflictInstErr fam_inst :: FamInst
fam_inst (match1 :: FamInstMatch
match1 : _)
  | FamInstMatch { fim_instance :: FamInstMatch -> FamInst
fim_instance = FamInst
conf_inst } <- FamInstMatch
match1
  , let sorted :: [FamInst]
sorted  = (FamInst -> SrcLoc) -> [FamInst] -> [FamInst]
forall b a. Ord b => (a -> b) -> [a] -> [a]
sortWith FamInst -> SrcLoc
getSpan [FamInst
fam_inst, FamInst
conf_inst]
        fi1 :: FamInst
fi1     = [FamInst] -> FamInst
forall a. [a] -> a
head [FamInst]
sorted
        span :: SrcSpan
span    = CoAxBranch -> SrcSpan
coAxBranchSpan (CoAxiom Unbranched -> CoAxBranch
coAxiomSingleBranch (FamInst -> CoAxiom Unbranched
famInstAxiom FamInst
fi1))
  = SrcSpan -> TcRn () -> TcRn ()
forall a. SrcSpan -> TcRn a -> TcRn a
setSrcSpan SrcSpan
span (TcRn () -> TcRn ()) -> TcRn () -> TcRn ()
forall a b. (a -> b) -> a -> b
$ SDoc -> TcRn ()
addErr (SDoc -> TcRn ()) -> SDoc -> TcRn ()
forall a b. (a -> b) -> a -> b
$
    SDoc -> Int -> SDoc -> SDoc
hang (String -> SDoc
text "Conflicting family instance declarations:")
       2 ([SDoc] -> SDoc
vcat [ TyCon -> CoAxBranch -> SDoc
pprCoAxBranchUser (CoAxiom Unbranched -> TyCon
forall (br :: BranchFlag). CoAxiom br -> TyCon
coAxiomTyCon CoAxiom Unbranched
ax) (CoAxiom Unbranched -> CoAxBranch
coAxiomSingleBranch CoAxiom Unbranched
ax)
               | FamInst
fi <- [FamInst]
sorted
               , let ax :: CoAxiom Unbranched
ax = FamInst -> CoAxiom Unbranched
famInstAxiom FamInst
fi ])
 where
   getSpan :: FamInst -> SrcLoc
getSpan = CoAxiom Unbranched -> SrcLoc
forall a. NamedThing a => a -> SrcLoc
getSrcLoc (CoAxiom Unbranched -> SrcLoc)
-> (FamInst -> CoAxiom Unbranched) -> FamInst -> SrcLoc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FamInst -> CoAxiom Unbranched
famInstAxiom
   -- The sortWith just arranges that instances are dislayed in order
   -- of source location, which reduced wobbling in error messages,
   -- and is better for users

tcGetFamInstEnvs :: TcM FamInstEnvs
-- Gets both the external-package inst-env
-- and the home-pkg inst env (includes module being compiled)
tcGetFamInstEnvs :: TcM (FamInstEnv, FamInstEnv)
tcGetFamInstEnvs
  = do { ExternalPackageState
eps <- TcRnIf TcGblEnv TcLclEnv ExternalPackageState
forall gbl lcl. TcRnIf gbl lcl ExternalPackageState
getEps; TcGblEnv
env <- TcRnIf TcGblEnv TcLclEnv TcGblEnv
forall gbl lcl. TcRnIf gbl lcl gbl
getGblEnv
       ; (FamInstEnv, FamInstEnv) -> TcM (FamInstEnv, FamInstEnv)
forall (m :: * -> *) a. Monad m => a -> m a
return (ExternalPackageState -> FamInstEnv
eps_fam_inst_env ExternalPackageState
eps, TcGblEnv -> FamInstEnv
tcg_fam_inst_env TcGblEnv
env) }