FamInst.hs 45.6 KB
Newer Older
Austin Seipp's avatar
Austin Seipp committed
1
-- The @FamInst@ type: family instance heads
2

3
{-# LANGUAGE CPP, GADTs, ViewPatterns #-}
Ian Lynagh's avatar
Ian Lynagh committed
4

5 6
module FamInst (
        FamInstEnvs, tcGetFamInstEnvs,
7
        checkFamInstConsistency, tcExtendLocalFamInstEnv,
8 9
        tcLookupDataFamInst, tcLookupDataFamInst_maybe,
        tcInstNewTyCon_maybe, tcTopNormaliseNewTypeTF_maybe,
Jan Stolarek's avatar
Jan Stolarek committed
10 11 12
        newFamInst,

        -- * Injectivity
13
        reportInjectivityErrors, reportConflictingInjectivityErrs
14 15
    ) where

16 17
import GhcPrelude

Sylvain Henry's avatar
Sylvain Henry committed
18
import GHC.Driver.Types
Sylvain Henry's avatar
Sylvain Henry committed
19 20 21
import GHC.Core.FamInstEnv
import GHC.Core.InstEnv( roughMatchTcs )
import GHC.Core.Coercion
Sylvain Henry's avatar
Sylvain Henry committed
22
import GHC.Core.Lint
23
import TcEvidence
24
import GHC.Iface.Load
Simon Marlow's avatar
Simon Marlow committed
25
import TcRnMonad
Sylvain Henry's avatar
Sylvain Henry committed
26
import GHC.Types.SrcLoc as SrcLoc
Sylvain Henry's avatar
Sylvain Henry committed
27
import GHC.Core.TyCon
28
import TcType
Sylvain Henry's avatar
Sylvain Henry committed
29
import GHC.Core.Coercion.Axiom
Sylvain Henry's avatar
Sylvain Henry committed
30
import GHC.Driver.Session
Sylvain Henry's avatar
Sylvain Henry committed
31
import GHC.Types.Module
32
import Outputable
33
import Util
Sylvain Henry's avatar
Sylvain Henry committed
34
import GHC.Types.Name.Reader
Sylvain Henry's avatar
Sylvain Henry committed
35
import GHC.Core.DataCon ( dataConName )
36
import Maybes
Sylvain Henry's avatar
Sylvain Henry committed
37 38 39
import GHC.Core.TyCo.Rep
import GHC.Core.TyCo.FVs
import GHC.Core.TyCo.Ppr ( pprWithExplicitKindsWhen )
40
import TcMType
Sylvain Henry's avatar
Sylvain Henry committed
41
import GHC.Types.Name
42
import Panic
Sylvain Henry's avatar
Sylvain Henry committed
43
import GHC.Types.Var.Set
44
import FV
45
import Bag( Bag, unionBags, unitBag )
46
import Control.Monad
47
import Data.List ( sortBy )
48
import Data.List.NonEmpty ( NonEmpty(..) )
49
import Data.Function ( on )
50

51 52
import qualified GHC.LanguageExtensions  as LangExt

53
#include "HsVersions.h"
54

55 56
{- Note [The type family instance consistency story]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92

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
93 94
  "family instance module". This flag `mi_finsts` is recorded in the
  interface file.
95 96

* For every module we calculate the set of all of its direct and
97 98 99
  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.
100 101

* When type checking a module M we check consistency of all the type
102 103 104
  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.
105

106 107 108 109 110
  - 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).
111

112 113 114
  - 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'.
115

116
There are four subtle points in this scheme which have not been
117 118 119
addressed yet.

* We have checked consistency of the family instances *defined* by M
120 121 122 123 124 125 126 127 128
  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.
129 130

* It can also happen that M uses a function defined in another module
131 132 133 134 135
  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.
136 137

* When a module C imports a boot module B.hs-boot, we check that C's
138 139 140 141 142 143 144 145 146
  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.
147
  See Note [Loading your own hi-boot file] in GHC.Iface.Load.
148 149
-}

Austin Seipp's avatar
Austin Seipp committed
150 151 152
{-
************************************************************************
*                                                                      *
153
                 Making a FamInst
Austin Seipp's avatar
Austin Seipp committed
154 155 156
*                                                                      *
************************************************************************
-}
157 158 159 160 161

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

163
newFamInst :: FamFlavor -> CoAxiom Unbranched -> TcM FamInst
164
-- Freshen the type variables of the FamInst branches
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
165
newFamInst flavor axiom@(CoAxiom { co_ax_tc = fam_tc })
166 167
  = ASSERT2( tyCoVarsOfTypes lhs `subVarSet` tcv_set, text "lhs" <+> pp_ax )
    ASSERT2( lhs_kind `eqType` rhs_kind, text "kind" <+> pp_ax $$ ppr lhs_kind $$ ppr rhs_kind )
