FamInstEnv.hs 40.2 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,
15
        identicalFamInstHead, famInstEnvElts, familyInstances, orphNamesOfFamInst,
16

17 18 19
        -- * CoAxioms
        mkCoAxBranch, mkBranchedCoAxiom, mkUnbranchedCoAxiom, mkSingleCoAxiom,
        computeAxiomIncomps,
20 21

        FamInstMatch(..),
22
        lookupFamInstEnv, lookupFamInstEnvConflicts,
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
23
        isDominatedBy,
Simon Peyton Jones's avatar
Simon Peyton Jones committed
24

25
        -- Normalisation
26
        topNormaliseType, topNormaliseType_maybe,
27
        normaliseType, normaliseTcApp,
28
        reduceTyFamApp_maybe, chooseBranch,
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
29 30

        -- Flattening
31
        flattenTys
32 33 34 35
    ) where

#include "HsVersions.h"

36
import InstEnv
37
import Unify
38
import Type
39
import TcType ( orphNamesOfTypes )
TomSchrijvers's avatar
TomSchrijvers committed
40
import TypeRep
41
import TyCon
42
import Coercion
43
import CoAxiom
44
import VarSet
Simon Peyton Jones's avatar
Simon Peyton Jones committed
45
import VarEnv
46 47
import Name
import UniqFM
48
import Outputable
TomSchrijvers's avatar
TomSchrijvers committed
49
import Maybes
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
50 51
import TrieMap
import Unique
TomSchrijvers's avatar
TomSchrijvers committed
52
import Util
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
53
import Var
54 55 56
import Pair
import SrcLoc
import NameSet
57
import FastString
58

