FamInstEnv.hs 63.6 KB
Newer Older
1 2 3
-- (c) The University of Glasgow 2006
--
-- FamInstEnv: Type checked family instance declarations
4

eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
5
{-# LANGUAGE CPP, GADTs, ScopedTypeVariables #-}
6 7 8

module FamInstEnv (
        FamInst(..), FamFlavor(..), famInstAxiom, famInstTyCon, famInstRHS,
Simon Peyton Jones's avatar
Simon Peyton Jones committed
9
        famInstsRepTyCons, famInstRepTyCon_maybe, dataFamInstRepTyCon,
10
        pprFamInst, pprFamInsts,
11
        mkImportedFamInst,
12

Simon Peyton Jones's avatar
Simon Peyton Jones committed
13 14
        FamInstEnvs, FamInstEnv, emptyFamInstEnv, emptyFamInstEnvs,
        extendFamInstEnv, deleteFromFamInstEnv, extendFamInstEnvList,
Simon Peyton Jones's avatar
Simon Peyton Jones committed
15
        identicalFamInstHead, famInstEnvElts, familyInstances,
16

17 18
        -- * CoAxioms
        mkCoAxBranch, mkBranchedCoAxiom, mkUnbranchedCoAxiom, mkSingleCoAxiom,
Simon Peyton Jones's avatar
Simon Peyton Jones committed
19
        mkNewTypeCoAxiom,
20 21

        FamInstMatch(..),
Jan Stolarek's avatar
Jan Stolarek committed
22 23 24 25 26 27
        lookupFamInstEnv, lookupFamInstEnvConflicts, lookupFamInstEnvByTyCon,

        isDominatedBy, apartnessCheck,

        -- Injectivity
        InjectivityCheckResult(..),
Jan Stolarek's avatar
Jan Stolarek committed
28
        lookupFamInstEnvInjectivityConflicts, injectiveBranches,
Simon Peyton Jones's avatar
Simon Peyton Jones committed
29

30
        -- Normalisation
31
        topNormaliseType, topNormaliseType_maybe,
32
        normaliseType, normaliseTcApp,
33
        reduceTyFamApp_maybe,
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
34 35

        -- Flattening
36
        flattenTys
37 38 39 40
    ) where

#include "HsVersions.h"

41
import Unify
42
import Type
43
import TyCoRep
44
import TyCon
45
import Coercion
46
import CoAxiom
47
import VarSet
Simon Peyton Jones's avatar
Simon Peyton Jones committed
48
import VarEnv
49
import Name
50
import PrelNames ( eqPrimTyConKey )
51
import UniqFM
52
import Outputable
TomSchrijvers's avatar
TomSchrijvers committed
53
import Maybes
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
54 55
import TrieMap
import Unique
TomSchrijvers's avatar
TomSchrijvers committed
56
import Util
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
57
import Var
58 59
import Pair
import SrcLoc
60
import FastString
61 62
import MonadUtils
import Control.Monad
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
63
import Data.Function ( on )
Simon Peyton Jones's avatar
Simon Peyton Jones committed
64
import Data.List( mapAccumL )
65

66 67 68
{-
************************************************************************
*                                                                      *
69
          Type checked family instance heads
70 71
*                                                                      *
************************************************************************
72

73 74 75 76 77 78 79 80
Note [FamInsts and CoAxioms]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~
* CoAxioms and FamInsts are just like
  DFunIds  and ClsInsts

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

* A FamInst is a Haskell source-language thing, corresponding
Simon Peyton Jones's avatar
Simon Peyton Jones committed
81
  to a type/data family instance declaration.
82 83 84
    - The FamInst contains a CoAxiom, which is the evidence
      for the instance

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

89
data FamInst  -- See Note [FamInsts and CoAxioms]
Jan Stolarek's avatar
Jan Stolarek committed
90 91 92
  = FamInst { fi_axiom  :: CoAxiom Unbranched -- The new coercion axiom
                                              -- introduced by this family
                                              -- instance
Simon Peyton Jones's avatar
Simon Peyton Jones committed
93 94 95 96 97 98
                 -- INVARIANT: apart from freshening (see below)
                 --    fi_tvs = cab_tvs of the (single) axiom branch
                 --    fi_cvs = cab_cvs ...ditto...
                 --    fi_tys = cab_lhs ...ditto...
                 --    fi_rhs = cab_rhs ...ditto...

99 100
            , fi_flavor :: FamFlavor

Simon Peyton Jones's avatar
Simon Peyton Jones committed
101
            -- Everything below here is a redundant,
102
            -- cached version of the two things above
Simon Peyton Jones's avatar
Simon Peyton Jones committed
103
            -- except that the TyVars are freshened
104 105 106 107 108 109 110
            , fi_fam   :: Name          -- Family name

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

Jan Stolarek's avatar
Jan Stolarek committed
111
            -- Used for "proper matching"; ditto
112
            , fi_tvs :: [TyVar]      -- Template tyvars for full match
Simon Peyton Jones's avatar
Simon Peyton Jones committed
113
            , fi_cvs :: [CoVar]      -- Template covars for full match
114 115
                 -- Like ClsInsts, these variables are always fresh
                 -- See Note [Template tyvars are fresh] in InstEnv
116 117 118 119

            , fi_tys    :: [Type]       --   The LHS type patterns
            -- May be eta-reduced; see Note [Eta reduction for data families]

120
            , fi_rhs :: Type         --   the RHS, with its freshened vars
121
            }
122

Simon Peyton Jones's avatar
Simon Peyton Jones committed
123
data FamFlavor
124 125
  = SynFamilyInst         -- A synonym family
  | DataFamilyInst TyCon  -- A data family, with its representation TyCon
126

127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159 160 161 162
{- Note [Eta reduction for data families]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Consider this
   data family T a b :: *
   newtype instance T Int a = MkT (IO a) deriving( Monad )
We'd like this to work.

From the 'newtype instance' you might think we'd get:
   newtype TInt a = MkT (IO a)
   axiom ax1 a :: T Int a ~ TInt a   -- The newtype-instance part
   axiom ax2 a :: TInt a ~ IO a      -- The newtype part

But now what can we do?  We have this problem
   Given:   d  :: Monad IO
   Wanted:  d' :: Monad (T Int) = d |> ????
What coercion can we use for the ???

Solution: eta-reduce both axioms, thus:
   axiom ax1 :: T Int ~ TInt
   axiom ax2 :: TInt ~ IO
Now
   d' = d |> Monad (sym (ax2 ; ax1))

This eta reduction happens for data instances as well as newtype
instances. Here we want to eta-reduce the data family axiom.
All this is done in TcInstDcls.tcDataFamInstDecl.

See also Note [Newtype eta] in TyCon.

Bottom line:
  For a FamInst with fi_flavour = DataFamilyInst rep_tc,
  - fi_tvs may be shorter than tyConTyVars of rep_tc
  - fi_tys may be shorter than tyConArity of the family tycon
       i.e. LHS is unsaturated
  - fi_rhs will be (rep_tc fi_tvs)
       i.e. RHS is un-saturated
Simon Peyton Jones's avatar
Simon Peyton Jones committed
163 164 165

  But when fi_flavour = SynFamilyInst,
  - fi_tys has the exact arity of the family tycon
166 167
-}

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

172 173 174 175
-- Split the left-hand side of the FamInst
famInstSplitLHS :: FamInst -> (TyCon, [Type])
famInstSplitLHS (FamInst { fi_axiom = axiom, fi_tys = lhs })
  = (coAxiomTyCon axiom, lhs)
176

177 178 179
-- Get the RHS of the FamInst
famInstRHS :: FamInst -> Type
famInstRHS = fi_rhs
180

181 182 183
-- Get the family TyCon of the FamInst
famInstTyCon :: FamInst -> TyCon
famInstTyCon = coAxiomTyCon . famInstAxiom
184

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

-- Extracts the TyCon for this *data* (or newtype) instance
190
famInstRepTyCon_maybe :: FamInst -> Maybe TyCon
Simon Peyton Jones's avatar
Simon Peyton Jones committed
191
famInstRepTyCon_maybe fi
192 193 194 195
  = case fi_flavor fi of
       DataFamilyInst tycon -> Just tycon
       SynFamilyInst        -> Nothing

196
dataFamInstRepTyCon :: FamInst -> TyCon
Simon Peyton Jones's avatar
Simon Peyton Jones committed
197
dataFamInstRepTyCon fi
198 199 200
  = case fi_flavor fi of
       DataFamilyInst tycon -> tycon
       SynFamilyInst        -> pprPanic "dataFamInstRepTyCon" (ppr fi)
201

202 203 204
{-
************************************************************************
*                                                                      *
205
        Pretty printing
206 207 208
*                                                                      *
************************************************************************
-}
209

210
instance NamedThing FamInst where
211
   getName = coAxiomName . fi_axiom
212

213
instance Outputable FamInst where
214 215 216
   ppr = pprFamInst

-- Prints the FamInst as a family instance declaration
217 218
-- NB: FamInstEnv.pprFamInst is used only for internal, debug printing
--     See pprTyThing.pprFamInst for printing for the user
219 220
pprFamInst :: FamInst -> SDoc
pprFamInst famInst
221
  = hang (pprFamInstHdr famInst) 2 (ifPprDebug debug_stuff)
222
  where
223
    ax = fi_axiom famInst
224 225 226 227
    debug_stuff = vcat [ text "Coercion axiom:" <+> ppr ax
                       , text "Tvs:" <+> ppr (fi_tvs famInst)
                       , text "LHS:" <+> ppr (fi_tys famInst)
                       , text "RHS:" <+> ppr (fi_rhs famInst) ]
228 229 230

pprFamInstHdr :: FamInst -> SDoc
pprFamInstHdr fi@(FamInst {fi_flavor = flavor})
231
  = pprTyConSort <+> pp_instance <+> pp_head
232
  where
Simon Peyton Jones's avatar
Simon Peyton Jones committed
233
    -- For *associated* types, say "type T Int = blah"
234
    -- For *top level* type instances, say "type instance T Int = blah"
Simon Peyton Jones's avatar
Simon Peyton Jones committed
235
    pp_instance
236
      | isTyConAssoc fam_tc = empty
237
      | otherwise           = text "instance"
238

239 240 241 242 243 244 245 246 247 248 249 250 251
    (fam_tc, etad_lhs_tys) = famInstSplitLHS fi
    vanilla_pp_head = pprTypeApp fam_tc etad_lhs_tys

    pp_head | DataFamilyInst rep_tc <- flavor
            , isAlgTyCon rep_tc
            , let extra_tvs = dropList etad_lhs_tys (tyConTyVars rep_tc)
            , not (null extra_tvs)
            = getPprStyle $ \ sty ->
              if debugStyle sty
              then vanilla_pp_head   -- With -dppr-debug just show it as-is
              else pprTypeApp fam_tc (etad_lhs_tys ++ mkTyVarTys extra_tvs)
                     -- Without -dppr-debug, eta-expand
                     -- See Trac #8674
252 253 254
                     -- (This is probably over the top now that we use this
                     --  only for internal debug printing; PprTyThing.pprFamInst
                     --  is used for user-level printing.)
255 256 257
            | otherwise
            = vanilla_pp_head

258
    pprTyConSort = case flavor of
259
                     SynFamilyInst        -> text "type"
260
                     DataFamilyInst tycon
261 262 263 264
                       | isDataTyCon     tycon -> text "data"
                       | isNewTyCon      tycon -> text "newtype"
                       | isAbstractTyCon tycon -> text "data"
                       | otherwise             -> text "WEIRD" <+> ppr tycon
265 266

pprFamInsts :: [FamInst] -> SDoc
267
pprFamInsts finsts = vcat (map pprFamInst finsts)
268

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

286
-- Make a family instance representation from the information found in an
287
-- interface file.  In particular, we get the rough match info from the iface
288
-- (instead of computing it here).
289
mkImportedFamInst :: Name               -- Name of the family
290 291 292 293
                  -> [Maybe Name]       -- Rough match info
                  -> CoAxiom Unbranched -- Axiom introduced
                  -> FamInst            -- Resulting family instance
mkImportedFamInst fam mb_tcs axiom
294
  = FamInst {
295 296 297
      fi_fam    = fam,
      fi_tcs    = mb_tcs,
      fi_tvs    = tvs,
298
      fi_cvs    = cvs,
299 300 301 302
      fi_tys    = tys,
      fi_rhs    = rhs,
      fi_axiom  = axiom,
      fi_flavor = flavor }
Simon Peyton Jones's avatar
Simon Peyton Jones committed
303
  where
304
     -- See Note [Lazy axiom match]
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
305 306
     ~(CoAxBranch { cab_lhs = tys
                  , cab_tvs = tvs
307
                  , cab_cvs = cvs
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
308
                  , cab_rhs = rhs }) = coAxiomSingleBranch axiom
309 310 311

         -- Derive the flavor for an imported FamInst rather disgustingly
         -- Maybe we should store it in the IfaceFamInst?
312 313 314 315 316 317
     flavor = case splitTyConApp_maybe rhs of
                Just (tc, _)
                  | Just ax' <- tyConFamilyCoercion_maybe tc
                  , ax' == axiom
                  -> DataFamilyInst tc
                _ -> SynFamilyInst
318

319 320 321
{-
************************************************************************
*                                                                      *
322
                FamInstEnv
323 324
*                                                                      *
************************************************************************
325

326
Note [FamInstEnv]
327
~~~~~~~~~~~~~~~~~
328 329 330 331 332 333 334
A FamInstEnv maps a family name to the list of known instances for that family.

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

Gabor Greif's avatar
Gabor Greif committed
335
Nevertheless it is still useful to have data families in the FamInstEnv:
336 337 338 339 340 341

 - For finding overlaps and conflicts

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

Simon Peyton Jones's avatar
Simon Peyton Jones committed
342
 - In standalone deriving instance Eq (T [Int]) we need to find the
343
   representation type for T [Int]
344

345 346 347 348 349 350 351 352 353 354 355 356 357 358 359
Note [Varying number of patterns for data family axioms]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
For data families, the number of patterns may vary between instances.
For example
   data family T a b
   data instance T Int a = T1 a | T2
   data instance T Bool [a] = T3 a

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

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

Simon Peyton Jones's avatar
Simon Peyton Jones committed
360 361
These two axioms for T, one with one pattern, one with two;
see Note [Eta reduction for data families]
362
-}
363

364
type FamInstEnv = UniqFM FamilyInstEnv  -- Maps a family to its instances
365
     -- See Note [FamInstEnv]
366

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

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

373
instance Outputable FamilyInstEnv where
374
  ppr (FamIE fs) = text "FamIE" <+> vcat (map ppr fs)
375

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

380 381 382
emptyFamInstEnvs :: (FamInstEnv, FamInstEnv)
emptyFamInstEnvs = (emptyFamInstEnv, emptyFamInstEnv)

383 384 385
emptyFamInstEnv :: FamInstEnv
emptyFamInstEnv = emptyUFM

386
famInstEnvElts :: FamInstEnv -> [FamInst]
387
famInstEnvElts fi = [elt | FamIE elts <- eltsUFM fi, elt <- elts]
388

389
familyInstances :: (FamInstEnv, FamInstEnv) -> TyCon -> [FamInst]
390 391 392 393
familyInstances (pkg_fie, home_fie) fam
  = get home_fie ++ get pkg_fie
  where
    get env = case lookupUFM env fam of
394
                Just (FamIE insts) -> insts
395
                Nothing                      -> []
396

397
extendFamInstEnvList :: FamInstEnv -> [FamInst] -> FamInstEnv
398 399
extendFamInstEnvList inst_env fis = foldl extendFamInstEnv inst_env fis

400
extendFamInstEnv :: FamInstEnv -> FamInst -> FamInstEnv
Simon Peyton Jones's avatar
Simon Peyton Jones committed
401 402
extendFamInstEnv inst_env
                 ins_item@(FamInst {fi_fam = cls_nm})
403
  = addToUFM_C add inst_env cls_nm (FamIE [ins_item])
404
  where
405
    add (FamIE items) _ = FamIE (ins_item:items)
406

407
deleteFromFamInstEnv :: FamInstEnv -> FamInst -> FamInstEnv
408
-- Used only for overriding in GHCi
Simon Peyton Jones's avatar
Simon Peyton Jones committed
409 410 411 412
deleteFromFamInstEnv inst_env fam_inst@(FamInst {fi_fam = fam_nm})
 = adjustUFM adjust inst_env fam_nm
 where
   adjust :: FamilyInstEnv -> FamilyInstEnv
413
   adjust (FamIE items)
414
     = FamIE (filterOut (identicalFamInstHead fam_inst) items)
Simon Peyton Jones's avatar
Simon Peyton Jones committed
415

416 417
identicalFamInstHead :: FamInst -> FamInst -> Bool
-- ^ True when the LHSs are identical
Simon Peyton Jones's avatar
Simon Peyton Jones committed
418
-- Used for overriding in GHCi
419
identicalFamInstHead (FamInst { fi_axiom = ax1 }) (FamInst { fi_axiom = ax2 })
420
  =  coAxiomTyCon ax1 == coAxiomTyCon ax2
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
421 422
  && numBranches brs1 == numBranches brs2
  && and ((zipWith identical_branch `on` fromBranches) brs1 brs2)
423 424 425 426 427
  where
    brs1 = coAxiomBranches ax1
    brs2 = coAxiomBranches ax2

    identical_branch br1 br2
428 429
      =  isJust (tcMatchTys lhs1 lhs2)
      && isJust (tcMatchTys lhs2 lhs1)
430 431 432
      where
        lhs1 = coAxBranchLHS br1
        lhs2 = coAxBranchLHS br2
433

434 435 436
{-
************************************************************************
*                                                                      *
437
                Compatibility
438 439
*                                                                      *
************************************************************************
440

eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
441 442 443 444 445 446 447 448 449 450 451 452
Note [Apartness]
~~~~~~~~~~~~~~~~
In dealing with closed type families, we must be able to check that one type
will never reduce to another. This check is called /apartness/. The check
is always between a target (which may be an arbitrary type) and a pattern.
Here is how we do it:

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

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

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

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

463
type family F a where
464 465 466 467 468 469
  F Int = Bool
  F a   = Int

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

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

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

As another example, consider this:

Jan Stolarek's avatar
Jan Stolarek committed
484
type family G x where
485 486 487 488 489 490 491 492 493
  G Int = Bool
  G a   = Double

type family H y
-- no instances

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

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

497 498 499
type family J a where
  J Int = Int
  J a   = a
500

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

504 505 506
So, the rule is this: when looking up a branch in a closed type family, we
find a branch that matches the target, but then we make sure that the target
is apart from every previous *incompatible* branch. We don't check the
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
507
branches that are compatible with the matching branch, because they are either
508
irrelevant (clause 1 of compatible) or benign (clause 2 of compatible).
509
-}
510

511
-- See Note [Compatibility]
512 513 514
compatibleBranches :: CoAxBranch -> CoAxBranch -> Bool
compatibleBranches (CoAxBranch { cab_lhs = lhs1, cab_rhs = rhs1 })
                   (CoAxBranch { cab_lhs = lhs2, cab_rhs = rhs2 })
Simon Peyton Jones's avatar
Simon Peyton Jones committed
515
  = case tcUnifyTysFG (const BindMe) lhs1 lhs2 of
516 517 518 519 520 521
      SurelyApart -> True
      Unifiable subst
        | Type.substTy subst rhs1 `eqType` Type.substTy subst rhs2
        -> True
      _ -> False

Jan Stolarek's avatar
Jan Stolarek committed
522 523 524 525 526 527 528 529 530 531 532 533 534 535 536 537 538 539 540 541 542 543 544 545 546 547 548 549 550 551 552 553 554 555 556 557 558 559
-- | Result of testing two type family equations for injectiviy.
data InjectivityCheckResult
   = InjectivityAccepted
    -- ^ Either RHSs are distinct or unification of RHSs leads to unification of
    -- LHSs
   | InjectivityUnified CoAxBranch CoAxBranch
    -- ^ RHSs unify but LHSs don't unify under that substitution.  Relevant for
    -- closed type families where equation after unification might be
    -- overlpapped (in which case it is OK if they don't unify).  Constructor
    -- stores axioms after unification.

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

560 561
-- takes a CoAxiom with unknown branch incompatibilities and computes
-- the compatibilities
562
-- See Note [Storing compatibility] in CoAxiom
Simon Peyton Jones's avatar
Simon Peyton Jones committed
563 564 565
computeAxiomIncomps :: [CoAxBranch] -> [CoAxBranch]
computeAxiomIncomps branches
  = snd (mapAccumL go [] branches)
566
  where
Simon Peyton Jones's avatar
Simon Peyton Jones committed
567 568 569 570 571
    go :: [CoAxBranch] -> CoAxBranch -> ([CoAxBranch], CoAxBranch)
    go prev_brs cur_br
       = (cur_br : prev_brs, new_br)
       where
         new_br = cur_br { cab_incomps = mk_incomps prev_brs cur_br }
572

Simon Peyton Jones's avatar
Simon Peyton Jones committed
573 574 575
    mk_incomps :: [CoAxBranch] -> CoAxBranch -> [CoAxBranch]
    mk_incomps prev_brs cur_br
       = filter (not . compatibleBranches cur_br) prev_brs
576

577 578 579
{-
************************************************************************
*                                                                      *
580
           Constructing axioms
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
581
    These functions are here because tidyType / tcUnifyTysFG
582
    are not available in CoAxiom
Simon Peyton Jones's avatar
Simon Peyton Jones committed
583 584

    Also computeAxiomIncomps is too sophisticated for CoAxiom
585 586
*                                                                      *
************************************************************************
587 588 589 590 591 592

Note [Tidy axioms when we build them]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
We print out axioms and don't want to print stuff like
    F k k a b = ...
Instead we must tidy those kind variables.  See Trac #7524.
593
-}
594

595
-- all axiom roles are Nominal, as this is only used with type families
596
mkCoAxBranch :: [TyVar] -- original, possibly stale, tyvars
597
             -> [CoVar] -- possibly stale covars
598 599
             -> [Type]  -- LHS patterns
             -> Type    -- RHS
Simon Peyton Jones's avatar
Simon Peyton Jones committed
600
             -> [Role]
601 602
             -> SrcSpan
             -> CoAxBranch
Simon Peyton Jones's avatar
Simon Peyton Jones committed
603
mkCoAxBranch tvs cvs lhs rhs roles loc
604
  = CoAxBranch { cab_tvs     = tvs1
605
               , cab_cvs     = cvs1
606
               , cab_lhs     = tidyTypes env lhs
Simon Peyton Jones's avatar
Simon Peyton Jones committed
607
               , cab_roles   = roles
608 609
               , cab_rhs     = tidyType  env rhs
               , cab_loc     = loc
610 611
               , cab_incomps = placeHolderIncomps }
  where
612 613
    (env1, tvs1) = tidyTyCoVarBndrs emptyTidyEnv tvs
    (env,  cvs1) = tidyTyCoVarBndrs env1         cvs
614 615 616 617 618 619
    -- See Note [Tidy axioms when we build them]

-- all of the following code is here to avoid mutual dependencies with
-- Coercion
mkBranchedCoAxiom :: Name -> TyCon -> [CoAxBranch] -> CoAxiom Branched
mkBranchedCoAxiom ax_name fam_tc branches
Simon Peyton Jones's avatar
Simon Peyton Jones committed
620
  = CoAxiom { co_ax_unique   = nameUnique ax_name
621 622
            , co_ax_name     = ax_name
            , co_ax_tc       = fam_tc
623
            , co_ax_role     = Nominal
624
            , co_ax_implicit = False
Simon Peyton Jones's avatar
Simon Peyton Jones committed
625
            , co_ax_branches = manyBranches (computeAxiomIncomps branches) }
626 627 628 629 630 631

mkUnbranchedCoAxiom :: Name -> TyCon -> CoAxBranch -> CoAxiom Unbranched
mkUnbranchedCoAxiom ax_name fam_tc branch
  = CoAxiom { co_ax_unique   = nameUnique ax_name
            , co_ax_name     = ax_name
            , co_ax_tc       = fam_tc
632
            , co_ax_role     = Nominal
633
            , co_ax_implicit = False
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
634
            , co_ax_branches = unbranched (branch { cab_incomps = [] }) }
635

636
mkSingleCoAxiom :: Role -> Name
637
                -> [TyVar] -> [CoVar] -> TyCon -> [Type] -> Type
638 639 640 641
                -> CoAxiom Unbranched
-- Make a single-branch CoAxiom, incluidng making the branch itself
-- Used for both type family (Nominal) and data family (Representational)
-- axioms, hence passing in the Role
642
mkSingleCoAxiom role ax_name tvs cvs fam_tc lhs_tys rhs_ty
643 644 645
  = CoAxiom { co_ax_unique   = nameUnique ax_name
            , co_ax_name     = ax_name
            , co_ax_tc       = fam_tc
646
            , co_ax_role     = role
647
            , co_ax_implicit = False
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
648
            , co_ax_branches = unbranched (branch { cab_incomps = [] }) }
649
  where
Simon Peyton Jones's avatar
Simon Peyton Jones committed
650 651 652 653 654 655 656 657 658 659 660 661 662 663 664 665 666 667 668 669
    branch = mkCoAxBranch tvs cvs lhs_tys rhs_ty
                          (map (const Nominal) tvs)
                          (getSrcSpan ax_name)

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

671 672 673
{-
************************************************************************
*                                                                      *
674
                Looking up a family instance
675 676
*                                                                      *
************************************************************************
677 678 679 680 681 682 683 684 685 686 687 688 689 690 691 692 693

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

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

  data instance T [a] = ..

desugared to

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

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

696
-- when matching a type family application, we get a FamInst,
697 698
-- and the list of types the axiom should be applied to
data FamInstMatch = FamInstMatch { fim_instance :: FamInst
699
                                 , fim_tys      :: [Type]
700
                                 , fim_cos      :: [Coercion]
701
                                 }
702
  -- See Note [Over-saturated matches]
703 704 705

instance Outputable FamInstMatch where
  ppr (FamInstMatch { fim_instance = inst
706 707
                    , fim_tys      = tys
                    , fim_cos      = cos })
708
    = text "match with" <+> parens (ppr inst) <+> ppr tys <+> ppr cos
709

Jan Stolarek's avatar
Jan Stolarek committed
710 711 712 713 714 715 716 717
lookupFamInstEnvByTyCon :: FamInstEnvs -> TyCon -> [FamInst]
lookupFamInstEnvByTyCon (pkg_ie, home_ie) fam_tc
  = get pkg_ie ++ get home_ie
  where
    get ie = case lookupUFM ie fam_tc of
               Nothing          -> []
               Just (FamIE fis) -> fis

718 719
lookupFamInstEnv
    :: FamInstEnvs
720 721
    -> TyCon -> [Type]          -- What we are looking for
    -> [FamInstMatch]           -- Successful matches
722
-- Precondition: the tycon is saturated (or over-saturated)
723 724

lookupFamInstEnv
725 726
   = lookup_fam_inst_env match
   where
727
     match _ _ tpl_tys tys = tcMatchTys tpl_tys tys
728 729 730

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

740 741
lookupFamInstEnvConflicts envs fam_inst@(FamInst { fi_axiom = new_axiom })
  = lookup_fam_inst_env my_unify envs fam tys
742
  where
743
    (fam, tys) = famInstSplitLHS fam_inst
Simon Peyton Jones's avatar
Simon Peyton Jones committed
744
        -- In example above,   fam tys' = F [b]
745 746

    my_unify (FamInst { fi_axiom = old_axiom }) tpl_tvs tpl_tys _
747
       = ASSERT2( tyCoVarsOfTypes tys `disjointVarSet` tpl_tvs,
748 749
                  (ppr fam <+> ppr tys) $$
                  (ppr tpl_tvs <+> ppr tpl_tys) )
750 751
                -- Unification will break badly if the variables overlap
                -- They shouldn't because we allocate separate uniques for them
Simon Peyton Jones's avatar
Simon Peyton Jones committed
752
         if compatibleBranches (coAxiomSingleBranch old_axiom) new_branch
753 754 755
           then Nothing
           else Just noSubst
      -- Note [Family instance overlap conflicts]
756

757 758
    noSubst = panic "lookupFamInstEnvConflicts noSubst"
    new_branch = coAxiomSingleBranch new_axiom
759

Jan Stolarek's avatar
Jan Stolarek committed
760 761 762 763 764 765 766 767 768 769 770 771 772 773 774 775 776 777 778 779 780 781 782 783 784 785 786 787 788 789 790 791 792 793 794 795 796 797 798 799 800 801 802 803 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
--------------------------------------------------------------------------------
--                 Type family injectivity checking bits                      --
--------------------------------------------------------------------------------

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

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

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

   A:  RHSs are different.

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

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

       RHSs of these two equations unify under [ a |-> Int ] substitution.
       Under this substitution LHSs are equal therefore these equations don't
       violate injectivity annotation.

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

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

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

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

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

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

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

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

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

3. If a RHS of a type family equation is a type family application then the type
   family is rejected as not injective.

4. If a LHS type variable that is declared as injective is not mentioned on
   injective position in the RHS then the type family is rejected as not
   injective.  "Injective position" means either an argument to a type
   constructor or argument to a type family on injective position.

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


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

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

      lookup_inj_fam_conflicts ie
          | isOpenFamilyTyCon fam, Just (FamIE insts) <- lookupUFM ie fam
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
878
          = map (coAxiomSingleBranch . fi_axiom) $
Jan Stolarek's avatar
Jan Stolarek committed
879 880 881 882 883 884 885 886
            filter isInjConflict insts
          | otherwise = []


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

887
{-
dreixel's avatar
dreixel committed
888 889 890 891 892 893
Note [Family instance overlap conflicts]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
- In the case of data family instances, any overlap is fundamentally a
  conflict (as these instances imply injective type mappings).

- In the case of type family instances, overlap is admitted as long as
894 895
  the right-hand sides of the overlapping rules coincide under the
  overlap substitution.  eg
dreixel's avatar
dreixel committed
896 897
       type instance F a Int = a
       type instance F Int b = b
Simon Peyton Jones's avatar
Simon Peyton Jones committed
898
  These two overlap on (F Int Int) but then both RHSs are Int,
dreixel's avatar
dreixel committed
899 900
  so all is well. We require that they are syntactically equal;
  anything else would be difficult to test for at this stage.
901
-}
dreixel's avatar
dreixel committed
902

903 904
------------------------------------------------------------
-- Might be a one-way match or a unifier
905 906
type MatchFun =  FamInst                -- The FamInst template
              -> TyVarSet -> [Type]     --   fi_tvs, fi_tys of that FamInst
Simon Peyton Jones's avatar
Simon Peyton Jones committed
907
              -> [Type]                 -- Target to match against
908
              -> Maybe TCvSubst
chak@cse.unsw.edu.au.'s avatar
chak@cse.unsw.edu.au. committed
909

910
lookup_fam_inst_env'          -- The worker, local to this module
911
    :: MatchFun
912
    -> FamInstEnv
913 914
    -> TyCon -> [Type]        -- What we are looking for
    -> [FamInstMatch]
915 916
lookup_fam_inst_env' match_fun ie fam match_tys
  | isOpenFamilyTyCon fam
917
  , Just (FamIE insts) <- lookupUFM ie fam
918
  = find insts    -- The common case
919 920
  | otherwise = []
  where
921 922

    find [] = []
923 924
    find (item@(FamInst { fi_tcs = mb_tcs, fi_tvs = tpl_tvs, fi_cvs = tpl_cvs
                        , fi_tys = tpl_tys }) : rest)
925
        -- Fast check for no match, uses the "rough match" fields
926
      | instanceCantMatch rough_tcs mb_tcs
927 928 929 930 931
      = find rest

        -- Proper check
      | Just subst <- match_fun item (mkVarSet tpl_tvs) tpl_tys match_tys1
      = (FamInstMatch { fim_instance = item
932 933 934 935
                      , fim_tys      = substTyVars subst tpl_tvs `chkAppend` match_tys2
                      , fim_cos      = ASSERT( all (isJust . lookupCoVar subst) tpl_cvs )
                                       substCoVars subst tpl_cvs
                      })
936 937 938
        : find rest

        -- No match => try next
939
      | otherwise
940 941
      = find rest

942
      where
943
        (rough_tcs, match_tys1, match_tys2) = split_tys tpl_tys
Simon Peyton Jones's avatar
Simon Peyton Jones committed
944

945 946 947 948 949
      -- Precondition: the tycon is saturated (or over-saturated)

    -- Deal with over-saturation
    -- See Note [Over-saturated matches]
    split_tys tpl_tys
950
      | isTypeFamilyTyCon fam
951 952 953 954 955 956 957 958 959 960
      = pre_rough_split_tys

      | otherwise
      = let (match_tys1, match_tys2) = splitAtList tpl_tys match_tys
            rough_tcs = roughMatchTcs match_tys1
        in (rough_tcs, match_tys1, match_tys2)

    (pre_match_tys1, pre_match_tys2) = splitAt (tyConArity fam) match_tys
    pre_rough_split_tys
      = (roughMatchTcs pre_match_tys1, pre_match_tys1, pre_match_tys2)
961

962
lookup_fam_inst_env           -- The worker, local to this module
963 964
    :: MatchFun
    -> FamInstEnvs
Jan Stolarek's avatar
Jan Stolarek committed
965 966
    -> TyCon -> [Type]        -- What we are looking for
    -> [FamInstMatch]         -- Successful matches
967 968

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

Simon Peyton Jones's avatar
Simon Peyton Jones committed
970 971 972
lookup_fam_inst_env match_fun (pkg_ie, home_ie) fam tys
  =  lookup_fam_inst_env' match_fun home_ie fam tys
  ++ lookup_fam_inst_env' match_fun pkg_ie  fam tys
973

974
{-
975 976 977