1 -- (c) The University of Glasgow 2012

3 {-# LANGUAGE CPP, DataKinds, DeriveDataTypeable, GADTs, KindSignatures,

4 ScopedTypeVariables, StandaloneDeriving, RoleAnnotations #-}

6 -- | Module for coercion axioms, used to represent type family instances

7 -- and newtypes

13 mapAccumBranches,

22 coAxBranchRoles,

24 placeHolderIncomps,

29 BuiltInSynFamily(..), trivialBuiltInFamily

34 import Outputable

35 import FastString

36 import Name

37 import Unique

38 import Var

39 import Util

40 import Binary

41 import Pair

42 import BasicTypes

44 import SrcLoc

51 {-

52 Note [Coercion axiom branches]

53 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

54 In order to allow closed type families, an axiom needs to contain an

55 ordered list of alternatives, called branches. The kind of the coercion built

56 from an axiom is determined by which index is used when building the coercion

57 from the axiom.

59 For example, consider the axiom derived from the following declaration:

61 type family F a where

62 F [Int] = Bool

63 F [a] = Double

64 F (a b) = Char

66 This will give rise to this axiom:

68 axF :: { F [Int] ~ Bool

69 ; forall (a :: *). F [a] ~ Double

70 ; forall (k :: *) (a :: k -> *) (b :: k). F (a b) ~ Char

71 }

73 The axiom is used with the AxiomInstCo constructor of Coercion. If we wish

74 to have a coercion showing that F (Maybe Int) ~ Char, it will look like

76 axF[2] <*> <Maybe> <Int> :: F (Maybe Int) ~ Char

77 -- or, written using concrete-ish syntax --

78 AxiomInstCo axF 2 [Refl *, Refl Maybe, Refl Int]

80 Note that the index is 0-based.

82 For type-checking, it is also necessary to check that no previous pattern

83 can unify with the supplied arguments. After all, it is possible that some

84 of the type arguments are lambda-bound type variables whose instantiation may

85 cause an earlier match among the branches. We wish to prohibit this behavior,

86 so the type checker rules out the choice of a branch where a previous branch

87 can unify. See also [Apartness] in FamInstEnv.hs.

89 For example, the following is malformed, where 'a' is a lambda-bound type

90 variable:

92 axF[2] <*> <a> <Bool> :: F (a Bool) ~ Char

94 Why? Because a might be instantiated with [], meaning that branch 1 should

95 apply, not branch 2. This is a vital consistency check; without it, we could

96 derive Int ~ Bool, and that is a Bad Thing.

98 Note [Branched axioms]

99 ~~~~~~~~~~~~~~~~~~~~~~

100 Although a CoAxiom has the capacity to store many branches, in certain cases,

101 we want only one. These cases are in data/newtype family instances, newtype

102 coercions, and type family instances.

103 Furthermore, these unbranched axioms are used in a

104 variety of places throughout GHC, and it would difficult to generalize all of

105 that code to deal with branched axioms, especially when the code can be sure

106 of the fact that an axiom is indeed a singleton. At the same time, it seems

107 dangerous to assume singlehood in various places through GHC.

109 The solution to this is to label a CoAxiom with a phantom type variable

110 declaring whether it is known to be a singleton or not. The branches

111 are stored using a special datatype, declared below, that ensures that the

112 type variable is accurate.

114 ************************************************************************

115 * *

116 Branches

117 * *

118 ************************************************************************

119 -}

122 -- Counting from zero

124 -- promoted data type

128 -- By using type synonyms for the promoted constructors, we avoid needing

129 -- DataKinds and the promotion quote in client modules. This also means that

130 -- we don't need to export the term-level constructors, which should never be used.

134 type role Branches nominal

139 where

150 MkBranches arr

161 -- | The @[CoAxBranch]@ passed into the mapping function is a list of

162 -- all previous branches, reversed

167 where

173 {-

174 ************************************************************************

175 * *

176 Coercion axioms

177 * *

178 ************************************************************************

180 Note [Storing compatibility]

181 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~

182 During axiom application, we need to be aware of which branches are compatible

183 with which others. The full explanation is in Note [Compatibility] in

184 FamInstEnv. (The code is placed there to avoid a dependency from CoAxiom on

185 the unification algorithm.) Although we could theoretically compute

186 compatibility on the fly, this is silly, so we store it in a CoAxiom.

188 Specifically, each branch refers to all other branches with which it is

189 incompatible. This list might well be empty, and it will always be for the

190 first branch of any axiom.

192 CoAxBranches that do not (yet) belong to a CoAxiom should have a panic thunk

193 stored in cab_incomps. The incompatibilities are properly a property of the

194 axiom as a whole, and they are computed only when the final axiom is built.

196 During serialization, the list is converted into a list of the indices

197 of the branches.

198 -}

200 -- | A 'CoAxiom' is a \"coercion constructor\", i.e. a named equality axiom.

202 -- If you edit this type, you may need to update the GHC formalism

203 -- See Note [GHC Formalism] in coreSyn/CoreLint.hs

204 data CoAxiom br

210 -- e.g. the newtype or family tycon

213 -- See Note [Implicit axioms]

214 -- INVARIANT: co_ax_implicit == True implies length co_ax_branches == 1.

215 }

217 data CoAxBranch

218 = CoAxBranch

220 -- See Note [CoAxiom locations]

222 -- See Note [CoAxBranch type variables]

224 -- Always empty, for now.

225 -- See Note [Constraints in patterns]

226 -- in TcTyClsDecls