59 60 61
{-
************************************************************************
*                                                                      *
62
          Type checked family instance heads
63 64
*                                                                      *
************************************************************************
65

66 67 68 69 70 71 72 73
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
74
  to a type/data family instance declaration.
75 76 77
    - The FamInst contains a CoAxiom, which is the evidence
      for the instance

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

82 83 84 85 86
data FamInst  -- See Note [FamInsts and CoAxioms]
  = FamInst { fi_axiom  :: CoAxiom Unbranched  -- The new coercion axiom introduced
                                               -- by this family instance
            , fi_flavor :: FamFlavor

Simon Peyton Jones's avatar
Simon Peyton Jones committed
87
            -- Everything below here is a redundant,
88
            -- cached version of the two things above
Simon Peyton Jones's avatar
Simon Peyton Jones committed
89
            -- except that the TyVars are freshened
90 91 92 93 94 95 96 97 98
            , 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

                -- Used for "proper matching"; ditto
            , fi_tvs    :: [TyVar]      -- Template tyvars for full match
99
                                 -- Like ClsInsts, these variables are always
100 101
                                 -- fresh. See Note [Template tyvars are fresh]
                                 -- in InstEnv
102

103 104
            , fi_tys    :: [Type]       --   and its arg types
                -- INVARIANT: fi_tvs = coAxiomTyVars fi_axiom
105

106 107
            , fi_rhs    :: Type         --   the RHS, with its freshened vars
            }
108

Simon Peyton Jones's avatar
Simon Peyton Jones committed
109
data FamFlavor
110 111
  = SynFamilyInst         -- A synonym family
  | DataFamilyInst TyCon  -- A data family, with its representation TyCon
112

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

117 118 119 120
-- Split the left-hand side of the FamInst
famInstSplitLHS :: FamInst -> (TyCon, [Type])
famInstSplitLHS (FamInst { fi_axiom = axiom, fi_tys = lhs })
  = (coAxiomTyCon axiom, lhs)
121

122 123 124
-- Get the RHS of the FamInst
famInstRHS :: FamInst -> Type
famInstRHS = fi_rhs
125

126 127 128
-- Get the family TyCon of the FamInst
famInstTyCon :: FamInst -> TyCon
famInstTyCon = coAxiomTyCon . famInstAxiom
129

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

-- Extracts the TyCon for this *data* (or newtype) instance
135
famInstRepTyCon_maybe :: FamInst -> Maybe TyCon
Simon Peyton Jones's avatar
Simon Peyton Jones committed
136
famInstRepTyCon_maybe fi
137 138 139 140
  = case fi_flavor fi of
       DataFamilyInst tycon -> Just tycon
       SynFamilyInst        -> Nothing

141
dataFamInstRepTyCon :: FamInst -> TyCon
Simon Peyton Jones's avatar
Simon Peyton Jones committed
142
dataFamInstRepTyCon fi
143 144 145
  = case fi_flavor fi of
       DataFamilyInst tycon -> tycon
       SynFamilyInst        -> pprPanic "dataFamInstRepTyCon" (ppr fi)
146

147 148 149
{-
************************************************************************
*                                                                      *
150
        Pretty printing
151 152 153
*                                                                      *
************************************************************************
-}
154

155
instance NamedThing FamInst where
156
   getName = coAxiomName . fi_axiom
157

158
instance Outputable FamInst where
159 160 161
   ppr = pprFamInst

-- Prints the FamInst as a family instance declaration
162 163
-- NB: FamInstEnv.pprFamInst is used only for internal, debug printing
--     See pprTyThing.pprFamInst for printing for the user
164 165 166 167
pprFamInst :: FamInst -> SDoc
pprFamInst famInst
  = hang (pprFamInstHdr famInst)
       2 (vcat [ ifPprDebug (ptext (sLit "Coercion axiom:") <+> ppr ax)
168
               , ifPprDebug (ptext (sLit "RHS:") <+> ppr (famInstRHS famInst)) ])
169
  where
170 171 172 173
    ax = fi_axiom famInst

pprFamInstHdr :: FamInst -> SDoc
pprFamInstHdr fi@(FamInst {fi_flavor = flavor})
174
  = pprTyConSort <+> pp_instance <+> pp_head
175
  where
Simon Peyton Jones's avatar
Simon Peyton Jones committed
176
    -- For *associated* types, say "type T Int = blah"
177
    -- For *top level* type instances, say "type instance T Int = blah"
Simon Peyton Jones's avatar
Simon Peyton Jones committed
178
    pp_instance
179 180 181
      | isTyConAssoc fam_tc = empty
      | otherwise           = ptext (sLit "instance")

182 183 184 185 186 187 188 189 190 191 192 193 194
    (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
195 196 197
                     -- (This is probably over the top now that we use this
                     --  only for internal debug printing; PprTyThing.pprFamInst
                     --  is used for user-level printing.)
198 199 200
            | otherwise
            = vanilla_pp_head

201 202 203 204 205 206 207 208 209
    pprTyConSort = case flavor of
                     SynFamilyInst        -> ptext (sLit "type")
                     DataFamilyInst tycon
                       | isDataTyCon     tycon -> ptext (sLit "data")
                       | isNewTyCon      tycon -> ptext (sLit "newtype")
                       | isAbstractTyCon tycon -> ptext (sLit "data")
                       | otherwise             -> ptext (sLit "WEIRD") <+> ppr tycon

pprFamInsts :: [FamInst] -> SDoc
210
pprFamInsts finsts = vcat (map pprFamInst finsts)
211

212
{-
213 214 215 216 217 218 219 220 221 222 223 224 225 226
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.
227
-}
228

229
-- Make a family instance representation from the information found in an
230
-- interface file.  In particular, we get the rough match info from the iface
231
-- (instead of computing it here).
232
mkImportedFamInst :: Name               -- Name of the family
233 234 235 236
                  -> [Maybe Name]       -- Rough match info
                  -> CoAxiom Unbranched -- Axiom introduced
                  -> FamInst            -- Resulting family instance
mkImportedFamInst fam mb_tcs axiom
237
  = FamInst {
238 239 240 241 242 243 244
      fi_fam    = fam,
      fi_tcs    = mb_tcs,
      fi_tvs    = tvs,
      fi_tys    = tys,
      fi_rhs    = rhs,
      fi_axiom  = axiom,
      fi_flavor = flavor }
Simon Peyton Jones's avatar
Simon Peyton Jones committed
245
  where
246 247 248 249 250
     -- See Note [Lazy axiom match]
     ~(CoAxiom { co_ax_branches =
       ~(FirstBranch ~(CoAxBranch { cab_lhs = tys
                                  , cab_tvs = tvs
                                  , cab_rhs = rhs })) }) = axiom
251 252 253

         -- Derive the flavor for an imported FamInst rather disgustingly
         -- Maybe we should store it in the IfaceFamInst?
254 255 256 257 258 259
     flavor = case splitTyConApp_maybe rhs of
                Just (tc, _)
                  | Just ax' <- tyConFamilyCoercion_maybe tc
                  , ax' == axiom
                  -> DataFamilyInst tc
                _ -> SynFamilyInst
260

261 262 263
{-
************************************************************************
*                                                                      *
264
                FamInstEnv
265 266
*                                                                      *
************************************************************************
267

268
Note [FamInstEnv]
269
~~~~~~~~~~~~~~~~~
270 271 272 273 274 275 276 277 278 279 280 281 282 283
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.

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

 - For finding overlaps and conflicts

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

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

287 288 289 290 291 292 293 294 295 296 297 298 299 300 301 302 303 304
Note [Varying number of patterns for data family axioms]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
For data families, the number of patterns may vary between instances.
For example
   data family T a b
   data instance T Int a = T1 a | T2
   data instance T Bool [a] = T3 a

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

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

These two axioms for T, one with one pattern, one with two.  The reason
for this eta-reduction is decribed in TcInstDcls
   Note [Eta reduction for data family axioms]
305
-}
306

307
type FamInstEnv = UniqFM FamilyInstEnv  -- Maps a family to its instances
308
     -- See Note [FamInstEnv]
309

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

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

316
instance Outputable FamilyInstEnv where
317
  ppr (FamIE fs) = ptext (sLit "FamIE") <+> vcat (map ppr fs)
318

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

323 324 325
emptyFamInstEnvs :: (FamInstEnv, FamInstEnv)
emptyFamInstEnvs = (emptyFamInstEnv, emptyFamInstEnv)

326 327 328
emptyFamInstEnv :: FamInstEnv
emptyFamInstEnv = emptyUFM

329
famInstEnvElts :: FamInstEnv -> [FamInst]
330
famInstEnvElts fi = [elt | FamIE elts <- eltsUFM fi, elt <- elts]
331

332
familyInstances :: (FamInstEnv, FamInstEnv) -> TyCon -> [FamInst]
333 334 335 336
familyInstances (pkg_fie, home_fie) fam
  = get home_fie ++ get pkg_fie
  where
    get env = case lookupUFM env fam of
337
                Just (FamIE insts) -> insts
338
                Nothing                      -> []
339

340
-- | Collects the names of the concrete types and type constructors that
341
-- make up the LHS of a type family instance, including the family
Simon Peyton Jones's avatar
Simon Peyton Jones committed
342
-- name itself.
343
--
344 345
-- For instance, given `type family Foo a b`:
-- `type instance Foo (F (G (H a))) b = ...` would yield [Foo,F,G,H]
346 347
--
-- Used in the implementation of ":info" in GHCi.
348
orphNamesOfFamInst :: FamInst -> NameSet
349 350
orphNamesOfFamInst fam_inst
  = orphNamesOfTypes (concat (brListMap cab_lhs (coAxiomBranches axiom)))
351
    `extendNameSet` getName (coAxiomTyCon axiom)
352 353
  where
    axiom = fi_axiom fam_inst
354

355
extendFamInstEnvList :: FamInstEnv -> [FamInst] -> FamInstEnv
356 357
extendFamInstEnvList inst_env fis = foldl extendFamInstEnv inst_env fis

358
extendFamInstEnv :: FamInstEnv -> FamInst -> FamInstEnv
Simon Peyton Jones's avatar
Simon Peyton Jones committed
359 360
extendFamInstEnv inst_env
                 ins_item@(FamInst {fi_fam = cls_nm})
361
  = addToUFM_C add inst_env cls_nm (FamIE [ins_item])
362
  where
363
    add (FamIE items) _ = FamIE (ins_item:items)
364

365
deleteFromFamInstEnv :: FamInstEnv -> FamInst -> FamInstEnv
366
-- Used only for overriding in GHCi
Simon Peyton Jones's avatar
Simon Peyton Jones committed
367 368 369 370
deleteFromFamInstEnv inst_env fam_inst@(FamInst {fi_fam = fam_nm})
 = adjustUFM adjust inst_env fam_nm
 where
   adjust :: FamilyInstEnv -> FamilyInstEnv
371
   adjust (FamIE items)
372
     = FamIE (filterOut (identicalFamInstHead fam_inst) items)
Simon Peyton Jones's avatar
Simon Peyton Jones committed
373

374 375
identicalFamInstHead :: FamInst -> FamInst -> Bool
-- ^ True when the LHSs are identical
Simon Peyton Jones's avatar
Simon Peyton Jones committed
376
-- Used for overriding in GHCi
377
identicalFamInstHead (FamInst { fi_axiom = ax1 }) (FamInst { fi_axiom = ax2 })
378
  =  coAxiomTyCon ax1 == coAxiomTyCon ax2
379
  && brListLength brs1 == brListLength brs2
380 381 382 383 384 385 386 387 388 389 390 391 392
  && and (brListZipWith identical_branch brs1 brs2)
  where
    brs1 = coAxiomBranches ax1
    brs2 = coAxiomBranches ax2

    identical_branch br1 br2
      =  isJust (tcMatchTys tvs1 lhs1 lhs2)
      && isJust (tcMatchTys tvs2 lhs2 lhs1)
      where
        tvs1 = mkVarSet (coAxBranchTyVars br1)
        tvs2 = mkVarSet (coAxBranchTyVars br2)
        lhs1 = coAxBranchLHS br1
        lhs2 = coAxBranchLHS br2
393

394 395 396
{-
************************************************************************
*                                                                      *
397
                Compatibility
398 399
*                                                                      *
************************************************************************
400

eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
401 402 403 404 405 406 407 408 409 410 411 412
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].)

413 414 415 416 417 418
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.
419

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

423
type family F a where
424 425 426 427 428 429
  F Int = Bool
  F a   = Int

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

430 431 432 433
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.

434 435
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
436
substitution induced by the match, other branches are surely apart. (See
437
Note [Apartness].) This is similar to what happens with class
438 439 440 441 442 443 444 445 446 447 448 449 450 451 452 453 454
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:

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

type family H y
-- no instances

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

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

458 459 460
type family J a where
  J Int = Int
  J a   = a
461

462 463
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.
464

465 466 467
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
468
branches that are compatible with the matching branch, because they are either
469
irrelevant (clause 1 of compatible) or benign (clause 2 of compatible).
470
-}
471