Simon Peyton Jones's avatar
Simon Peyton Jones committed
168 169 170
    -- We used to have an assertion that the tyvars of the RHS were bound
    -- by tcv_set, but in error situations like  F Int = a that isn't
    -- true; a later check in checkValidFamInst rejects it
171
    do { (subst, tvs') <- freshenTyVarBndrs tvs
172
       ; (subst, cvs') <- freshenCoVarBndrsX subst cvs
Ryan Scott's avatar
Ryan Scott committed
173 174 175
       ; dflags <- getDynFlags
       ; let lhs'     = substTys subst lhs
             rhs'     = substTy  subst rhs
176
             tcvs'    = tvs' ++ cvs'
177 178 179 180
       ; ifErrsM (return ()) $ -- Don't lint when there are errors, because
                               -- errors might mean TcTyCons.
                               -- See Note [Recover from validity error] in TcTyClsDecls
         when (gopt Opt_DoCoreLinting dflags) $
Ryan Scott's avatar
Ryan Scott committed
181 182 183
           -- 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].
184
           case lintTypes dflags tcvs' (rhs':lhs') of
Ryan Scott's avatar
Ryan Scott committed
185
             Nothing       -> pure ()
186 187 188 189 190 191 192 193
             Just fail_msg -> pprPanic "Core Lint error in newFamInst" $
                              vcat [ fail_msg
                                   , ppr fam_tc
                                   , ppr subst
                                   , ppr tvs'
                                   , ppr cvs'
                                   , ppr lhs'
                                   , ppr rhs' ]
194
       ; return (FamInst { fi_fam      = tyConName fam_tc
195
                         , fi_flavor   = flavor
196 197
                         , fi_tcs      = roughMatchTcs lhs
                         , fi_tvs      = tvs'
198
                         , fi_cvs      = cvs'
Ryan Scott's avatar
Ryan Scott committed
199 200
                         , fi_tys      = lhs'
                         , fi_rhs      = rhs'
201
                         , fi_axiom    = axiom }) }
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
202
  where
203 204
    lhs_kind = tcTypeKind (mkTyConApp fam_tc lhs)
    rhs_kind = tcTypeKind rhs
205 206
    tcv_set  = mkVarSet (tvs ++ cvs)
    pp_ax    = pprCoAxiom axiom
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
207
    CoAxBranch { cab_tvs = tvs
208
               , cab_cvs = cvs
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
209 210 211
               , cab_lhs = lhs
               , cab_rhs = rhs } = coAxiomSingleBranch axiom

212

Austin Seipp's avatar
Austin Seipp committed
213 214 215
{-
************************************************************************
*                                                                      *
216
        Optimised overlap checking for family instances
Austin Seipp's avatar
Austin Seipp committed
217 218
*                                                                      *
************************************************************************
219

Simon Peyton Jones's avatar
Simon Peyton Jones committed
220 221
Note [Checking family instance consistency]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
222 223 224 225 226
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.

227 228 229 230 231 232
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
233 234 235 236

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

237 238 239 240 241 242 243 244
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
Sylvain Henry's avatar
Sylvain Henry committed
245
certain that the modules in our `GHC.Driver.Types.dep_finsts' are consistent.)
246 247 248

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

niteria's avatar
niteria committed
250 251 252 253 254 255 256 257 258 259 260 261 262 263 264 265 266 267 268 269 270 271 272 273 274 275 276 277 278 279 280 281 282 283 284 285 286 287 288 289 290 291 292 293 294 295 296 297 298 299 300
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.
301
-}
302

303 304 305
-- 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].
niteria's avatar
niteria committed
306 307 308
-- We don't need to check the current module, this is done in
-- tcExtendLocalFamInstEnv.
-- See Note [The type family instance consistency story].
309
checkFamInstConsistency :: [Module] -> TcM ()
niteria's avatar
niteria committed
310
checkFamInstConsistency directlyImpMods
311
  = do { (eps, hpt) <- getEpsAndHpt
312
       ; traceTc "checkFamInstConsistency" (ppr directlyImpMods)
313
       ; let { -- Fetch the iface of a given module.  Must succeed as
314 315
               -- all directly imported modules must already have been loaded.
               modIface mod =
316
                 case lookupIfaceByModule hpt (eps_PIT eps) mod of
317 318
                   Nothing    -> panicDoc "FamInst.checkFamInstConsistency"
                                          (ppr mod $$ pprHPT hpt)
319 320
                   Just iface -> iface

niteria's avatar
niteria committed
321 322 323 324 325 326 327
               -- 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 mod =
328
                 if mi_finsts (mi_final_exts (modIface mod)) then mod:deps else deps
niteria's avatar
niteria committed
329 330
                 where
                 deps = dep_finsts . mi_deps . modIface $ mod
331

332
             ; hmiModule     = mi_module . hm_iface
333
             ; hmiFamInstEnv = extendFamInstEnvList emptyFamInstEnv
334
                               . md_fam_insts . hm_details
335
             ; hpt_fam_insts = mkModuleEnv [ (hmiModule hmi, hmiFamInstEnv hmi)
niteria's avatar
niteria committed
336
                                           | hmi <- eltsHpt hpt]
niteria's avatar
niteria committed
337

338
             }
339

340
       ; checkMany hpt_fam_insts modConsistent directlyImpMods
341 342
       }
  where
niteria's avatar
niteria committed
343 344 345 346 347
    -- 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
348 349
      -> TcM ()
    checkMany hpt_fam_insts modConsistent mods = go [] emptyModuleSet mods
niteria's avatar
niteria committed
350 351 352 353 354
      where
      go :: [Module] -- list of consistent modules
         -> ModuleSet -- set of consistent modules, same elements as the
                      -- list above
         -> [Module] -- modules to process
355 356 357 358
         -> TcM ()
      go _ _ [] = return ()
      go consistent consistent_set (mod:mods) = do
        sequence_
niteria's avatar
niteria committed
359 360 361 362 363 364
          [ check hpt_fam_insts m1 m2
          | m1 <- to_check_from_mod
            -- loop over toCheckFromMod first, it's usually smaller,
            -- it may even be empty
          , m2 <- to_check_from_consistent
          ]
365
        go consistent' consistent_set' mods
niteria's avatar
niteria committed
366 367 368 369 370 371 372 373 374 375 376 377 378 379
        where
        mod_deps_consistent =  modConsistent mod
        mod_deps_consistent_set = mkModuleSet mod_deps_consistent
        consistent' = to_check_from_mod ++ consistent
        consistent_set' =
          extendModuleSetList consistent_set to_check_from_mod
        to_check_from_consistent =
          filterOut (`elemModuleSet` mod_deps_consistent_set) consistent
        to_check_from_mod =
          filterOut (`elemModuleSet` consistent_set) 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
380
        --   a set into a non-deterministicly ordered list. Which
niteria's avatar
niteria committed
381 382 383 384 385 386 387 388 389 390 391 392 393 394 395
        --   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 hpt_fam_insts m1 m2
396 397 398 399 400 401 402 403 404 405 406
      = do { env1' <- getFamInsts hpt_fam_insts 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 = famInstEnvSize env1'
                 sizeE2 = famInstEnvSize env2'
                 (env1, env2) = if sizeE1 < sizeE2 then (env1', env2')
                                                   else (env2', env1')
407 408 409 410 411 412
           -- 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.
413
           -- Not so!  Consider the following case:
414
           --
415 416 417 418 419 420 421 422 423 424 425 426
           --   -- 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
427
           -- for F until we have typechecked the family.  Thus, we
428 429 430 431 432 433 434 435 436 437 438 439 440 441 442 443 444 445 446 447 448 449 450 451 452
           -- 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
           --
453 454 455
           -- In fact, it is even necessary to defer for occurrences in
           -- the RHS, because we may test for *compatibility* in event
           -- of an overlap.
456 457 458 459 460 461 462 463 464 465
           --
           -- 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.
466
           --
467
           -- See also Note [Tying the knot]
468
           -- for why we are doing this at all.
469
           ; let check_now = famInstEnvElts env1
470 471
           ; mapM_ (checkForConflicts (emptyFamInstEnv, env2))           check_now
           ; mapM_ (checkForInjectivityConflicts (emptyFamInstEnv,env2)) check_now
Jan Stolarek's avatar
Jan Stolarek committed
472 473
 }

474 475 476 477 478 479 480 481
getFamInsts :: ModuleEnv FamInstEnv -> Module -> TcM FamInstEnv
getFamInsts hpt_fam_insts mod
  | Just env <- lookupModuleEnv hpt_fam_insts mod = return env
  | otherwise = do { _ <- initIfaceTcRn (loadSysInterface doc mod)
                   ; eps <- getEps
                   ; return (expectJust "checkFamInstConsistency" $
                             lookupModuleEnv (eps_mod_fam_inst_env eps) mod) }
  where
482
    doc = ppr mod <+> text "is a family-instance module"
483

Austin Seipp's avatar
Austin Seipp committed
484 485 486
{-
************************************************************************
*                                                                      *
487
        Lookup
Austin Seipp's avatar
Austin Seipp committed
488 489
*                                                                      *
************************************************************************
490

Austin Seipp's avatar
Austin Seipp committed
491
-}
492

493 494 495 496 497 498 499
-- | 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)
500
tcInstNewTyCon_maybe = instNewTyCon_maybe
501

502 503
-- | Like 'tcLookupDataFamInst_maybe', but returns the arguments back if
-- there is no data family to unwrap.
504
-- Returns a Representational coercion
505
tcLookupDataFamInst :: FamInstEnvs -> TyCon -> [TcType]
506
                    -> (TyCon, [TcType], Coercion)
507 508 509
tcLookupDataFamInst fam_inst_envs tc tc_args
  | Just (rep_tc, rep_args, co)
      <- tcLookupDataFamInst_maybe fam_inst_envs tc tc_args
510
  = (rep_tc, rep_args, co)
511
  | otherwise
512
  = (tc, tc_args, mkRepReflCo (mkTyConApp tc tc_args))
513 514 515

tcLookupDataFamInst_maybe :: FamInstEnvs -> TyCon -> [TcType]
                          -> Maybe (TyCon, [TcType], Coercion)
516
-- ^ Converts a data family type (eg F [a]) to its representation type (eg FList a)
517
-- and returns a coercion between the two: co :: F [a] ~R FList a.
518
tcLookupDataFamInst_maybe fam_inst_envs tc tc_args
519 520
  | isDataFamilyTyCon tc
  , match : _ <- lookupFamInstEnv fam_inst_envs tc tc_args
521 522 523 524 525
  , FamInstMatch { fim_instance = rep_fam@(FamInst { fi_axiom = ax
                                                   , fi_cvs   = cvs })
                 , fim_tys      = rep_args
                 , fim_cos      = rep_cos } <- match
  , let rep_tc = dataFamInstRepTyCon rep_fam
526
        co     = mkUnbranchedAxInstCo Representational ax rep_args
527
                                      (mkCoVarCos cvs)
Sylvain Henry's avatar
Sylvain Henry committed
528
  = ASSERT( null rep_cos ) -- See Note [Constrained family instances] in GHC.Core.FamInstEnv
529
    Just (rep_tc, rep_args, co)
530 531 532

  | otherwise
  = Nothing
533

534
-- | 'tcTopNormaliseNewTypeTF_maybe' gets rid of top-level newtypes,
535
-- potentially looking through newtype /instances/.
536
--
537
-- It is only used by the type inference engine (specifically, when
538
-- solving representational equality), and hence it is careful to unwrap
539 540 541 542 543 544 545 546 547
-- 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.
548
--
549 550 551 552
-- 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
553 554 555
tcTopNormaliseNewTypeTF_maybe :: FamInstEnvs
                              -> GlobalRdrEnv
                              -> Type
556
                              -> Maybe ((Bag GlobalRdrElt, TcCoercion), Type)
557 558
tcTopNormaliseNewTypeTF_maybe faminsts rdr_env ty
-- cf. FamInstEnv.topNormaliseType_maybe and Coercion.topNormaliseNewType_maybe
559
  = topNormaliseTypeX stepper plus ty
560
  where
561 562 563 564 565 566
    plus :: (Bag GlobalRdrElt, TcCoercion) -> (Bag GlobalRdrElt, TcCoercion)
         -> (Bag GlobalRdrElt, TcCoercion)
    plus (gres1, co1) (gres2, co2) = ( gres1 `unionBags` gres2
                                     , co1 `mkTransCo` co2 )

    stepper :: NormaliseStepper (Bag GlobalRdrElt, TcCoercion)
567 568 569
    stepper = unwrap_newtype `composeSteppers` unwrap_newtype_instance

    -- For newtype instances we take a double step or nothing, so that
Simon Peyton Jones's avatar
Simon Peyton Jones committed
570
    -- we don't return the representation type of the newtype instance,
571 572 573
    -- which would lead to terrible error messages
    unwrap_newtype_instance rec_nts tc tys
      | Just (tc', tys', co) <- tcLookupDataFamInst_maybe faminsts tc tys
574
      = mapStepResult (\(gres, co1) -> (gres, co `mkTransCo` co1)) $
575 576
        unwrap_newtype rec_nts tc' tys'
      | otherwise = NS_Done
577 578

    unwrap_newtype rec_nts tc tys
579 580 581 582 583 584
      | Just con <- newTyConDataCon_maybe tc
      , Just gre <- lookupGRE_Name rdr_env (dataConName con)
           -- This is where we check that the
           -- data constructor is in scope
      = mapStepResult (\co -> (unitBag gre, co)) $
        unwrapNewTypeStepper rec_nts tc tys
585 586 587 588

      | otherwise
      = NS_Done

Austin Seipp's avatar
Austin Seipp committed
589 590 591
{-
************************************************************************
*                                                                      *
592
        Extending the family instance environment
Austin Seipp's avatar
Austin Seipp committed
593 594 595
*                                                                      *
************************************************************************
-}
596

597 598 599 600
-- 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).
601
tcExtendLocalFamInstEnv :: [FamInst] -> TcM a -> TcM a
602 603 604 605 606 607

-- 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 [] thing_inside = thing_inside

-- Otherwise proceed...
608
tcExtendLocalFamInstEnv fam_insts thing_inside
609 610 611 612 613 614 615
 = 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]
        loadDependentFamInstModules fam_insts

        -- Now add the instances one by one
      ; env <- getGblEnv
616
      ; (inst_env', fam_insts') <- foldlM addLocalFamInst
Jan Stolarek's avatar
Jan Stolarek committed
617 618
                                       (tcg_fam_inst_env env, tcg_fam_insts env)
                                       fam_insts
619

Simon Peyton Jones's avatar
Simon Peyton Jones committed
620
      ; let env' = env { tcg_fam_insts    = fam_insts'
621
                       , tcg_fam_inst_env = inst_env' }
622
      ; setGblEnv env' thing_inside
623
      }
624

625 626 627 628 629 630 631 632 633 634 635 636 637 638 639 640 641 642 643 644 645 646 647 648 649 650 651 652 653 654 655 656 657 658 659
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 fam_insts
 = do { env <- getGblEnv
      ; let this_mod = tcg_mod env
            imports  = tcg_imports env

            want_module mod  -- See Note [Home package family instances]
              | mod == this_mod = False
              | home_fams_only  = moduleUnitId mod == moduleUnitId this_mod
              | otherwise       = True
            home_fams_only = all (nameIsHomePackage this_mod . fi_fam) 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.
-}

660
-- Check that the proposed new instance is OK,
661
-- and then add it to the home inst env
662
-- This must be lazy in the fam_inst arguments, see Note [Lazy axiom match]
Sylvain Henry's avatar
Sylvain Henry committed
663
-- in GHC.Core.FamInstEnv
Jan Stolarek's avatar
Jan Stolarek committed
664 665 666
addLocalFamInst :: (FamInstEnv,[FamInst])
                -> FamInst
                -> TcM (FamInstEnv, [FamInst])
667
addLocalFamInst (home_fie, my_fis) fam_inst
Simon Peyton Jones's avatar
Simon Peyton Jones committed
668 669
        -- home_fie includes home package and this module
        -- my_fies is just the ones from this module
670
  = do { traceTc "addLocalFamInst" (ppr fam_inst)
671

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

675 676
       ; mod <- getModule
       ; traceTc "alfi" (ppr mod)
Simon Peyton Jones's avatar
Simon Peyton Jones committed
677

678 679 680 681 682 683
           -- 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.
Simon Peyton Jones's avatar
Simon Peyton Jones committed
684
       ; eps <- getEps
685 686
       ; let inst_envs = (eps_fam_inst_env eps, home_fie)
             home_fie' = extendFamInstEnv home_fie fam_inst
Simon Peyton Jones's avatar
Simon Peyton Jones committed
687

Jan Stolarek's avatar
Jan Stolarek committed
688
           -- Check for conflicting instance decls and injectivity violations
689 690 691 692 693
       ; ((), no_errs) <- askNoErrs $
         do { checkForConflicts            inst_envs fam_inst
            ; checkForInjectivityConflicts inst_envs fam_inst
            ; checkInjectiveEquation       fam_inst
            }
Jan Stolarek's avatar
Jan Stolarek committed
694

695
       ; if no_errs then
696
            return (home_fie', fam_inst : my_fis)
697
         else
698
            return (home_fie,  my_fis) }
699

Austin Seipp's avatar
Austin Seipp committed
700 701 702
{-
************************************************************************
*                                                                      *
703
        Checking an instance against conflicts with an instance env
Austin Seipp's avatar
Austin Seipp committed
704 705
*                                                                      *
************************************************************************
706 707 708

Check whether a single family instance conflicts with those in two instance
environments (one for the EPS and one for the HPT).
Austin Seipp's avatar
Austin Seipp committed
709
-}
710

711 712
-- | Checks to make sure no two family instances overlap.
checkForConflicts :: FamInstEnvs -> FamInst -> TcM ()
713 714
checkForConflicts inst_envs fam_inst
  = do { let conflicts = lookupFamInstEnvConflicts inst_envs fam_inst
715 716 717 718 719
       ; traceTc "checkForConflicts" $
         vcat [ ppr (map fim_instance conflicts)
              , ppr fam_inst
              -- , ppr inst_envs
         ]
720 721 722
       ; reportConflictInstErr fam_inst conflicts }

checkForInjectivityConflicts :: FamInstEnvs -> FamInst -> TcM ()
Sylvain Henry's avatar
Sylvain Henry committed
723
  -- see Note [Verifying injectivity annotation] in GHC.Core.FamInstEnv, check 1B1.
724 725 726 727 728 729 730 731 732 733
checkForInjectivityConflicts instEnvs famInst
    | isTypeFamilyTyCon tycon   -- as opposed to data family tycon
    , Injective inj <- tyConInjectivityInfo tycon
    = let conflicts = lookupFamInstEnvInjectivityConflicts inj instEnvs famInst in
      reportConflictingInjectivityErrs tycon conflicts (coAxiomSingleBranch (fi_axiom famInst))

    | otherwise
    = return ()

    where tycon = famInstTyCon famInst
734

Jan Stolarek's avatar
Jan Stolarek committed
735 736 737
-- | 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
738 739
-- annotation. This looks only at the one equation; it does not look for
-- interaction between equations. Use checkForInjectivityConflicts for that.
Sylvain Henry's avatar
Sylvain Henry committed
740
-- Does checks (2)-(4) of Note [Verifying injectivity annotation] in GHC.Core.FamInstEnv.
741 742
checkInjectiveEquation :: FamInst -> TcM ()
checkInjectiveEquation famInst
Jan Stolarek's avatar
Jan Stolarek committed
743 744
    | isTypeFamilyTyCon tycon
    -- type family is injective in at least one argument
745
    , Injective inj <- tyConInjectivityInfo tycon = do
746 747
    { dflags <- getDynFlags
    ; let axiom = coAxiomSingleBranch fi_ax
Sylvain Henry's avatar
Sylvain Henry committed
748
          -- see Note [Verifying injectivity annotation] in GHC.Core.FamInstEnv
749
    ; reportInjectivityErrors dflags fi_ax axiom inj
Jan Stolarek's avatar
Jan Stolarek committed
750 751 752 753
    }

    -- if there was no injectivity annotation or tycon does not represent a
    -- type family we report no conflicts
754 755 756
    | otherwise
    = return ()

Jan Stolarek's avatar
Jan Stolarek committed
757
    where tycon = famInstTyCon famInst
758
          fi_ax = fi_axiom famInst
Jan Stolarek's avatar
Jan Stolarek committed
759

760 761 762
-- | Report a list of injectivity errors together with their source locations.
-- Looks only at one equation; does not look for conflicts *among* equations.
reportInjectivityErrors
763 764
   :: DynFlags
   -> CoAxiom br   -- ^ Type family for which we generate errors
Jan Stolarek's avatar
Jan Stolarek committed
765 766
   -> CoAxBranch   -- ^ Currently checked equation (represented by axiom)
   -> [Bool]       -- ^ Injectivity annotation
767 768
   -> TcM ()
reportInjectivityErrors dflags fi_ax axiom inj
Jan Stolarek's avatar
Jan Stolarek committed
769
  = ASSERT2( any id inj, text "No injective type variables" )
770 771 772 773 774 775 776 777 778 779 780 781 782 783
    do let lhs             = coAxBranchLHS axiom
           rhs             = coAxBranchRHS axiom
           fam_tc          = coAxiomTyCon fi_ax
           (unused_inj_tvs, unused_vis, undec_inst_flag)
                           = unusedInjTvsInRHS dflags fam_tc lhs rhs
           inj_tvs_unused  = not $ isEmptyVarSet unused_inj_tvs
           tf_headed       = isTFHeaded rhs
           bare_variables  = bareTvInRHSViolated lhs rhs
           wrong_bare_rhs  = not $ null bare_variables

       when inj_tvs_unused $ reportUnusedInjectiveVarsErr fam_tc unused_inj_tvs
                                                          unused_vis undec_inst_flag axiom
       when tf_headed      $ reportTfHeadedErr            fam_tc axiom
       when wrong_bare_rhs $ reportBareVariableInRHSErr   fam_tc bare_variables axiom
Jan Stolarek's avatar
Jan Stolarek committed
784

Jan Stolarek's avatar
Jan Stolarek committed
785 786
-- | Is type headed by a type family application?
isTFHeaded :: Type -> Bool
787
-- See Note [Verifying injectivity annotation], case 3.
788
isTFHeaded ty | Just ty' <- coreView ty
Jan Stolarek's avatar
Jan Stolarek committed
789 790 791
              = isTFHeaded ty'
isTFHeaded ty | (TyConApp tc args) <- ty
              , isTypeFamilyTyCon tc
792
              = args `lengthIs` tyConArity tc
Jan Stolarek's avatar
Jan Stolarek committed
793 794 795 796 797 798
isTFHeaded _  = 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]
799
-- See Note [Verifying injectivity annotation], case 2.
Jan Stolarek's avatar
Jan Stolarek committed
800 801 802 803
bareTvInRHSViolated pats rhs | isTyVarTy rhs
   = filter (not . isTyVarTy) pats
bareTvInRHSViolated _ _ = []

804 805 806 807 808 809 810 811 812 813 814 815 816 817 818 819 820 821 822 823 824 825 826 827 828 829 830 831 832 833 834 835 836 837 838 839 840 841 842 843 844 845 846 847 848 849 850 851 852 853 854 855 856 857 858 859 860 861 862 863 864 865 866 867 868 869 870 871 872 873 874 875 876 877 878 879 880 881 882 883 884 885 886
------------------------------------------------------------------
-- 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
887
have not yet looked at the RHS.
888 889 890 891 892 893 894 895 896 897 898 899 900 901 902 903 904 905 906 907 908 909 910 911 912 913 914 915 916 917 918 919 920 921 922

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
923 924
                     , Bool   -- True <=> one or more variable is used invisibly
                     , Bool ) -- True <=> suggest -XUndecidableInstances
Sylvain Henry's avatar
Sylvain Henry committed
925
-- See Note [Verifying injectivity annotation] in GHC.Core.FamInstEnv.
926 927 928 929 930 931 932 933 934 935 936 937 938 939 940 941 942 943 944 945 946 947 948 949 950 951 952 953 954 955 956 957 958 959 960
-- 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 dflags tycon@(tyConInjectivityInfo -> Injective inj_list) lhs rhs =
  -- Note [Coverage condition for injective type families], step 5
  (bad_vars, any_invisible, suggest_undec)
    where
      undec_inst = xopt LangExt.UndecidableInstances dflags

      inj_lhs = filterByList inj_list lhs
      lhs_vars = tyCoVarsOfTypes inj_lhs

      rhs_inj_vars = fvVarSet $ injectiveVarsOfType undec_inst rhs

      bad_vars = lhs_vars `minusVarSet` rhs_inj_vars

      any_bad = not $ isEmptyVarSet bad_vars

      invis_vars = fvVarSet $ invisibleVarsOfTypes [mkTyConApp tycon lhs, rhs]

      any_invisible = any_bad && (bad_vars `intersectsVarSet` invis_vars)
      suggest_undec = any_bad &&
                      not undec_inst &&
                      (lhs_vars `subVarSet` fvVarSet (injectiveVarsOfType True rhs))

-- When the type family is not injective in any arguments
unusedInjTvsInRHS _ _ _ _ = (emptyVarSet, False, False)

---------------------------------------
-- Producing injectivity error messages
---------------------------------------
Jan Stolarek's avatar
Jan Stolarek committed
961

962 963 964 965 966 967 968 969 970 971 972 973 974 975
-- | 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 _ [] _ = return ()
reportConflictingInjectivityErrs fam_tc (confEqn1:_) tyfamEqn
  = addErrs [buildInjectivityError fam_tc herald (confEqn1 :| [tyfamEqn])]
  where
    herald = text "Type family equation right-hand sides overlap; this violates" $$
             text "the family's injectivity annotation:"

-- | Injectivity error herald common to all injectivity errors.
injectivityErrorHerald :: SDoc
injectivityErrorHerald =
  text "Type family equation violates the family's injectivity annotation."
Jan Stolarek's avatar
Jan Stolarek committed
976

977 978

-- | Report error message for equation with injective type variables unused in
979
-- the RHS. Note [Coverage condition for injective type families], step 6
980 981 982 983 984 985 986 987 988 989 990 991 992
reportUnusedInjectiveVarsErr :: TyCon
                             -> TyVarSet
                             -> Bool   -- True <=> print invisible arguments
                             -> Bool   -- True <=> suggest -XUndecidableInstances
                             -> CoAxBranch
                             -> TcM ()
reportUnusedInjectiveVarsErr fam_tc tvs has_kinds undec_inst tyfamEqn
  = let (loc, doc) = buildInjectivityError fam_tc
                                  (injectivityErrorHerald $$
                                   herald $$
                                   text "In the type family equation:")
                                  (tyfamEqn :| [])
    in addErrAt loc (pprWithExplicitKindsWhen has_kinds doc)
Jan Stolarek's avatar
Jan Stolarek committed
993
    where
994
      herald = sep [ what <+> text "variable" <>
Tobias Dammers's avatar
Tobias Dammers committed
995
                  pluralVarSet tvs <+> pprVarSet tvs (pprQuotedList . scopedSort)
996
                , text "cannot be inferred from the right-hand side." ]
997
               $$ extra
998 999 1000 1001 1002 1003 1004

      what | has_kinds = text "Type/kind"
           | otherwise = text "Type"

      extra | undec_inst = text "Using UndecidableInstances might help"
            | otherwise  = empty

1005
-- | Report error message for equation that has a type family call at the top
Jan Stolarek's avatar
Jan Stolarek committed
1006
-- level of RHS
1007 1008 1009 1010 1011 1012 1013 1014 1015
reportTfHeadedErr :: TyCon -> CoAxBranch -> TcM ()
reportTfHeadedErr fam_tc branch
  = addErrs [buildInjectivityError fam_tc
               (injectivityErrorHerald $$
                 text "RHS of injective type family equation cannot" <+>
                 text "be a type family:")
               (branch :| [])]

-- | Report error message for equation that has a bare type variable in the RHS
Jan Stolarek's avatar
Jan Stolarek committed
1016
-- but LHS pattern is not a bare type variable.
1017 1018 1019 1020
reportBareVariableInRHSErr :: TyCon -> [Type] -> CoAxBranch -> TcM ()
reportBareVariableInRHSErr fam_tc tys branch
  = addErrs [buildInjectivityError fam_tc
                 (injectivityErrorHerald $$
Jan Stolarek's avatar
Jan Stolarek committed
1021 1022 1023
                  text "RHS of injective type family equation is a bare" <+>
                  text "type variable" $$
                  text "but these LHS type and kind patterns are not bare" <+>
1024 1025 1026 1027 1028 1029 1030 1031
                  text "variables:" <+> pprQuotedList tys)
                 (branch :| [])]

buildInjectivityError :: TyCon -> SDoc -> NonEmpty CoAxBranch -> (SrcSpan, SDoc)
buildInjectivityError fam_tc herald (eqn1 :| rest_eqns)
  = ( coAxBranchSpan eqn1
    , hang herald
         2 (vcat (map (pprCoAxBranchUser fam_tc) (eqn1 : rest_eqns))) )
Jan Stolarek's avatar
Jan Stolarek committed
1032

1033 1034 1035 1036 1037
reportConflictInstErr :: FamInst -> [FamInstMatch] -> TcRn ()
reportConflictInstErr _ []
  = return ()  -- No conflicts
reportConflictInstErr fam_inst (match1 : _)
  | FamInstMatch { fim_instance = conf_inst } <- match1
1038
  , let sorted  = sortBy (SrcLoc.leftmost_smallest `on` getSpan) [fam_inst, conf_inst]
1039 1040 1041 1042 1043 1044 1045
        fi1     = head sorted
        span    = coAxBranchSpan (coAxiomSingleBranch (famInstAxiom fi1))
  = setSrcSpan span $ addErr $
    hang (text "Conflicting family instance declarations:")
       2 (vcat [ pprCoAxBranchUser (coAxiomTyCon ax) (coAxiomSingleBranch ax)
               | fi <- sorted
               , let ax = famInstAxiom fi ])
1046
 where
1047 1048
   getSpan = getSrcSpan . famInstAxiom
   -- The sortBy just arranges that instances are displayed in order
1049 1050
   -- of source location, which reduced wobbling in error messages,
   -- and is better for users
1051

1052
tcGetFamInstEnvs :: TcM FamInstEnvs
1053 1054
-- Gets both the external-package inst-env
-- and the home-pkg inst env (includes module being compiled)
1055
tcGetFamInstEnvs
1056
  = do { eps <- getEps; env <- getGblEnv
1057
       ; return (eps_fam_inst_env eps, tcg_fam_inst_env env) }