{-# LANGUAGE GADTs, ViewPatterns #-}

-- | The @FamInst@ type: family instance heads
module GHC.Tc.Instance.Family (
        FamInstEnvs, tcGetFamInstEnvs,
        checkFamInstConsistency, tcExtendLocalFamInstEnv,
        tcLookupDataFamInst, tcLookupDataFamInst_maybe,
        tcInstNewTyCon_maybe, tcTopNormaliseNewTypeTF_maybe,

        -- * Injectivity
        reportInjectivityErrors, reportConflictingInjectivityErrs
    ) where

import GHC.Prelude

import GHC.Driver.DynFlags
import GHC.Driver.Env

import GHC.Core.FamInstEnv
import GHC.Core.Coercion
import GHC.Core.TyCon
import GHC.Core.Coercion.Axiom
import GHC.Core.DataCon ( dataConName )
import GHC.Core.TyCo.Rep
import GHC.Core.TyCo.FVs

import GHC.Iface.Load

import GHC.Tc.Errors.Types
import GHC.Tc.Types.Evidence
import GHC.Tc.Utils.Monad
import GHC.Tc.Utils.TcType

import GHC.Unit.External
import GHC.Unit.Module
import GHC.Unit.Module.ModIface
import GHC.Unit.Module.ModDetails
import GHC.Unit.Module.Deps
import GHC.Unit.Home.ModInfo

import GHC.Types.SrcLoc as SrcLoc
import GHC.Types.Name.Reader
import GHC.Types.Name
import GHC.Types.Var.Set

import GHC.Utils.Outputable
import GHC.Utils.Misc
import GHC.Utils.Panic
import GHC.Utils.FV

import GHC.Data.Bag( Bag, unionBags, unitBag )
import GHC.Data.Maybe

import Control.Monad
import Data.List.NonEmpty ( NonEmpty(..) )
import qualified Data.List.NonEmpty as NE
import Data.Function ( on )

import qualified GHC.LanguageExtensions  as LangExt
import GHC.Unit.Env (unitEnv_hpts)

{- 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 GHC.Iface.Load.
-}

{-
************************************************************************
*                                                                      *
        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 `GHC.Driver.Env.dep_finsts' are consistent.)

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.
-}

-- 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] -> TcM ()
checkFamInstConsistency [Module]
directlyImpMods
  = do { (eps, hug) <- TcRnIf TcGblEnv TcLclEnv (ExternalPackageState, HomeUnitGraph)
forall gbl lcl.
TcRnIf gbl lcl (ExternalPackageState, HomeUnitGraph)
getEpsAndHug
       ; traceTc "checkFamInstConsistency" (ppr directlyImpMods)
       ; let { -- Fetch the iface of a given module.  Must succeed as
               -- all directly imported modules must already have been loaded.
               modIface Module
mod =
                 case HomeUnitGraph -> PackageIfaceTable -> Module -> Maybe ModIface
lookupIfaceByModule HomeUnitGraph
hug (ExternalPackageState -> PackageIfaceTable
eps_PIT ExternalPackageState
eps) Module
mod of
                   Maybe ModIface
Nothing    -> String -> SDoc -> ModIface
forall a. String -> SDoc -> a
panicDoc String
"FamInst.checkFamInstConsistency"
                                          (Module -> SDoc
forall a. Outputable a => a -> SDoc
ppr Module
mod SDoc -> SDoc -> SDoc
forall doc. IsDoc doc => doc -> doc -> doc
$$ HomeUnitGraph -> SDoc
forall a. Outputable a => a -> SDoc
ppr HomeUnitGraph
hug)
                   Just 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
mod =
                 if ModIfaceBackend -> WhetherHasFamInst
mi_finsts (ModIface -> IfaceBackendExts 'ModIfaceFinal
forall (phase :: ModIfacePhase).
ModIface_ phase -> IfaceBackendExts phase
mi_final_exts (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
forall (phase :: ModIfacePhase). ModIface_ phase -> 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     = ModIface -> Module
forall (phase :: ModIfacePhase). ModIface_ phase -> Module
mi_module (ModIface -> Module)
-> (HomeModInfo -> ModIface) -> HomeModInfo -> Module
forall b c a. (b -> c) -> (a -> b) -> a -> c
. HomeModInfo -> ModIface
hm_iface
             ; 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 = [(Module, FamInstEnv)] -> ModuleEnv FamInstEnv
forall a. [(Module, a)] -> ModuleEnv a
mkModuleEnv [ (HomeModInfo -> Module
hmiModule HomeModInfo
hmi, HomeModInfo -> FamInstEnv
hmiFamInstEnv HomeModInfo
hmi)
                                           | HomePackageTable
hpt <- HomeUnitGraph -> [HomePackageTable]
unitEnv_hpts HomeUnitGraph
hug
                                           , HomeModInfo
hmi <- HomePackageTable -> [HomeModInfo]
eltsHpt HomePackageTable
hpt ]

             }

       ; checkMany hpt_fam_insts modConsistent 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] -> TcM ()
checkMany ModuleEnv FamInstEnv
hpt_fam_insts Module -> [Module]
modConsistent [Module]
mods = [Module] -> ModuleSet -> [Module] -> TcM ()
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] -> TcM ()
go [Module]
_ ModuleSet
_ [] = () -> TcM ()
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
      go [Module]
consistent ModuleSet
consistent_set (Module
mod:[Module]
mods) = do
        [TcM ()] -> TcM ()
forall (t :: * -> *) (m :: * -> *) a.
(Foldable t, Monad m) =>
t (m a) -> m ()
sequence_
          [ ModuleEnv FamInstEnv -> Module -> Module -> TcM ()
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] -> TcM ()
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 -> WhetherHasFamInst) -> [Module] -> [Module]
forall a. (a -> WhetherHasFamInst) -> [a] -> [a]
filterOut (Module -> ModuleSet -> WhetherHasFamInst
`elemModuleSet` ModuleSet
mod_deps_consistent_set) [Module]
consistent
        to_check_from_mod :: [Module]
to_check_from_mod =
          (Module -> WhetherHasFamInst) -> [Module] -> [Module]
forall a. (a -> WhetherHasFamInst) -> [a] -> [a]
filterOut (Module -> ModuleSet -> WhetherHasFamInst
`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-deterministically 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 -> TcM ()
check ModuleEnv FamInstEnv
hpt_fam_insts Module
m1 Module
m2
      = do { env1' <- ModuleEnv FamInstEnv -> Module -> TcM FamInstEnv
getFamInsts ModuleEnv FamInstEnv
hpt_fam_insts Module
m1
           ; env2' <- getFamInsts hpt_fam_insts 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 = FamInstEnv -> Int
famInstEnvSize FamInstEnv
env1'
                 sizeE2 = FamInstEnv -> Int
famInstEnvSize FamInstEnv
env2'
                 (env1, env2) = if sizeE1 < sizeE2 then (env1', env2')
                                                   else (env2', env1')

           ; let check_now = FamInstEnv -> [FamInst]
famInstEnvElts FamInstEnv
env1
           ; mapM_ (checkForConflicts (emptyFamInstEnv, env2))           check_now
           ; mapM_ (checkForInjectivityConflicts (emptyFamInstEnv,env2)) check_now
 }

getFamInsts :: ModuleEnv FamInstEnv -> Module -> TcM FamInstEnv
getFamInsts :: ModuleEnv FamInstEnv -> Module -> TcM FamInstEnv
getFamInsts ModuleEnv FamInstEnv
hpt_fam_insts Module
mod
  | Just 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 a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (m :: * -> *) a. Monad m => a -> m a
return FamInstEnv
env
  | WhetherHasFamInst
otherwise = do { _ <- 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)
                   ; eps <- getEps
                   ; return (expectJust "checkFamInstConsistency" $
                             lookupModuleEnv (eps_mod_fam_inst_env eps) mod) }
  where
    doc :: SDoc
doc = Module -> SDoc
forall a. Outputable a => a -> SDoc
ppr Module
mod SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"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 -> [TcType] -> Maybe (TcType, TcCoercion)
tcInstNewTyCon_maybe = TyCon -> [TcType] -> Maybe (TcType, 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 -> [TcType] -> (TyCon, [TcType], TcCoercion)
tcLookupDataFamInst (FamInstEnv, FamInstEnv)
fam_inst_envs TyCon
tc [TcType]
tc_args
  | Just (TyCon
rep_tc, [TcType]
rep_args, TcCoercion
co)
      <- (FamInstEnv, FamInstEnv)
-> TyCon -> [TcType] -> Maybe (TyCon, [TcType], TcCoercion)
tcLookupDataFamInst_maybe (FamInstEnv, FamInstEnv)
fam_inst_envs TyCon
tc [TcType]
tc_args
  = (TyCon
rep_tc, [TcType]
rep_args, TcCoercion
co)
  | WhetherHasFamInst
otherwise
  = (TyCon
tc, [TcType]
tc_args, TcType -> TcCoercion
mkRepReflCo (TyCon -> [TcType] -> TcType
mkTyConApp TyCon
tc [TcType]
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 -> [TcType] -> Maybe (TyCon, [TcType], TcCoercion)
tcLookupDataFamInst_maybe (FamInstEnv, FamInstEnv)
fam_inst_envs TyCon
tc [TcType]
tc_args
  | TyCon -> WhetherHasFamInst
isDataFamilyTyCon TyCon
tc
  , FamInstMatch
match : [FamInstMatch]
_ <- (FamInstEnv, FamInstEnv) -> TyCon -> [TcType] -> [FamInstMatch]
lookupFamInstEnv (FamInstEnv, FamInstEnv)
fam_inst_envs TyCon
tc [TcType]
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 -> [CoVar]
fi_cvs   = [CoVar]
cvs })
                 , fim_tys :: FamInstMatch -> [TcType]
fim_tys      = [TcType]
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 -> [TcType] -> [TcCoercion] -> TcCoercion
mkUnbranchedAxInstCo Role
Representational CoAxiom Unbranched
ax [TcType]
rep_args
                                      ([CoVar] -> [TcCoercion]
mkCoVarCos [CoVar]
cvs)
  = WhetherHasFamInst
-> Maybe (TyCon, [TcType], TcCoercion)
-> Maybe (TyCon, [TcType], TcCoercion)
forall a. HasCallStack => WhetherHasFamInst -> a -> a
assert ([TcCoercion] -> WhetherHasFamInst
forall a. [a] -> WhetherHasFamInst
forall (t :: * -> *) a. Foldable t => t a -> WhetherHasFamInst
null [TcCoercion]
rep_cos) (Maybe (TyCon, [TcType], TcCoercion)
 -> Maybe (TyCon, [TcType], TcCoercion))
-> Maybe (TyCon, [TcType], TcCoercion)
-> Maybe (TyCon, [TcType], TcCoercion)
forall a b. (a -> b) -> a -> b
$ -- See Note [Constrained family instances] in ??? (renamed?)
    (TyCon, [TcType], TcCoercion)
-> Maybe (TyCon, [TcType], TcCoercion)
forall a. a -> Maybe a
Just (TyCon
rep_tc, [TcType]
rep_args, TcCoercion
co)

  | WhetherHasFamInst
otherwise
  = Maybe (TyCon, [TcType], TcCoercion)
forall a. Maybe a
Nothing

-- | 'tcTopNormaliseNewTypeTF_maybe' gets rid of top-level newtypes,
-- potentially looking through newtype /instances/ and type synonyms.
--
-- 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 gets a GlobalRdrEnv argument.
--
-- It is careful not to unwrap data/newtype instances nor synonyms
-- 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 ((gres, co), 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
-> TcType
-> Maybe ((Bag (GlobalRdrEltX GREInfo), TcCoercion), TcType)
tcTopNormaliseNewTypeTF_maybe (FamInstEnv, FamInstEnv)
faminsts GlobalRdrEnv
rdr_env TcType
ty
-- cf. FamInstEnv.topNormaliseType_maybe and Coercion.topNormaliseNewType_maybe
  = NormaliseStepper (Bag (GlobalRdrEltX GREInfo), TcCoercion)
-> ((Bag (GlobalRdrEltX GREInfo), TcCoercion)
    -> (Bag (GlobalRdrEltX GREInfo), TcCoercion)
    -> (Bag (GlobalRdrEltX GREInfo), TcCoercion))
-> TcType
-> Maybe ((Bag (GlobalRdrEltX GREInfo), TcCoercion), TcType)
forall ev.
NormaliseStepper ev
-> (ev -> ev -> ev) -> TcType -> Maybe (ev, TcType)
topNormaliseTypeX NormaliseStepper (Bag (GlobalRdrEltX GREInfo), TcCoercion)
stepper (Bag (GlobalRdrEltX GREInfo), TcCoercion)
-> (Bag (GlobalRdrEltX GREInfo), TcCoercion)
-> (Bag (GlobalRdrEltX GREInfo), TcCoercion)
plus TcType
ty
  where
    plus :: (Bag GlobalRdrElt, TcCoercion) -> (Bag GlobalRdrElt, TcCoercion)
         -> (Bag GlobalRdrElt, TcCoercion)
    plus :: (Bag (GlobalRdrEltX GREInfo), TcCoercion)
-> (Bag (GlobalRdrEltX GREInfo), TcCoercion)
-> (Bag (GlobalRdrEltX GREInfo), TcCoercion)
plus (Bag (GlobalRdrEltX GREInfo)
gres1, TcCoercion
co1) (Bag (GlobalRdrEltX GREInfo)
gres2, TcCoercion
co2) = ( Bag (GlobalRdrEltX GREInfo)
gres1 Bag (GlobalRdrEltX GREInfo)
-> Bag (GlobalRdrEltX GREInfo) -> Bag (GlobalRdrEltX GREInfo)
forall a. Bag a -> Bag a -> Bag a
`unionBags` Bag (GlobalRdrEltX GREInfo)
gres2
                                     , TcCoercion
co1 TcCoercion -> TcCoercion -> TcCoercion
`mkTransCo` TcCoercion
co2 )

    stepper :: NormaliseStepper (Bag GlobalRdrElt, TcCoercion)
    stepper :: NormaliseStepper (Bag (GlobalRdrEltX GREInfo), TcCoercion)
stepper = NormaliseStepper (Bag (GlobalRdrEltX GREInfo), TcCoercion)
unwrap_newtype NormaliseStepper (Bag (GlobalRdrEltX GREInfo), TcCoercion)
-> NormaliseStepper (Bag (GlobalRdrEltX GREInfo), TcCoercion)
-> NormaliseStepper (Bag (GlobalRdrEltX GREInfo), TcCoercion)
forall ev.
NormaliseStepper ev -> NormaliseStepper ev -> NormaliseStepper ev
`composeSteppers` NormaliseStepper (Bag (GlobalRdrEltX GREInfo), 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 (GlobalRdrEltX GREInfo), TcCoercion)
unwrap_newtype_instance RecTcChecker
rec_nts TyCon
tc [TcType]
tys
      | Just (TyCon
tc', [TcType]
tys', TcCoercion
co) <- (FamInstEnv, FamInstEnv)
-> TyCon -> [TcType] -> Maybe (TyCon, [TcType], TcCoercion)
tcLookupDataFamInst_maybe (FamInstEnv, FamInstEnv)
faminsts TyCon
tc [TcType]
tys
      = (TcCoercion -> TcCoercion)
-> (Bag (GlobalRdrEltX GREInfo), TcCoercion)
-> (Bag (GlobalRdrEltX GREInfo), TcCoercion)
forall a b.
(a -> b)
-> (Bag (GlobalRdrEltX GREInfo), a)
-> (Bag (GlobalRdrEltX GREInfo), b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (TcCoercion -> TcCoercion -> TcCoercion
mkTransCo TcCoercion
co) ((Bag (GlobalRdrEltX GREInfo), TcCoercion)
 -> (Bag (GlobalRdrEltX GREInfo), TcCoercion))
-> NormaliseStepResult (Bag (GlobalRdrEltX GREInfo), TcCoercion)
-> NormaliseStepResult (Bag (GlobalRdrEltX GREInfo), TcCoercion)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> NormaliseStepper (Bag (GlobalRdrEltX GREInfo), TcCoercion)
unwrap_newtype RecTcChecker
rec_nts TyCon
tc' [TcType]
tys'
      | WhetherHasFamInst
otherwise = NormaliseStepResult (Bag (GlobalRdrEltX GREInfo), TcCoercion)
forall ev. NormaliseStepResult ev
NS_Done

    unwrap_newtype :: NormaliseStepper (Bag (GlobalRdrEltX GREInfo), TcCoercion)
unwrap_newtype RecTcChecker
rec_nts TyCon
tc [TcType]
tys
      | Just DataCon
con <- TyCon -> Maybe DataCon
newTyConDataCon_maybe TyCon
tc
      , Just GlobalRdrEltX GREInfo
gre <- GlobalRdrEnv -> Name -> Maybe (GlobalRdrEltX GREInfo)
forall info.
Outputable info =>
GlobalRdrEnvX info -> Name -> Maybe (GlobalRdrEltX info)
lookupGRE_Name GlobalRdrEnv
rdr_env (DataCon -> Name
dataConName DataCon
con)
           -- This is where we check that the
           -- data constructor is in scope
      = (,) (GlobalRdrEltX GREInfo -> Bag (GlobalRdrEltX GREInfo)
forall a. a -> Bag a
unitBag GlobalRdrEltX GREInfo
gre) (TcCoercion -> (Bag (GlobalRdrEltX GREInfo), TcCoercion))
-> NormaliseStepResult TcCoercion
-> NormaliseStepResult (Bag (GlobalRdrEltX GREInfo), TcCoercion)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> NormaliseStepper TcCoercion
unwrapNewTypeStepper RecTcChecker
rec_nts TyCon
tc [TcType]
tys

      | WhetherHasFamInst
otherwise
      = NormaliseStepResult (Bag (GlobalRdrEltX GREInfo), 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 :: forall a. [FamInst] -> TcM a -> TcM a
tcExtendLocalFamInstEnv [] TcM a
thing_inside = TcM a
thing_inside

-- Otherwise proceed...
tcExtendLocalFamInstEnv [FamInst]
fam_insts 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] -> TcM ()
loadDependentFamInstModules [FamInst]
fam_insts

        -- Now add the instances one by one
      ; env <- TcRnIf TcGblEnv TcLclEnv TcGblEnv
forall gbl lcl. TcRnIf gbl lcl gbl
getGblEnv
      ; (inst_env', fam_insts') <- foldlM addLocalFamInst
                                       (tcg_fam_inst_env env, tcg_fam_insts env)
                                       fam_insts

      ; let env' = TcGblEnv
env { tcg_fam_insts    = fam_insts'
                       , tcg_fam_inst_env = inst_env' }
      ; setGblEnv env' 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] -> TcM ()
loadDependentFamInstModules [FamInst]
fam_insts
 = do { env <- TcRnIf TcGblEnv TcLclEnv TcGblEnv
forall gbl lcl. TcRnIf gbl lcl gbl
getGblEnv
      ; let this_mod = TcGblEnv -> Module
tcg_mod TcGblEnv
env
            imports  = TcGblEnv -> ImportAvails
tcg_imports TcGblEnv
env

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

      ; loadModuleInterfaces (text "Loading family-instance modules") $
        filter want_module (imp_finsts 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 GHC.Core.FamInstEnv
addLocalFamInst :: (FamInstEnv,[FamInst])
                -> FamInst
                -> TcM (FamInstEnv, [FamInst])
addLocalFamInst :: (FamInstEnv, [FamInst])
-> FamInst -> IOEnv (Env TcGblEnv TcLclEnv) (FamInstEnv, [FamInst])
addLocalFamInst (FamInstEnv
home_fie, [FamInst]
my_fis) FamInst
fam_inst
        -- home_fie includes home package and this module
        -- my_fies is just the ones from this module
  = do { String -> SDoc -> TcM ()
traceTc String
"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.

       ; mod <- IOEnv (Env TcGblEnv TcLclEnv) Module
forall (m :: * -> *). HasModule m => m Module
getModule
       ; traceTc "alfi" (ppr 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.
       ; eps <- getEps
       ; let inst_envs = (ExternalPackageState -> FamInstEnv
eps_fam_inst_env ExternalPackageState
eps, FamInstEnv
home_fie)
             home_fie' = FamInstEnv -> FamInst -> FamInstEnv
extendFamInstEnv FamInstEnv
home_fie FamInst
fam_inst

           -- Check for conflicting instance decls and injectivity violations
       ; ((), no_errs) <- askNoErrs $
         do { checkForConflicts            inst_envs fam_inst
            ; checkForInjectivityConflicts inst_envs fam_inst
            ; checkInjectiveEquation       fam_inst
            }

       ; if no_errs then
            return (home_fie', fam_inst : my_fis)
         else
            return (home_fie,  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).
-}

-- | Checks to make sure no two family instances overlap.
checkForConflicts :: FamInstEnvs -> FamInst -> TcM ()
checkForConflicts :: (FamInstEnv, FamInstEnv) -> FamInst -> TcM ()
checkForConflicts (FamInstEnv, FamInstEnv)
inst_envs FamInst
fam_inst
  = do { let conflicts :: [FamInst]
conflicts = (FamInstEnv, FamInstEnv) -> FamInst -> [FamInst]
lookupFamInstEnvConflicts (FamInstEnv, FamInstEnv)
inst_envs FamInst
fam_inst
       ; String -> SDoc -> TcM ()
traceTc String
"checkForConflicts" (SDoc -> TcM ()) -> SDoc -> TcM ()
forall a b. (a -> b) -> a -> b
$
         [SDoc] -> SDoc
forall doc. IsDoc doc => [doc] -> doc
vcat [ [FamInst] -> SDoc
forall a. Outputable a => a -> SDoc
ppr [FamInst]
conflicts
              , FamInst -> SDoc
forall a. Outputable a => a -> SDoc
ppr FamInst
fam_inst
              -- , ppr inst_envs
         ]
       ; FamInst -> [FamInst] -> TcM ()
reportConflictInstErr FamInst
fam_inst [FamInst]
conflicts }

checkForInjectivityConflicts :: FamInstEnvs -> FamInst -> TcM ()
  -- see Note [Verifying injectivity annotation] in GHC.Core.FamInstEnv, check 1B1.
checkForInjectivityConflicts :: (FamInstEnv, FamInstEnv) -> FamInst -> TcM ()
checkForInjectivityConflicts (FamInstEnv, FamInstEnv)
instEnvs FamInst
famInst
    | TyCon -> WhetherHasFamInst
isTypeFamilyTyCon TyCon
tycon   -- as opposed to data family tycon
    , Injective [WhetherHasFamInst]
inj <- TyCon -> Injectivity
tyConInjectivityInfo TyCon
tycon
    = let conflicts :: [CoAxBranch]
conflicts = [WhetherHasFamInst]
-> (FamInstEnv, FamInstEnv) -> FamInst -> [CoAxBranch]
lookupFamInstEnvInjectivityConflicts [WhetherHasFamInst]
inj (FamInstEnv, FamInstEnv)
instEnvs FamInst
famInst in
      TyCon -> [CoAxBranch] -> CoAxBranch -> TcM ()
reportConflictingInjectivityErrs TyCon
tycon [CoAxBranch]
conflicts (CoAxiom Unbranched -> CoAxBranch
coAxiomSingleBranch (FamInst -> CoAxiom Unbranched
fi_axiom FamInst
famInst))

    | WhetherHasFamInst
otherwise
    = () -> TcM ()
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (m :: * -> *) a. Monad m => a -> m a
return ()

    where tycon :: TyCon
tycon = FamInst -> TyCon
famInstTyCon FamInst
famInst

-- | 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. This looks only at the one equation; it does not look for
-- interaction between equations. Use checkForInjectivityConflicts for that.
-- Does checks (2)-(4) of Note [Verifying injectivity annotation] in "GHC.Core.FamInstEnv".
checkInjectiveEquation :: FamInst -> TcM ()
checkInjectiveEquation :: FamInst -> TcM ()
checkInjectiveEquation FamInst
famInst
    | TyCon -> WhetherHasFamInst
isTypeFamilyTyCon TyCon
tycon
    -- type family is injective in at least one argument
    , Injective [WhetherHasFamInst]
inj <- TyCon -> Injectivity
tyConInjectivityInfo TyCon
tycon = do
    { dflags <- IOEnv (Env TcGblEnv TcLclEnv) DynFlags
forall (m :: * -> *). HasDynFlags m => m DynFlags
getDynFlags
    ; let axiom = CoAxiom Unbranched -> CoAxBranch
coAxiomSingleBranch CoAxiom Unbranched
fi_ax
          -- see Note [Verifying injectivity annotation] in GHC.Core.FamInstEnv
    ; reportInjectivityErrors dflags fi_ax axiom inj
    }

    -- if there was no injectivity annotation or tycon does not represent a
    -- type family we report no conflicts
    | WhetherHasFamInst
otherwise
    = () -> TcM ()
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (m :: * -> *) a. Monad m => a -> m a
return ()

    where tycon :: TyCon
tycon = FamInst -> TyCon
famInstTyCon FamInst
famInst
          fi_ax :: CoAxiom Unbranched
fi_ax = FamInst -> CoAxiom Unbranched
fi_axiom FamInst
famInst

-- | Report a list of injectivity errors together with their source locations.
-- Looks only at one equation; does not look for conflicts *among* equations.
reportInjectivityErrors
   :: DynFlags
   -> CoAxiom br   -- ^ Type family for which we generate errors
   -> CoAxBranch   -- ^ Currently checked equation (represented by axiom)
   -> [Bool]       -- ^ Injectivity annotation
   -> TcM ()
reportInjectivityErrors :: forall (br :: BranchFlag).
DynFlags
-> CoAxiom br -> CoAxBranch -> [WhetherHasFamInst] -> TcM ()
reportInjectivityErrors DynFlags
dflags CoAxiom br
fi_ax CoAxBranch
axiom [WhetherHasFamInst]
inj
  = WhetherHasFamInst -> SDoc -> TcM () -> TcM ()
forall a. HasCallStack => WhetherHasFamInst -> SDoc -> a -> a
assertPpr ((WhetherHasFamInst -> WhetherHasFamInst)
-> [WhetherHasFamInst] -> WhetherHasFamInst
forall (t :: * -> *) a.
Foldable t =>
(a -> WhetherHasFamInst) -> t a -> WhetherHasFamInst
any WhetherHasFamInst -> WhetherHasFamInst
forall a. a -> a
id [WhetherHasFamInst]
inj) (String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"No injective type variables") (TcM () -> TcM ()) -> TcM () -> TcM ()
forall a b. (a -> b) -> a -> b
$
    do let lhs :: [TcType]
lhs             = CoAxBranch -> [TcType]
coAxBranchLHS CoAxBranch
axiom
           rhs :: TcType
rhs             = CoAxBranch -> TcType
coAxBranchRHS CoAxBranch
axiom
           fam_tc :: TyCon
fam_tc          = CoAxiom br -> TyCon
forall (br :: BranchFlag). CoAxiom br -> TyCon
coAxiomTyCon CoAxiom br
fi_ax
           (TyVarSet
unused_inj_tvs, HasKinds
unused_vis, SuggestUndecidableInstances
undec_inst_flag)
                           = DynFlags
-> TyCon
-> [TcType]
-> TcType
-> (TyVarSet, HasKinds, SuggestUndecidableInstances)
unusedInjTvsInRHS DynFlags
dflags TyCon
fam_tc [TcType]
lhs TcType
rhs
           inj_tvs_unused :: WhetherHasFamInst
inj_tvs_unused  = WhetherHasFamInst -> WhetherHasFamInst
not (WhetherHasFamInst -> WhetherHasFamInst)
-> WhetherHasFamInst -> WhetherHasFamInst
forall a b. (a -> b) -> a -> b
$ TyVarSet -> WhetherHasFamInst
isEmptyVarSet TyVarSet
unused_inj_tvs
           tf_headed :: WhetherHasFamInst
tf_headed       = TcType -> WhetherHasFamInst
isTFHeaded TcType
rhs
           bare_variables :: [TcType]
bare_variables  = [TcType] -> TcType -> [TcType]
bareTvInRHSViolated [TcType]
lhs TcType
rhs
           wrong_bare_rhs :: WhetherHasFamInst
wrong_bare_rhs  = WhetherHasFamInst -> WhetherHasFamInst
not (WhetherHasFamInst -> WhetherHasFamInst)
-> WhetherHasFamInst -> WhetherHasFamInst
forall a b. (a -> b) -> a -> b
$ [TcType] -> WhetherHasFamInst
forall a. [a] -> WhetherHasFamInst
forall (t :: * -> *) a. Foldable t => t a -> WhetherHasFamInst
null [TcType]
bare_variables

       WhetherHasFamInst -> TcM () -> TcM ()
forall (f :: * -> *).
Applicative f =>
WhetherHasFamInst -> f () -> f ()
when WhetherHasFamInst
inj_tvs_unused (TcM () -> TcM ()) -> TcM () -> TcM ()
forall a b. (a -> b) -> a -> b
$ TyCon
-> TyVarSet
-> HasKinds
-> SuggestUndecidableInstances
-> CoAxBranch
-> TcM ()
reportUnusedInjectiveVarsErr TyCon
fam_tc TyVarSet
unused_inj_tvs
                                                          HasKinds
unused_vis SuggestUndecidableInstances
undec_inst_flag CoAxBranch
axiom
       WhetherHasFamInst -> TcM () -> TcM ()
forall (f :: * -> *).
Applicative f =>
WhetherHasFamInst -> f () -> f ()
when WhetherHasFamInst
tf_headed      (TcM () -> TcM ()) -> TcM () -> TcM ()
forall a b. (a -> b) -> a -> b
$ TyCon -> CoAxBranch -> TcM ()
reportTfHeadedErr            TyCon
fam_tc CoAxBranch
axiom
       WhetherHasFamInst -> TcM () -> TcM ()
forall (f :: * -> *).
Applicative f =>
WhetherHasFamInst -> f () -> f ()
when WhetherHasFamInst
wrong_bare_rhs (TcM () -> TcM ()) -> TcM () -> TcM ()
forall a b. (a -> b) -> a -> b
$ TyCon -> [TcType] -> CoAxBranch -> TcM ()
reportBareVariableInRHSErr   TyCon
fam_tc [TcType]
bare_variables CoAxBranch
axiom

-- | Is type headed by a type family application?
isTFHeaded :: Type -> Bool
-- See Note [Verifying injectivity annotation], case 3.
isTFHeaded :: TcType -> WhetherHasFamInst
isTFHeaded TcType
ty | Just TcType
ty' <- TcType -> Maybe TcType
coreView TcType
ty
              = TcType -> WhetherHasFamInst
isTFHeaded TcType
ty'
isTFHeaded TcType
ty | (TyConApp TyCon
tc [TcType]
args) <- TcType
ty
              , TyCon -> WhetherHasFamInst
isTypeFamilyTyCon TyCon
tc
              = [TcType]
args [TcType] -> Int -> WhetherHasFamInst
forall a. [a] -> Int -> WhetherHasFamInst
`lengthIs` TyCon -> Int
tyConArity TyCon
tc
isTFHeaded TcType
_  = WhetherHasFamInst
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], case 2.
bareTvInRHSViolated :: [TcType] -> TcType -> [TcType]
bareTvInRHSViolated [TcType]
pats TcType
rhs | TcType -> WhetherHasFamInst
isTyVarTy TcType
rhs
   = (TcType -> WhetherHasFamInst) -> [TcType] -> [TcType]
forall a. (a -> WhetherHasFamInst) -> [a] -> [a]
filter (WhetherHasFamInst -> WhetherHasFamInst
not (WhetherHasFamInst -> WhetherHasFamInst)
-> (TcType -> WhetherHasFamInst) -> TcType -> WhetherHasFamInst
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TcType -> WhetherHasFamInst
isTyVarTy) [TcType]
pats
bareTvInRHSViolated [TcType]
_ TcType
_ = []

------------------------------------------------------------------
-- Checking for the coverage condition for injective type families
------------------------------------------------------------------

{-
Note [Coverage condition for injective type families]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
The Injective Type Families paper describes how we can tell whether
or not a type family equation upholds the injectivity condition.
Briefly, consider the following:

  type family F a b = r | r -> a      -- NB: b is not injective

  type instance F ty1 ty2 = ty3

We need to make sure that all variables mentioned in ty1 are mentioned in ty3
-- that's how we know that knowing ty3 determines ty1. But they can't be
mentioned just anywhere in ty3: they must be in *injective* positions in ty3.
For example:

  type instance F a Int = Maybe (G a)

This is no good, if G is not injective. However, if G is indeed injective,
then this would appear to meet our needs. There is a trap here, though: while
knowing G a does indeed determine a, trying to compute a from G a might not
terminate. This is precisely the same problem that we have with functional
dependencies and their liberal coverage condition. Here is the test case:

  type family G a = r | r -> a
  type instance G [a] = [G a]
  [W] G alpha ~ [alpha]

We see that the equation given applies, because G alpha equals a list. So we
learn that alpha must be [beta] for some beta. We then have

  [W] G [beta] ~ [[beta]]

This can reduce to

  [W] [G beta] ~ [[beta]]

which then decomposes to

  [W] G beta ~ [beta]

right where we started. The equation G [a] = [G a] thus is dangerous: while
it does not violate the injectivity assumption, it might throw us into a loop,
with a particularly dastardly Wanted.

We thus do what functional dependencies do: require -XUndecidableInstances to
accept this.

Checking the coverage condition is not terribly hard, but we also want to produce
a nice error message. A nice error message has at least two properties:

1. If any of the variables involved are invisible or are used in an invisible context,
we want to print invisible arguments (as -fprint-explicit-kinds does).

2. If we fail to accept the equation because we're worried about non-termination,
we want to suggest UndecidableInstances.

To gather the right information, we can talk about the *usage* of a variable. Every
variable is used either visibly or invisibly, and it is either not used at all,
in a context where acceptance requires UndecidableInstances, or in a context that
does not require UndecidableInstances. If a variable is used both visibly and
invisibly, then we want to remember the fact that it was used invisibly: printing
out invisibles will be helpful for the user to understand what is going on.
If a variable is used where we need -XUndecidableInstances and where we don't,
we can similarly just remember the latter.

We thus define Visibility and NeedsUndecInstFlag below. These enumerations are
*ordered*, and we used their Ord instances. We then define VarUsage, which is just a pair
of a Visibility and a NeedsUndecInstFlag. (The visibility is irrelevant when a
variable is NotPresent, but this extra slack in the representation causes no
harm.) We finally define VarUsages as a mapping from variables to VarUsage.
Its Monoid instance combines two maps, using the Semigroup instance of VarUsage
to combine elements that are represented in both maps. In this way, we can
compositionally analyze types (and portions thereof).

To do the injectivity check:

1. We build VarUsages that represent the LHS (rather, the portion of the LHS
that is flagged as injective); each usage on the LHS is NotPresent, because we
have not yet looked at the RHS.

2. We also build a VarUsage for the RHS, done by injTyVarUsages.

3. We then combine these maps. Now, every variable in the injective components of the LHS
will be mapped to its correct usage (either NotPresent or perhaps needing
-XUndecidableInstances in order to be seen as injective).

4. We look up each var used in an injective argument on the LHS in
the map, making a list of tvs that should be determined by the RHS
but aren't.

5. We then return the set of bad variables, whether any of the bad
ones were used invisibly, and whether any bad ones need -XUndecidableInstances.
If -XUndecidableInstances is enabled, than a var that needs the flag
won't be bad, so it won't appear in this list.

6. We use all this information to produce a nice error message, (a) switching
on -fprint-explicit-kinds if appropriate and (b) telling the user about
-XUndecidableInstances if appropriate.

-}

-- | Return the set of type variables that a type family equation is
-- expected to be injective in but is not. Suppose we have @type family
-- F a b = r | r -> a@. Then any variables that appear free in the first
-- argument to F in an equation must be fixed by that equation's RHS.
-- This function returns all such variables that are not indeed fixed.
-- It also returns whether any of these variables appear invisibly
-- and whether -XUndecidableInstances would help.
-- See Note [Coverage condition for injective type families].
unusedInjTvsInRHS :: DynFlags
                  -> TyCon  -- type family
                  -> [Type] -- LHS arguments
                  -> Type   -- the RHS
                  -> ( TyVarSet
                     , HasKinds                     -- YesHasKinds <=> one or more variable is used invisibly
                     , SuggestUndecidableInstances) -- YesSuggestUndecidableInstaces <=> suggest -XUndecidableInstances
-- See Note [Verifying injectivity annotation] in GHC.Core.FamInstEnv.
-- This function implements check (4) described there, further
-- described in Note [Coverage condition for injective type families].
-- In theory (and modulo the -XUndecidableInstances wrinkle),
-- 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 :: DynFlags
-> TyCon
-> [TcType]
-> TcType
-> (TyVarSet, HasKinds, SuggestUndecidableInstances)
unusedInjTvsInRHS DynFlags
dflags tycon :: TyCon
tycon@(TyCon -> Injectivity
tyConInjectivityInfo -> Injective [WhetherHasFamInst]
inj_list) [TcType]
lhs TcType
rhs =
  -- Note [Coverage condition for injective type families], step 5
  (TyVarSet
bad_vars, WhetherHasFamInst -> HasKinds
hasKinds WhetherHasFamInst
any_invisible, WhetherHasFamInst -> SuggestUndecidableInstances
suggestUndecidableInstances WhetherHasFamInst
suggest_undec)
    where
      undec_inst :: WhetherHasFamInst
undec_inst = Extension -> DynFlags -> WhetherHasFamInst
xopt Extension
LangExt.UndecidableInstances DynFlags
dflags

      inj_lhs :: [TcType]
inj_lhs = [WhetherHasFamInst] -> [TcType] -> [TcType]
forall a. [WhetherHasFamInst] -> [a] -> [a]
filterByList [WhetherHasFamInst]
inj_list [TcType]
lhs
      lhs_vars :: TyVarSet
lhs_vars = [TcType] -> TyVarSet
tyCoVarsOfTypes [TcType]
inj_lhs

      rhs_inj_vars :: TyVarSet
rhs_inj_vars = FV -> TyVarSet
fvVarSet (FV -> TyVarSet) -> FV -> TyVarSet
forall a b. (a -> b) -> a -> b
$ WhetherHasFamInst -> TcType -> FV
injectiveVarsOfType WhetherHasFamInst
undec_inst TcType
rhs

      bad_vars :: TyVarSet
bad_vars = TyVarSet
lhs_vars TyVarSet -> TyVarSet -> TyVarSet
`minusVarSet` TyVarSet
rhs_inj_vars

      any_bad :: WhetherHasFamInst
any_bad = WhetherHasFamInst -> WhetherHasFamInst
not (WhetherHasFamInst -> WhetherHasFamInst)
-> WhetherHasFamInst -> WhetherHasFamInst
forall a b. (a -> b) -> a -> b
$ TyVarSet -> WhetherHasFamInst
isEmptyVarSet TyVarSet
bad_vars

      invis_vars :: TyVarSet
invis_vars = FV -> TyVarSet
fvVarSet (FV -> TyVarSet) -> FV -> TyVarSet
forall a b. (a -> b) -> a -> b
$ [TcType] -> FV
invisibleVarsOfTypes [TyCon -> [TcType] -> TcType
mkTyConApp TyCon
tycon [TcType]
lhs, TcType
rhs]

      any_invisible :: WhetherHasFamInst
any_invisible = WhetherHasFamInst
any_bad WhetherHasFamInst -> WhetherHasFamInst -> WhetherHasFamInst
&& (TyVarSet
bad_vars TyVarSet -> TyVarSet -> WhetherHasFamInst
`intersectsVarSet` TyVarSet
invis_vars)
      suggest_undec :: WhetherHasFamInst
suggest_undec = WhetherHasFamInst
any_bad WhetherHasFamInst -> WhetherHasFamInst -> WhetherHasFamInst
&&
                      WhetherHasFamInst -> WhetherHasFamInst
not WhetherHasFamInst
undec_inst WhetherHasFamInst -> WhetherHasFamInst -> WhetherHasFamInst
&&
                      (TyVarSet
lhs_vars TyVarSet -> TyVarSet -> WhetherHasFamInst
`subVarSet` FV -> TyVarSet
fvVarSet (WhetherHasFamInst -> TcType -> FV
injectiveVarsOfType WhetherHasFamInst
True TcType
rhs))

-- When the type family is not injective in any arguments
unusedInjTvsInRHS DynFlags
_ TyCon
_ [TcType]
_ TcType
_ = (TyVarSet
emptyVarSet, HasKinds
NoHasKinds, SuggestUndecidableInstances
NoSuggestUndecidableInstaces)

---------------------------------------
-- Producing injectivity error messages
---------------------------------------

-- | Report error message for a pair of equations violating an injectivity
-- annotation. No error message if there are no branches.
reportConflictingInjectivityErrs :: TyCon -> [CoAxBranch] -> CoAxBranch -> TcM ()
reportConflictingInjectivityErrs :: TyCon -> [CoAxBranch] -> CoAxBranch -> TcM ()
reportConflictingInjectivityErrs TyCon
_ [] CoAxBranch
_ = () -> TcM ()
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
reportConflictingInjectivityErrs TyCon
fam_tc (CoAxBranch
confEqn1:[CoAxBranch]
_) CoAxBranch
tyfamEqn
  = [(SrcSpan, TcRnMessage)] -> TcM ()
addErrs [(TyCon -> NonEmpty CoAxBranch -> TcRnMessage)
-> TyCon -> NonEmpty CoAxBranch -> (SrcSpan, TcRnMessage)
buildInjectivityError (InjectivityErrReason -> TyCon -> NonEmpty CoAxBranch -> TcRnMessage
TcRnFamInstNotInjective InjectivityErrReason
InjErrRhsOverlap)
                                   TyCon
fam_tc
                                   (CoAxBranch
confEqn1 CoAxBranch -> [CoAxBranch] -> NonEmpty CoAxBranch
forall a. a -> [a] -> NonEmpty a
:| [CoAxBranch
tyfamEqn])]

-- | Report error message for equation with injective type variables unused in
-- the RHS. Note [Coverage condition for injective type families], step 6
reportUnusedInjectiveVarsErr :: TyCon
                             -> TyVarSet
                             -> HasKinds                    -- YesHasKinds <=> print invisible arguments
                             -> SuggestUndecidableInstances -- YesSuggestUndecidableInstaces <=> suggest -XUndecidableInstances
                             -> CoAxBranch
                             -> TcM ()
reportUnusedInjectiveVarsErr :: TyCon
-> TyVarSet
-> HasKinds
-> SuggestUndecidableInstances
-> CoAxBranch
-> TcM ()
reportUnusedInjectiveVarsErr TyCon
fam_tc TyVarSet
tvs HasKinds
has_kinds SuggestUndecidableInstances
undec_inst CoAxBranch
tyfamEqn
  = let reason :: InjectivityErrReason
reason     = TyVarSet
-> HasKinds -> SuggestUndecidableInstances -> InjectivityErrReason
InjErrCannotInferFromRhs TyVarSet
tvs HasKinds
has_kinds SuggestUndecidableInstances
undec_inst
        (SrcSpan
loc, TcRnMessage
dia) = (TyCon -> NonEmpty CoAxBranch -> TcRnMessage)
-> TyCon -> NonEmpty CoAxBranch -> (SrcSpan, TcRnMessage)
buildInjectivityError (InjectivityErrReason -> TyCon -> NonEmpty CoAxBranch -> TcRnMessage
TcRnFamInstNotInjective InjectivityErrReason
reason) TyCon
fam_tc (CoAxBranch
tyfamEqn CoAxBranch -> [CoAxBranch] -> NonEmpty CoAxBranch
forall a. a -> [a] -> NonEmpty a
:| [])
    in SrcSpan -> TcRnMessage -> TcM ()
addErrAt SrcSpan
loc TcRnMessage
dia

-- | Report error message for equation that has a type family call at the top
-- level of RHS
reportTfHeadedErr :: TyCon -> CoAxBranch -> TcM ()
reportTfHeadedErr :: TyCon -> CoAxBranch -> TcM ()
reportTfHeadedErr TyCon
fam_tc CoAxBranch
branch
  = [(SrcSpan, TcRnMessage)] -> TcM ()
addErrs [(TyCon -> NonEmpty CoAxBranch -> TcRnMessage)
-> TyCon -> NonEmpty CoAxBranch -> (SrcSpan, TcRnMessage)
buildInjectivityError (InjectivityErrReason -> TyCon -> NonEmpty CoAxBranch -> TcRnMessage
TcRnFamInstNotInjective InjectivityErrReason
InjErrRhsCannotBeATypeFam)
                                   TyCon
fam_tc
                                   (CoAxBranch
branch CoAxBranch -> [CoAxBranch] -> NonEmpty CoAxBranch
forall a. a -> [a] -> NonEmpty a
:| [])]

-- | Report error message for equation that has a bare type variable in the RHS
-- but LHS pattern is not a bare type variable.
reportBareVariableInRHSErr :: TyCon -> [Type] -> CoAxBranch -> TcM ()
reportBareVariableInRHSErr :: TyCon -> [TcType] -> CoAxBranch -> TcM ()
reportBareVariableInRHSErr TyCon
fam_tc [TcType]
tys CoAxBranch
branch
  = [(SrcSpan, TcRnMessage)] -> TcM ()
addErrs [(TyCon -> NonEmpty CoAxBranch -> TcRnMessage)
-> TyCon -> NonEmpty CoAxBranch -> (SrcSpan, TcRnMessage)
buildInjectivityError (InjectivityErrReason -> TyCon -> NonEmpty CoAxBranch -> TcRnMessage
TcRnFamInstNotInjective ([TcType] -> InjectivityErrReason
InjErrRhsBareTyVar [TcType]
tys))
                                   TyCon
fam_tc
                                   (CoAxBranch
branch CoAxBranch -> [CoAxBranch] -> NonEmpty CoAxBranch
forall a. a -> [a] -> NonEmpty a
:| [])]

buildInjectivityError :: (TyCon -> NonEmpty CoAxBranch -> TcRnMessage)
                      -> TyCon
                      -> NonEmpty CoAxBranch
                      -> (SrcSpan, TcRnMessage)
buildInjectivityError :: (TyCon -> NonEmpty CoAxBranch -> TcRnMessage)
-> TyCon -> NonEmpty CoAxBranch -> (SrcSpan, TcRnMessage)
buildInjectivityError TyCon -> NonEmpty CoAxBranch -> TcRnMessage
mkErr TyCon
fam_tc NonEmpty CoAxBranch
branches
  = ( CoAxBranch -> SrcSpan
coAxBranchSpan (NonEmpty CoAxBranch -> CoAxBranch
forall a. NonEmpty a -> a
NE.head NonEmpty CoAxBranch
branches), TyCon -> NonEmpty CoAxBranch -> TcRnMessage
mkErr TyCon
fam_tc NonEmpty CoAxBranch
branches )

reportConflictInstErr :: FamInst -> [FamInst] -> TcRn ()
reportConflictInstErr :: FamInst -> [FamInst] -> TcM ()
reportConflictInstErr FamInst
_ []
  = () -> TcM ()
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (m :: * -> *) a. Monad m => a -> m a
return ()  -- No conflicts
reportConflictInstErr FamInst
fam_inst (FamInst
conf_inst : [FamInst]
_) =
   -- The sortBy just arranges that instances are displayed in order
   -- of source location, which reduced wobbling in error messages,
   -- and is better for users
  let   sorted :: NonEmpty FamInst
sorted  = (FamInst -> FamInst -> Ordering)
-> NonEmpty FamInst -> NonEmpty FamInst
forall a. (a -> a -> Ordering) -> NonEmpty a -> NonEmpty a
NE.sortBy (SrcSpan -> SrcSpan -> Ordering
SrcLoc.leftmost_smallest (SrcSpan -> SrcSpan -> Ordering)
-> (FamInst -> SrcSpan) -> FamInst -> FamInst -> Ordering
forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` FamInst -> SrcSpan
getSpan) (FamInst
fam_inst FamInst -> [FamInst] -> NonEmpty FamInst
forall a. a -> [a] -> NonEmpty a
NE.:| [FamInst
conf_inst])
        fi1 :: FamInst
fi1     = NonEmpty FamInst -> FamInst
forall a. NonEmpty a -> a
NE.head NonEmpty FamInst
sorted
        span :: SrcSpan
span    = CoAxBranch -> SrcSpan
coAxBranchSpan (CoAxiom Unbranched -> CoAxBranch
coAxiomSingleBranch (FamInst -> CoAxiom Unbranched
famInstAxiom FamInst
fi1))
        getSpan :: FamInst -> SrcSpan
getSpan = CoAxiom Unbranched -> SrcSpan
forall a. NamedThing a => a -> SrcSpan
getSrcSpan (CoAxiom Unbranched -> SrcSpan)
-> (FamInst -> CoAxiom Unbranched) -> FamInst -> SrcSpan
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FamInst -> CoAxiom Unbranched
famInstAxiom
  in SrcSpan -> TcM () -> TcM ()
forall a. SrcSpan -> TcRn a -> TcRn a
setSrcSpan SrcSpan
span (TcM () -> TcM ()) -> TcM () -> TcM ()
forall a b. (a -> b) -> a -> b
$ TcRnMessage -> TcM ()
addErr (TcRnMessage -> TcM ()) -> TcRnMessage -> TcM ()
forall a b. (a -> b) -> a -> b
$ NonEmpty FamInst -> TcRnMessage
TcRnConflictingFamInstDecls NonEmpty FamInst
sorted

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 { eps <- TcRnIf TcGblEnv TcLclEnv ExternalPackageState
forall gbl lcl. TcRnIf gbl lcl ExternalPackageState
getEps; env <- getGblEnv
       ; return (eps_fam_inst_env eps, tcg_fam_inst_env env) }