472
-- See Note [Compatibility]
473 474 475
compatibleBranches :: CoAxBranch -> CoAxBranch -> Bool
compatibleBranches (CoAxBranch { cab_lhs = lhs1, cab_rhs = rhs1 })
                   (CoAxBranch { cab_lhs = lhs2, cab_rhs = rhs2 })
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
476
  = case tcUnifyTysFG instanceBindFun lhs1 lhs2 of
477 478 479 480 481 482 483 484
      SurelyApart -> True
      Unifiable subst
        | Type.substTy subst rhs1 `eqType` Type.substTy subst rhs2
        -> True
      _ -> False

-- takes a CoAxiom with unknown branch incompatibilities and computes
-- the compatibilities
485
-- See Note [Storing compatibility] in CoAxiom
486 487 488 489 490 491 492 493 494 495 496 497 498 499
computeAxiomIncomps :: CoAxiom br -> CoAxiom br
computeAxiomIncomps ax@(CoAxiom { co_ax_branches = branches })
  = ax { co_ax_branches = go [] branches }
  where
    go :: [CoAxBranch] -> BranchList CoAxBranch br -> BranchList CoAxBranch br
    go prev_branches (FirstBranch br)
      = FirstBranch (br { cab_incomps = mk_incomps br prev_branches })
    go prev_branches (NextBranch br tail)
      = let br' = br { cab_incomps = mk_incomps br prev_branches } in
        NextBranch br' (go (br' : prev_branches) tail)

    mk_incomps :: CoAxBranch -> [CoAxBranch] -> [CoAxBranch]
    mk_incomps br = filter (not . compatibleBranches br)

