More fixes for unboxed tuples
[ghc.git] / compiler / types / CoAxiom.hs
1 -- (c) The University of Glasgow 2012
2
3 {-# LANGUAGE CPP, DataKinds, DeriveDataTypeable, GADTs, KindSignatures,
4 ScopedTypeVariables, StandaloneDeriving, RoleAnnotations #-}
5
6 -- | Module for coercion axioms, used to represent type family instances
7 -- and newtypes
8
9 module CoAxiom (
10 BranchFlag, Branched, Unbranched, BranchIndex, Branches,
11 manyBranches, unbranched,
12 fromBranches, numBranches,
13 mapAccumBranches,
14
15 CoAxiom(..), CoAxBranch(..),
16
17 toBranchedAxiom, toUnbranchedAxiom,
18 coAxiomName, coAxiomArity, coAxiomBranches,
19 coAxiomTyCon, isImplicitCoAxiom, coAxiomNumPats,
20 coAxiomNthBranch, coAxiomSingleBranch_maybe, coAxiomRole,
21 coAxiomSingleBranch, coAxBranchTyVars, coAxBranchCoVars,
22 coAxBranchRoles,
23 coAxBranchLHS, coAxBranchRHS, coAxBranchSpan, coAxBranchIncomps,
24 placeHolderIncomps,
25
26 Role(..), fsFromRole,
27
28 CoAxiomRule(..), Eqn,
29 BuiltInSynFamily(..), trivialBuiltInFamily
30 ) where
31
32 import {-# SOURCE #-} TyCoRep ( Type, pprType )
33 import {-# SOURCE #-} TyCon ( TyCon )
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
43 import Data.Typeable ( Typeable )
44 import SrcLoc
45 import qualified Data.Data as Data
46 import Data.Array
47 import Data.List ( mapAccumL )
48
49 #include "HsVersions.h"
50
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.
58
59 For example, consider the axiom derived from the following declaration:
60
61 type family F a where
62 F [Int] = Bool
63 F [a] = Double
64 F (a b) = Char
65
66 This will give rise to this axiom:
67
68 axF :: { F [Int] ~ Bool
69 ; forall (a :: *). F [a] ~ Double
70 ; forall (k :: *) (a :: k -> *) (b :: k). F (a b) ~ Char
71 }
72
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
75
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]
79
80 Note that the index is 0-based.
81
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.
88
89 For example, the following is malformed, where 'a' is a lambda-bound type
90 variable:
91
92 axF[2] <*> <a> <Bool> :: F (a Bool) ~ Char
93
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.
97
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.
108
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.
113
114 ************************************************************************
115 * *
116 Branches
117 * *
118 ************************************************************************
119 -}
120
121 type BranchIndex = Int -- The index of the branch in the list of branches
122 -- Counting from zero
123
124 -- promoted data type
125 data BranchFlag = Branched | Unbranched
126 type Branched = 'Branched
127 type Unbranched = 'Unbranched
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.
131
132 newtype Branches (br :: BranchFlag)
133 = MkBranches { unMkBranches :: Array BranchIndex CoAxBranch }
134 type role Branches nominal
135
136 manyBranches :: [CoAxBranch] -> Branches Branched
137 manyBranches brs = ASSERT( snd bnds >= fst bnds )
138 MkBranches (listArray bnds brs)
139 where
140 bnds = (0, length brs - 1)
141
142 unbranched :: CoAxBranch -> Branches Unbranched
143 unbranched br = MkBranches (listArray (0, 0) [br])
144
145 toBranched :: Branches br -> Branches Branched
146 toBranched = MkBranches . unMkBranches
147
148 toUnbranched :: Branches br -> Branches Unbranched
149 toUnbranched (MkBranches arr) = ASSERT( bounds arr == (0,0) )
150 MkBranches arr
151
152 fromBranches :: Branches br -> [CoAxBranch]
153 fromBranches = elems . unMkBranches
154
155 branchesNth :: Branches br -> BranchIndex -> CoAxBranch
156 branchesNth (MkBranches arr) n = arr ! n
157
158 numBranches :: Branches br -> Int
159 numBranches (MkBranches arr) = snd (bounds arr) + 1
160
161 -- | The @[CoAxBranch]@ passed into the mapping function is a list of
162 -- all previous branches, reversed
163 mapAccumBranches :: ([CoAxBranch] -> CoAxBranch -> CoAxBranch)
164 -> Branches br -> Branches br
165 mapAccumBranches f (MkBranches arr)
166 = MkBranches (listArray (bounds arr) (snd $ mapAccumL go [] (elems arr)))
167 where
168 go :: [CoAxBranch] -> CoAxBranch -> ([CoAxBranch], CoAxBranch)
169 go prev_branches cur_branch = ( cur_branch : prev_branches
170 , f prev_branches cur_branch )
171
172
173 {-
174 ************************************************************************
175 * *
176 Coercion axioms
177 * *
178 ************************************************************************
179
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.
187
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.
191
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.
195
196 During serialization, the list is converted into a list of the indices
197 of the branches.
198 -}
199
200 -- | A 'CoAxiom' is a \"coercion constructor\", i.e. a named equality axiom.
201
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
205 = CoAxiom -- Type equality axiom.
206 { co_ax_unique :: Unique -- Unique identifier
207 , co_ax_name :: Name -- Name for pretty-printing
208 , co_ax_role :: Role -- Role of the axiom's equality
209 , co_ax_tc :: TyCon -- The head of the LHS patterns
210 -- e.g. the newtype or family tycon
211 , co_ax_branches :: Branches br -- The branches that form this axiom
212 , co_ax_implicit :: Bool -- True <=> the axiom is "implicit"
213 -- See Note [Implicit axioms]
214 -- INVARIANT: co_ax_implicit == True implies length co_ax_branches == 1.
215 }
216
217 data CoAxBranch
218 = CoAxBranch
219 { cab_loc :: SrcSpan -- Location of the defining equation
220 -- See Note [CoAxiom locations]
221 , cab_tvs :: [TyVar] -- Bound type variables; not necessarily fresh
222 -- See Note [CoAxBranch type variables]
223 , cab_cvs :: [CoVar] -- Bound coercion variables
224 -- Always empty, for now.
225 -- See Note [Constraints in patterns]
226 -- in TcTyClsDecls
227 , cab_roles :: [Role] -- See Note [CoAxBranch roles]
228 , cab_lhs :: [Type] -- Type patterns to match against
229 -- See Note [CoAxiom saturation]
230 , cab_rhs :: Type -- Right-hand side of the equality
231 , cab_incomps :: [CoAxBranch] -- The previous incompatible branches
232 -- See Note [Storing compatibility]
233 }
234 deriving Data.Data
235
236 toBranchedAxiom :: CoAxiom br -> CoAxiom Branched
237 toBranchedAxiom (CoAxiom unique name role tc branches implicit)
238 = CoAxiom unique name role tc (toBranched branches) implicit
239
240 toUnbranchedAxiom :: CoAxiom br -> CoAxiom Unbranched
241 toUnbranchedAxiom (CoAxiom unique name role tc branches implicit)
242 = CoAxiom unique name role tc (toUnbranched branches) implicit
243
244 coAxiomNumPats :: CoAxiom br -> Int
245 coAxiomNumPats = length . coAxBranchLHS . (flip coAxiomNthBranch 0)
246
247 coAxiomNthBranch :: CoAxiom br -> BranchIndex -> CoAxBranch
248 coAxiomNthBranch (CoAxiom { co_ax_branches = bs }) index
249 = branchesNth bs index
250
251 coAxiomArity :: CoAxiom br -> BranchIndex -> Arity
252 coAxiomArity ax index
253 = length tvs + length cvs
254 where
255 CoAxBranch { cab_tvs = tvs, cab_cvs = cvs } = coAxiomNthBranch ax index
256
257 coAxiomName :: CoAxiom br -> Name
258 coAxiomName = co_ax_name
259
260 coAxiomRole :: CoAxiom br -> Role
261 coAxiomRole = co_ax_role
262
263 coAxiomBranches :: CoAxiom br -> Branches br
264 coAxiomBranches = co_ax_branches
265
266 coAxiomSingleBranch_maybe :: CoAxiom br -> Maybe CoAxBranch
267 coAxiomSingleBranch_maybe (CoAxiom { co_ax_branches = MkBranches arr })
268 | snd (bounds arr) == 0
269 = Just $ arr ! 0
270 | otherwise
271 = Nothing
272
273 coAxiomSingleBranch :: CoAxiom Unbranched -> CoAxBranch
274 coAxiomSingleBranch (CoAxiom { co_ax_branches = MkBranches arr })
275 = arr ! 0
276
277 coAxiomTyCon :: CoAxiom br -> TyCon
278 coAxiomTyCon = co_ax_tc
279
280 coAxBranchTyVars :: CoAxBranch -> [TyVar]
281 coAxBranchTyVars = cab_tvs
282
283 coAxBranchCoVars :: CoAxBranch -> [CoVar]
284 coAxBranchCoVars = cab_cvs
285
286 coAxBranchLHS :: CoAxBranch -> [Type]
287 coAxBranchLHS = cab_lhs
288
289 coAxBranchRHS :: CoAxBranch -> Type
290 coAxBranchRHS = cab_rhs
291
292 coAxBranchRoles :: CoAxBranch -> [Role]
293 coAxBranchRoles = cab_roles
294
295 coAxBranchSpan :: CoAxBranch -> SrcSpan
296 coAxBranchSpan = cab_loc
297
298 isImplicitCoAxiom :: CoAxiom br -> Bool
299 isImplicitCoAxiom = co_ax_implicit
300
301 coAxBranchIncomps :: CoAxBranch -> [CoAxBranch]
302 coAxBranchIncomps = cab_incomps
303
304 -- See Note [Compatibility checking] in FamInstEnv
305 placeHolderIncomps :: [CoAxBranch]
306 placeHolderIncomps = panic "placeHolderIncomps"
307
308 {- Note [CoAxiom saturation]
309 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~
310 * When co
311
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
320
321 instance C Int [z] where
322 type F Int [z] = ... -- Second param must be [z]
323
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.
327
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.
330
331 So, unlike FamInsts, there is no expectation that the cab_tvs
332 are fresh wrt each other, or any other CoAxBranch.
333
334 Note [CoAxBranch roles]
335 ~~~~~~~~~~~~~~~~~~~~~~~
336 Consider this code:
337
338 newtype Age = MkAge Int
339 newtype Wrap a = MkWrap a
340
341 convert :: Wrap Age -> Int
342 convert (MkWrap (MkAge i)) = i
343
344 We want this to compile to:
345
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])
349
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.
356
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.
365
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.
370
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
376
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 -}
382
383 instance Eq (CoAxiom br) where
384 a == b = case (a `compare` b) of { EQ -> True; _ -> False }
385 a /= b = case (a `compare` b) of { EQ -> False; _ -> True }
386
387 instance Ord (CoAxiom br) where
388 a <= b = case (a `compare` b) of { LT -> True; EQ -> True; GT -> False }
389 a < b = case (a `compare` b) of { LT -> True; EQ -> False; GT -> False }
390 a >= b = case (a `compare` b) of { LT -> False; EQ -> True; GT -> True }
391 a > b = case (a `compare` b) of { LT -> False; EQ -> False; GT -> True }
392 compare a b = getUnique a `compare` getUnique b
393
394 instance Uniquable (CoAxiom br) where
395 getUnique = co_ax_unique
396
397 instance Outputable (CoAxiom br) where
398 ppr = ppr . getName
399
400 instance NamedThing (CoAxiom br) where
401 getName = co_ax_name
402
403 instance Typeable br => Data.Data (CoAxiom br) where
404 -- don't traverse?
405 toConstr _ = abstractConstr "CoAxiom"
406 gunfold _ _ = error "gunfold"
407 dataTypeOf _ = mkNoRepType "CoAxiom"
408
409 instance Outputable CoAxBranch where
410 ppr (CoAxBranch { cab_loc = loc
411 , cab_lhs = lhs
412 , cab_rhs = rhs }) =
413 text "CoAxBranch" <+> parens (ppr loc) <> colon
414 <+> brackets (fsep (punctuate comma (map pprType lhs)))
415 <+> text "=>" <+> pprType rhs
416
417 {-
418 ************************************************************************
419 * *
420 Roles
421 * *
422 ************************************************************************
423
424 Roles are defined here to avoid circular dependencies.
425 -}
426
427 -- See Note [Roles] in Coercion
428 -- defined here to avoid cyclic dependency with Coercion
429 data Role = Nominal | Representational | Phantom
430 deriving (Eq, Ord, Data.Data)
431
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
436 fsFromRole :: Role -> FastString
437 fsFromRole Nominal = fsLit "nominal"
438 fsFromRole Representational = fsLit "representational"
439 fsFromRole Phantom = fsLit "phantom"
440
441 instance Outputable Role where
442 ppr = ftext . fsFromRole
443
444 instance Binary Role where
445 put_ bh Nominal = putByte bh 1
446 put_ bh Representational = putByte bh 2
447 put_ bh Phantom = putByte bh 3
448
449 get bh = do tag <- getByte bh
450 case tag of 1 -> return Nominal
451 2 -> return Representational
452 3 -> return Phantom
453 _ -> panic ("get Role " ++ show tag)
454
455 {-
456 ************************************************************************
457 * *
458 CoAxiomRule
459 Rules for building Evidence
460 * *
461 ************************************************************************
462
463 Conditional axioms. The general idea is that a `CoAxiomRule` looks like this:
464
465 forall as. (r1 ~ r2, s1 ~ s2) => t1 ~ t2
466
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 -}
472
473 -- | A more explicit representation for `t1 ~ t2`.
474 type Eqn = Pair Type
475
476 -- | For now, we work only with nominal equality.
477 data CoAxiomRule = CoAxiomRule
478 { coaxrName :: FastString
479 , coaxrAsmpRoles :: [Role] -- roles of parameter equations
480 , coaxrRole :: Role -- role of resulting equation
481 , coaxrProves :: [Eqn] -> Maybe Eqn
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 }
487
488 instance Data.Data CoAxiomRule where
489 -- don't traverse?
490 toConstr _ = abstractConstr "CoAxiomRule"
491 gunfold _ _ = error "gunfold"
492 dataTypeOf _ = mkNoRepType "CoAxiomRule"
493
494 instance Uniquable CoAxiomRule where
495 getUnique = getUnique . coaxrName
496
497 instance Eq CoAxiomRule where
498 x == y = coaxrName x == coaxrName y
499
500 instance Ord CoAxiomRule where
501 compare x y = compare (coaxrName x) (coaxrName y)
502
503 instance Outputable CoAxiomRule where
504 ppr = ppr . coaxrName
505
506
507 -- Type checking of built-in families
508 data BuiltInSynFamily = BuiltInSynFamily
509 { sfMatchFam :: [Type] -> Maybe (CoAxiomRule, [Type], Type)
510 , sfInteractTop :: [Type] -> Type -> [Eqn]
511 , sfInteractInert :: [Type] -> Type ->
512 [Type] -> Type -> [Eqn]
513 }
514
515 -- Provides default implementations that do nothing.
516 trivialBuiltInFamily :: BuiltInSynFamily
517 trivialBuiltInFamily = BuiltInSynFamily
518 { sfMatchFam = \_ -> Nothing
519 , sfInteractTop = \_ _ -> []
520 , sfInteractInert = \_ _ _ _ -> []
521 }