229 -- See Note [CoAxiom saturation]

232 -- See Note [Storing compatibility]

233 }

252 coAxiomArity ax index

254 where

258 coAxiomName = co_ax_name

261 coAxiomRole = co_ax_role

264 coAxiomBranches = co_ax_branches

270 | otherwise

271 = Nothing

278 coAxiomTyCon = co_ax_tc

281 coAxBranchTyVars = cab_tvs

284 coAxBranchCoVars = cab_cvs

287 coAxBranchLHS = cab_lhs

290 coAxBranchRHS = cab_rhs

293 coAxBranchRoles = cab_roles

296 coAxBranchSpan = cab_loc

299 isImplicitCoAxiom = co_ax_implicit

302 coAxBranchIncomps = cab_incomps

304 -- See Note [Compatibility checking] in FamInstEnv

308 {- Note [CoAxiom saturation]

309 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~

310 * When co

312 Note [CoAxBranch type variables]

313 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

314 In the case of a CoAxBranch of an associated type-family instance,

315 we use the *same* type variables (where possible) as the

316 enclosing class or instance. Consider

317 class C a b where

318 type F x b

319 type F [y] b = ... -- Second param must be b

321 instance C Int [z] where

322 type F Int [z] = ... -- Second param must be [z]

324 In the CoAxBranch in the instance decl (F Int [z]) we use the

325 same 'z', so that it's easy to check that that type is the same

326 as that in the instance header.

328 Similarly in the CoAxBranch for the default decl for F in the

329 class decl, we use the same 'b' to make the same check easy.

331 So, unlike FamInsts, there is no expectation that the cab_tvs

332 are fresh wrt each other, or any other CoAxBranch.

334 Note [CoAxBranch roles]

335 ~~~~~~~~~~~~~~~~~~~~~~~

336 Consider this code:

338 newtype Age = MkAge Int

339 newtype Wrap a = MkWrap a

341 convert :: Wrap Age -> Int

342 convert (MkWrap (MkAge i)) = i

344 We want this to compile to:

346 NTCo:Wrap :: forall a. Wrap a ~R a

347 NTCo:Age :: Age ~R Int

348 convert = \x -> x |> (NTCo:Wrap[0] NTCo:Age[0])

350 But, note that NTCo:Age is at role R. Thus, we need to be able to pass

351 coercions at role R into axioms. However, we don't *always* want to be able to

352 do this, as it would be disastrous with type families. The solution is to

353 annotate the arguments to the axiom with roles, much like we annotate tycon

354 tyvars. Where do these roles get set? Newtype axioms inherit their roles from

355 the newtype tycon; family axioms are all at role N.

357 Note [CoAxiom locations]

358 ~~~~~~~~~~~~~~~~~~~~~~~~

359 The source location of a CoAxiom is stored in two places in the

360 datatype tree.

361 * The first is in the location info buried in the Name of the

362 CoAxiom. This span includes all of the branches of a branched

363 CoAxiom.

364 * The second is in the cab_loc fields of the CoAxBranches.

366 In the case of a single branch, we can extract the source location of

367 the branch from the name of the CoAxiom. In other cases, we need an

368 explicit SrcSpan to correctly store the location of the equation

369 giving rise to the FamInstBranch.

371 Note [Implicit axioms]

372 ~~~~~~~~~~~~~~~~~~~~~~

373 See also Note [Implicit TyThings] in HscTypes

374 * A CoAxiom arising from data/type family instances is not "implicit".

375 That is, it has its own IfaceAxiom declaration in an interface file

377 * The CoAxiom arising from a newtype declaration *is* "implicit".

378 That is, it does not have its own IfaceAxiom declaration in an

379 interface file; instead the CoAxiom is generated by type-checking

380 the newtype declaration

381 -}

395 getUnique = co_ax_unique

401 getName = co_ax_name

404 -- don't traverse?

417 {-

418 ************************************************************************

419 * *

420 Roles

421 * *

422 ************************************************************************

424 Roles are defined here to avoid circular dependencies.

425 -}

427 -- See Note [Roles] in Coercion

428 -- defined here to avoid cyclic dependency with Coercion

432 -- These names are slurped into the parser code. Changing these strings

433 -- will change the **surface syntax** that GHC accepts! If you want to

434 -- change only the pretty-printing, do some replumbing. See

435 -- mkRoleAnnotDecl in RdrHsSyn

455 {-

456 ************************************************************************

457 * *

458 CoAxiomRule

459 Rules for building Evidence

460 * *

461 ************************************************************************

463 Conditional axioms. The general idea is that a `CoAxiomRule` looks like this:

465 forall as. (r1 ~ r2, s1 ~ s2) => t1 ~ t2

467 My intention is to reuse these for both (~) and (~#).

468 The short-term plan is to use this datatype to represent the type-nat axioms.

469 In the longer run, it may be good to unify this and `CoAxiom`,

470 as `CoAxiom` is the special case when there are no assumptions.

471 -}

473 -- | A more explicit representation for `t1 ~ t2`.

476 -- | For now, we work only with nominal equality.

482 -- ^ coaxrProves returns @Nothing@ when it doesn't like

483 -- the supplied arguments. When this happens in a coercion

484 -- that means that the coercion is ill-formed, and Core Lint

485 -- checks for that.

486 }

489 -- don't traverse?

507 -- Type checking of built-in families

513 }

515 -- Provides default implementations that do nothing.

516 trivialBuiltInFamily :: BuiltInSynFamily

517 trivialBuiltInFamily = BuiltInSynFamily

521 }