500 501 502
{-
************************************************************************
*                                                                      *
503
           Constructing axioms
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
504
    These functions are here because tidyType / tcUnifyTysFG
505
    are not available in CoAxiom
506 507
*                                                                      *
************************************************************************
508 509 510 511 512 513

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

516
-- all axiom roles are Nominal, as this is only used with type families
517 518 519 520 521 522
mkCoAxBranch :: [TyVar] -- original, possibly stale, tyvars
             -> [Type]  -- LHS patterns
             -> Type    -- RHS
             -> SrcSpan
             -> CoAxBranch
mkCoAxBranch tvs lhs rhs loc
523 524 525 526 527
  = CoAxBranch { cab_tvs     = tvs1
               , cab_lhs     = tidyTypes env lhs
               , cab_roles   = map (const Nominal) tvs1
               , cab_rhs     = tidyType  env rhs
               , cab_loc     = loc
528 529 530 531 532 533 534 535 536 537 538 539 540
               , cab_incomps = placeHolderIncomps }
  where
    (env, tvs1) = tidyTyVarBndrs emptyTidyEnv tvs
    -- 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
  = computeAxiomIncomps $
    CoAxiom { co_ax_unique   = nameUnique ax_name
            , co_ax_name     = ax_name
            , co_ax_tc       = fam_tc
541
            , co_ax_role     = Nominal
542 543 544 545 546 547 548 549
            , co_ax_implicit = False
            , co_ax_branches = toBranchList branches }

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
550
            , co_ax_role     = Nominal
551 552 553 554 555 556 557 558
            , co_ax_implicit = False
            , co_ax_branches = FirstBranch (branch { cab_incomps = [] }) }

mkSingleCoAxiom :: Name -> [TyVar] -> TyCon -> [Type] -> Type -> CoAxiom Unbranched
mkSingleCoAxiom ax_name tvs fam_tc lhs_tys rhs_ty
  = CoAxiom { co_ax_unique   = nameUnique ax_name
            , co_ax_name     = ax_name
            , co_ax_tc       = fam_tc
559
            , co_ax_role     = Nominal
560 561 562 563 564
            , co_ax_implicit = False
            , co_ax_branches = FirstBranch (branch { cab_incomps = [] }) }
  where
    branch = mkCoAxBranch tvs lhs_tys rhs_ty (getSrcSpan ax_name)

565 566 567
{-
************************************************************************
*                                                                      *
568
                Looking up a family instance
569 570
*                                                                      *
************************************************************************
571 572 573 574 575 576 577 578 579 580 581 582 583 584 585 586 587

@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)'.
588
-}
589

590
-- when matching a type family application, we get a FamInst,
591 592
-- and the list of types the axiom should be applied to
data FamInstMatch = FamInstMatch { fim_instance :: FamInst
593 594
                                 , fim_tys      :: [Type]
                                 }
595
  -- See Note [Over-saturated matches]
596 597 598 599

instance Outputable FamInstMatch where
  ppr (FamInstMatch { fim_instance = inst
                    , fim_tys      = tys })
600
    = ptext (sLit "match with") <+> parens (ppr inst) <+> ppr tys
601

602 603
lookupFamInstEnv
    :: FamInstEnvs
604 605
    -> TyCon -> [Type]          -- What we are looking for
    -> [FamInstMatch]           -- Successful matches
606
-- Precondition: the tycon is saturated (or over-saturated)
607 608

lookupFamInstEnv
609 610 611
   = lookup_fam_inst_env match
   where
     match _ tpl_tvs tpl_tys tys = tcMatchTys tpl_tvs tpl_tys tys
612 613 614

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

624 625
lookupFamInstEnvConflicts envs fam_inst@(FamInst { fi_axiom = new_axiom })
  = lookup_fam_inst_env my_unify envs fam tys
626
  where
627
    (fam, tys) = famInstSplitLHS fam_inst
Simon Peyton Jones's avatar
Simon Peyton Jones committed
628
        -- In example above,   fam tys' = F [b]
629 630 631 632 633

    my_unify (FamInst { fi_axiom = old_axiom }) tpl_tvs tpl_tys _
       = ASSERT2( tyVarsOfTypes tys `disjointVarSet` tpl_tvs,
                  (ppr fam <+> ppr tys) $$
                  (ppr tpl_tvs <+> ppr tpl_tys) )
634 635
                -- 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
636
         if compatibleBranches (coAxiomSingleBranch old_axiom) new_branch
637 638 639
           then Nothing
           else Just noSubst
      -- Note [Family instance overlap conflicts]
640

641 642
    noSubst = panic "lookupFamInstEnvConflicts noSubst"
    new_branch = coAxiomSingleBranch new_axiom
643

644
{-
dreixel's avatar
dreixel committed
645 646 647 648 649 650
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
651 652
  the right-hand sides of the overlapping rules coincide under the
  overlap substitution.  eg
dreixel's avatar
dreixel committed
653 654
       type instance F a Int = a
       type instance F Int b = b
Simon Peyton Jones's avatar
Simon Peyton Jones committed
655
  These two overlap on (F Int Int) but then both RHSs are Int,
dreixel's avatar
dreixel committed
656 657
  so all is well. We require that they are syntactically equal;
  anything else would be difficult to test for at this stage.
658
-}
dreixel's avatar
dreixel committed
659

660 661
------------------------------------------------------------
-- Might be a one-way match or a unifier
662 663
type MatchFun =  FamInst                -- The FamInst template
              -> TyVarSet -> [Type]     --   fi_tvs, fi_tys of that FamInst
Simon Peyton Jones's avatar
Simon Peyton Jones committed
664
              -> [Type]                 -- Target to match against
665
              -> Maybe TvSubst
chak@cse.unsw.edu.au.'s avatar
chak@cse.unsw.edu.au. committed
666

667
lookup_fam_inst_env'          -- The worker, local to this module
668
    :: MatchFun
669
    -> FamInstEnv
670 671
    -> TyCon -> [Type]        -- What we are looking for
    -> [FamInstMatch]
672 673
lookup_fam_inst_env' match_fun ie fam match_tys
  | isOpenFamilyTyCon fam
674
  , Just (FamIE insts) <- lookupUFM ie fam
675
  = find insts    -- The common case
676 677
  | otherwise = []
  where
678 679

    find [] = []
Simon Peyton Jones's avatar
Simon Peyton Jones committed
680
    find (item@(FamInst { fi_tcs = mb_tcs, fi_tvs = tpl_tvs,
681 682
                          fi_tys = tpl_tys }) : rest)
        -- Fast check for no match, uses the "rough match" fields
683
      | instanceCantMatch rough_tcs mb_tcs
684 685 686 687 688 689 690 691 692
      = find rest

        -- Proper check
      | Just subst <- match_fun item (mkVarSet tpl_tvs) tpl_tys match_tys1
      = (FamInstMatch { fim_instance = item
                      , fim_tys      = substTyVars subst tpl_tvs `chkAppend` match_tys2 })
        : find rest

        -- No match => try next
693
      | otherwise
694 695
      = find rest

696
      where
697
        (rough_tcs, match_tys1, match_tys2) = split_tys tpl_tys
Simon Peyton Jones's avatar
Simon Peyton Jones committed
698

699 700 701 702 703
      -- Precondition: the tycon is saturated (or over-saturated)

    -- Deal with over-saturation
    -- See Note [Over-saturated matches]
    split_tys tpl_tys
704
      | isTypeFamilyTyCon fam
705 706 707 708 709 710 711 712 713 714
      = 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)
715

716
lookup_fam_inst_env           -- The worker, local to this module
717 718
    :: MatchFun
    -> FamInstEnvs
719
    -> TyCon -> [Type]          -- What we are looking for
720
    -> [FamInstMatch]           -- Successful matches
721 722

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

Simon Peyton Jones's avatar
Simon Peyton Jones committed
724 725 726
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
727

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

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

Simon Peyton Jones's avatar
Simon Peyton Jones committed
739
Then looking up (F (Int,Bool) Char) will return a FamInstMatch
740 741
     (FPair, [Int,Bool,Char])
The "extra" type argument [Char] just stays on the end.
742

Simon Peyton Jones's avatar
Simon Peyton Jones committed
743 744
We handle data families and type families separately here:

Gabor Greif's avatar
Gabor Greif committed
745
 * For type families, all instances of a type family must have the
Simon Peyton Jones's avatar
Simon Peyton Jones committed
746 747 748
   same arity, so we can precompute the split between the match_tys
   and the overflow tys. This is done in pre_rough_split_tys.

Gabor Greif's avatar
Gabor Greif committed
749
 * For data family instances, though, we need to re-split for each
Simon Peyton Jones's avatar
Simon Peyton Jones committed
750 751
   instance, because the breakdown might be different for each
   instance.  Why?  Because of eta reduction; see Note [Eta reduction
752
   for data family axioms] in TcInstDcls.
753
-}
754 755 756 757 758 759 760 761 762

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

772 773 774
{-
************************************************************************
*                                                                      *
775
                Choosing an axiom application
776 777
*                                                                      *
************************************************************************
778 779 780

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

Simon Peyton Jones's avatar
Simon Peyton Jones committed
783 784 785 786
reduceTyFamApp_maybe :: FamInstEnvs
                     -> Role              -- Desired role of result coercion
                     -> TyCon -> [Type]
                     -> Maybe (Coercion, Type)
787
-- Attempt to do a *one-step* reduction of a type-family application
Simon Peyton Jones's avatar
Simon Peyton Jones committed
788 789 790
--    but *not* newtypes
-- Works on type-synonym families always; data-families only if
--     the role we seek is representational
791 792 793
-- It does *not* normlise the type arguments first, so this may not
--     go as far as you want. If you want normalised type arguments,
--     use normaliseTcArgs first.
794 795 796
--
-- The TyCon can be oversaturated.
-- Works on both open and closed families
797

798
reduceTyFamApp_maybe envs role tc tys
Simon Peyton Jones's avatar
Simon Peyton Jones committed
799 800 801 802 803
  | Phantom <- role
  = Nothing

  | case role of
       Representational -> isOpenFamilyTyCon    tc
804
       _                -> isOpenTypeFamilyTyCon tc
Simon Peyton Jones's avatar
Simon Peyton Jones committed
805 806 807 808
       -- If we seek a representational coercion
       -- (e.g. the call in topNormaliseType_maybe) then we can
       -- unwrap data families as well as type-synonym families;
       -- otherwise only type-synonym families
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
809
  , FamInstMatch { fim_instance = fam_inst
810
                 , fim_tys =      inst_tys } : _ <- lookupFamInstEnv envs tc tys
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
811 812
      -- NB: Allow multiple matches because of compatible overlap
                                                    
813 814 815
  = let ax     = famInstAxiom fam_inst
        co     = mkUnbranchedAxInstCo role ax inst_tys
        ty     = pSnd (coercionKind co)
816
    in Just (co, ty)
817 818

  | Just ax <- isClosedSynFamilyTyCon_maybe tc
819
  , Just (ind, inst_tys) <- chooseBranch ax tys
820 821
  = let co     = mkAxInstCo role ax ind inst_tys
        ty     = pSnd (coercionKind co)
822
    in Just (co, ty)
823

824
  | Just ax           <- isBuiltInSynFamTyCon_maybe tc
825
  , Just (coax,ts,ty) <- sfMatchFam ax tys
826
  = let co = mkAxiomRuleCo coax ts []
827
    in Just (co, ty)
828

829 830 831 832 833 834 835 836 837 838 839 840 841 842 843 844 845 846 847 848 849 850
  | otherwise
  = Nothing

-- The axiom can be oversaturated. (Closed families only.)
chooseBranch :: CoAxiom Branched -> [Type] -> Maybe (BranchIndex, [Type])
chooseBranch axiom tys
  = do { let num_pats = coAxiomNumPats axiom
             (target_tys, extra_tys) = splitAt num_pats tys
             branches = coAxiomBranches axiom
       ; (ind, inst_tys) <- findBranch (fromBranchList branches) 0 target_tys
       ; return (ind, inst_tys ++ extra_tys) }

-- The axiom must *not* be oversaturated
findBranch :: [CoAxBranch]             -- branches to check
           -> BranchIndex              -- index of current branch
           -> [Type]                   -- target types
           -> Maybe (BranchIndex, [Type])
findBranch (CoAxBranch { cab_tvs = tpl_tvs, cab_lhs = tpl_lhs, cab_incomps = incomps }
              : rest) ind target_tys
  = case tcMatchTys (mkVarSet tpl_tvs) tpl_lhs target_tys of
      Just subst -- matching worked. now, check for apartness.
        |  all (isSurelyApart
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
851
                . tcUnifyTysFG instanceBindFun flattened_target
852
                . coAxBranchLHS) incomps
853 854 855 856 857 858 859 860 861
        -> -- matching worked & we're apart from all incompatible branches. success
           Just (ind, substTyVars subst tpl_tvs)

      -- failure. keep looking
      _ -> findBranch rest (ind+1) target_tys

  where isSurelyApart SurelyApart = True
        isSurelyApart _           = False

eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
862 863 864 865
        flattened_target = flattenTys in_scope target_tys
        in_scope = mkInScopeSet (unionVarSets $
                                 map (tyVarsOfTypes . coAxBranchLHS) incomps)

866 867
-- fail if no branches left
findBranch [] _ _ = Nothing
TomSchrijvers's avatar
TomSchrijvers committed
868

869 870 871
{-
************************************************************************
*                                                                      *
872
                Looking up a family instance
873 874 875
*                                                                      *
************************************************************************
-}
TomSchrijvers's avatar
TomSchrijvers committed
876

877 878 879 880 881
topNormaliseType :: FamInstEnvs -> Type -> Type
topNormaliseType env ty = case topNormaliseType_maybe env ty of
                            Just (_co, ty') -> ty'
                            Nothing         -> ty

eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
882
topNormaliseType_maybe :: FamInstEnvs -> Type -> Maybe (Coercion, Type)
883

eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
884
-- ^ Get rid of *outermost* (or toplevel)
885
--      * type function redex
886
--      * newtypes
887 888 889 890 891 892 893
-- using appropriate coercions.  Specifically, if
--   topNormaliseType_maybe env ty = Maybe (co, ty')
-- then
--   (a) co :: ty ~ ty'
--   (b) ty' is not a newtype, and is not a type-family redex
--
-- However, ty' can be something like (Maybe (F ty)), where
894
-- (F ty) is a redex.
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
895
--
896
-- Its a bit like Type.repType, but handles type families too
897
-- The coercion returned is always an R coercion
898

899
topNormaliseType_maybe env ty
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
900
  = topNormaliseTypeX_maybe stepper ty
901
  where
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
902 903 904 905
    stepper
      = unwrapNewTypeStepper
        `composeSteppers`
        \ rec_nts tc tys ->
906 907 908
        let (args_co, ntys) = normaliseTcArgs env Representational tc tys in
        case reduceTyFamApp_maybe env Representational tc ntys of
          Just (co, rhs) -> NS_Step rec_nts rhs (args_co `mkTransCo` co)
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
909
          Nothing        -> NS_Done
TomSchrijvers's avatar
TomSchrijvers committed