De-orphan a load of Binary instances
[ghc.git] / compiler / types / CoAxiom.lhs
1 %
2 % (c) The University of Glasgow 2012
3 %
4
5 \begin{code}
6
7 {-# LANGUAGE GADTs, ScopedTypeVariables #-}
8
9 -- | Module for coercion axioms, used to represent type family instances
10 -- and newtypes
11
12 module CoAxiom (
13        Branched, Unbranched, BranchIndex, BranchList(..),
14        toBranchList, fromBranchList,
15        toBranchedList, toUnbranchedList,
16        brListLength, brListNth, brListMap, brListFoldr, brListMapM,
17        brListFoldlM_, brListZipWith,
18
19        CoAxiom(..), CoAxBranch(..), 
20
21        toBranchedAxiom, toUnbranchedAxiom,
22        coAxiomName, coAxiomArity, coAxiomBranches,
23        coAxiomTyCon, isImplicitCoAxiom, coAxiomNumPats,
24        coAxiomNthBranch, coAxiomSingleBranch_maybe,
25        coAxiomSingleBranch, coAxBranchTyVars, coAxBranchLHS,
26        coAxBranchRHS, coAxBranchSpan, coAxBranchIncomps,
27        placeHolderIncomps
28        ) where 
29
30 import {-# SOURCE #-} TypeRep ( Type )
31 import {-# SOURCE #-} TyCon ( TyCon )
32 import Outputable
33 import Name
34 import Unique
35 import Var
36 import Util
37 import BasicTypes
38 import Data.Typeable ( Typeable )
39 import SrcLoc
40 import qualified Data.Data as Data
41
42 #include "HsVersions.h"
43
44 \end{code}
45
46 Note [Coercion axiom branches]
47 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
48 In order to allow type family instance groups, an axiom needs to contain an
49 ordered list of alternatives, called branches. The kind of the coercion built
50 from an axiom is determined by which index is used when building the coercion
51 from the axiom.
52
53 For example, consider the axiom derived from the following declaration:
54
55 type instance where
56   F [Int] = Bool
57   F [a]   = Double
58   F (a b) = Char
59
60 This will give rise to this axiom:
61
62 axF :: {                                           F [Int] ~ Bool
63        ; forall (a :: *).                          F [a]   ~ Double
64        ; forall (k :: BOX) (a :: k -> *) (b :: k). F (a b) ~ Char
65        }
66
67 The axiom is used with the AxiomInstCo constructor of Coercion. If we wish
68 to have a coercion showing that F (Maybe Int) ~ Char, it will look like
69
70 axF[2] <*> <Maybe> <Int> :: F (Maybe Int) ~ Char
71 -- or, written using concrete-ish syntax --
72 AxiomInstCo axF 2 [Refl *, Refl Maybe, Refl Int]
73
74 Note that the index is 0-based.
75
76 For type-checking, it is also necessary to check that no previous pattern
77 can unify with the supplied arguments. After all, it is possible that some
78 of the type arguments are lambda-bound type variables whose instantiation may
79 cause an earlier match among the branches. We wish to prohibit this behavior,
80 so the type checker rules out the choice of a branch where a previous branch
81 can unify. See also [Branched instance checking] in FamInstEnv.hs.
82
83 For example, the following is malformed, where 'a' is a lambda-bound type
84 variable:
85
86 axF[2] <*> <a> <Bool> :: F (a Bool) ~ Char
87
88 Why? Because a might be instantiated with [], meaning that branch 1 should
89 apply, not branch 2. This is a vital consistency check; without it, we could
90 derive Int ~ Bool, and that is a Bad Thing.
91
92 Note [Branched axioms]
93 ~~~~~~~~~~~~~~~~~~~~~~~
94 Although a CoAxiom has the capacity to store many branches, in certain cases,
95 we want only one. These cases are in data/newtype family instances, newtype
96 coercions, and type family instances declared with "type instance ...", not
97 "type instance where". Furthermore, these unbranched axioms are used in a
98 variety of places throughout GHC, and it would difficult to generalize all of
99 that code to deal with branched axioms, especially when the code can be sure
100 of the fact that an axiom is indeed a singleton. At the same time, it seems
101 dangerous to assume singlehood in various places through GHC.
102
103 The solution to this is to label a CoAxiom with a phantom type variable
104 declaring whether it is known to be a singleton or not. The list of branches
105 is stored using a special form of list, declared below, that ensures that the
106 type variable is accurate.
107
108 As of this writing (Dec 2012), it would not be appropriate to use a promoted
109 type as the phantom type, so we use empty datatypes. We wish to have GHC
110 remain compilable with GHC 7.2.1. If you are revising this code and GHC no
111 longer needs to remain compatible with GHC 7.2.x, then please update this
112 code to use promoted types.
113
114
115 %************************************************************************
116 %*                                                                      *
117                     Branch lists
118 %*                                                                      *
119 %************************************************************************
120
121 \begin{code}
122 type BranchIndex = Int  -- The index of the branch in the list of branches
123                         -- Counting from zero
124
125 -- the phantom type labels
126 data Unbranched deriving Typeable
127 data Branched deriving Typeable
128
129 data BranchList a br where
130   FirstBranch :: a -> BranchList a br
131   NextBranch :: a -> BranchList a br -> BranchList a Branched
132
133 -- convert to/from lists
134 toBranchList :: [a] -> BranchList a Branched
135 toBranchList [] = pprPanic "toBranchList" empty
136 toBranchList [b] = FirstBranch b
137 toBranchList (h:t) = NextBranch h (toBranchList t)
138
139 fromBranchList :: BranchList a br -> [a]
140 fromBranchList (FirstBranch b) = [b]
141 fromBranchList (NextBranch h t) = h : (fromBranchList t)
142
143 -- convert from any BranchList to a Branched BranchList
144 toBranchedList :: BranchList a br -> BranchList a Branched
145 toBranchedList (FirstBranch b) = FirstBranch b
146 toBranchedList (NextBranch h t) = NextBranch h t
147
148 -- convert from any BranchList to an Unbranched BranchList
149 toUnbranchedList :: BranchList a br -> BranchList a Unbranched
150 toUnbranchedList (FirstBranch b) = FirstBranch b
151 toUnbranchedList _ = pprPanic "toUnbranchedList" empty
152
153 -- length
154 brListLength :: BranchList a br -> Int
155 brListLength (FirstBranch _) = 1
156 brListLength (NextBranch _ t) = 1 + brListLength t
157
158 -- lookup
159 brListNth :: BranchList a br -> BranchIndex -> a
160 brListNth (FirstBranch b) 0 = b
161 brListNth (NextBranch h _) 0 = h
162 brListNth (NextBranch _ t) n = brListNth t (n-1)
163 brListNth _ _ = pprPanic "brListNth" empty
164
165 -- map, fold
166 brListMap :: (a -> b) -> BranchList a br -> [b]
167 brListMap f (FirstBranch b) = [f b]
168 brListMap f (NextBranch h t) = f h : (brListMap f t)
169
170 brListFoldr :: (a -> b -> b) -> b -> BranchList a br -> b
171 brListFoldr f x (FirstBranch b) = f b x
172 brListFoldr f x (NextBranch h t) = f h (brListFoldr f x t)
173
174 brListMapM :: Monad m => (a -> m b) -> BranchList a br -> m [b]
175 brListMapM f (FirstBranch b) = f b >>= \fb -> return [fb]
176 brListMapM f (NextBranch h t) = do { fh <- f h
177                                    ; ft <- brListMapM f t
178                                    ; return (fh : ft) }
179
180 brListFoldlM_ :: forall a b m br. Monad m
181               => (a -> b -> m a) -> a -> BranchList b br -> m ()
182 brListFoldlM_ f z brs = do { _ <- go z brs
183                            ; return () }
184   where go :: forall br'. Monad m => a -> BranchList b br' -> m a
185         go acc (FirstBranch b)  = f acc b
186         go acc (NextBranch h t) = do { fh <- f acc h
187                                      ; go fh t }
188
189 -- zipWith
190 brListZipWith :: (a -> b -> c) -> BranchList a br1 -> BranchList b br2 -> [c]
191 brListZipWith f (FirstBranch a) (FirstBranch b) = [f a b]
192 brListZipWith f (FirstBranch a) (NextBranch b _) = [f a b]
193 brListZipWith f (NextBranch a _) (FirstBranch b) = [f a b]
194 brListZipWith f (NextBranch a ta) (NextBranch b tb) = f a b : brListZipWith f ta tb
195
196 -- pretty-printing
197
198 instance Outputable a => Outputable (BranchList a br) where
199   ppr = ppr . fromBranchList
200 \end{code}
201
202 %************************************************************************
203 %*                                                                      *
204                     Coercion axioms
205 %*                                                                      *
206 %************************************************************************
207
208 Note [Storing compatibility]
209 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~
210 During axiom application, we need to be aware of which branches are compatible
211 with which others. The full explanation is in Note [Compatibility] in
212 FamInstEnv. (The code is placed there to avoid a dependency from CoAxiom on
213 the unification algorithm.) Although we could theoretically compute
214 compatibility on the fly, this is silly, so we store it in a CoAxiom.
215
216 Specifically, each branch refers to all other branches with which it is
217 incompatible. This list might well be empty, and it will always be for the
218 first branch of any axiom.
219
220 CoAxBranches that do not (yet) belong to a CoAxiom should have a panic thunk
221 stored in cab_incomps. The incompatibilities are properly a property of the
222 axiom as a whole, and they are computed only when the final axiom is built.
223
224 During serialization, the list is converted into a list of the indices
225 of the branches.
226
227 \begin{code}
228 -- | A 'CoAxiom' is a \"coercion constructor\", i.e. a named equality axiom.
229
230 -- If you edit this type, you may need to update the GHC formalism
231 -- See Note [GHC Formalism] in coreSyn/CoreLint.lhs
232 data CoAxiom br
233   = CoAxiom                   -- Type equality axiom.
234     { co_ax_unique   :: Unique        -- unique identifier
235     , co_ax_name     :: Name          -- name for pretty-printing
236     , co_ax_tc       :: TyCon         -- the head of the LHS patterns
237     , co_ax_branches :: BranchList CoAxBranch br
238                                       -- the branches that form this axiom
239     , co_ax_implicit :: Bool          -- True <=> the axiom is "implicit"
240                                       -- See Note [Implicit axioms]
241          -- INVARIANT: co_ax_implicit == True implies length co_ax_branches == 1.
242     }
243   deriving Typeable
244
245 data CoAxBranch
246   = CoAxBranch
247     { cab_loc      :: SrcSpan       -- Location of the defining equation
248                                     -- See Note [CoAxiom locations]
249     , cab_tvs      :: [TyVar]       -- Bound type variables; not necessarily fresh
250                                     -- See Note [CoAxBranch type variables]
251     , cab_lhs      :: [Type]        -- Type patterns to match against
252     , cab_rhs      :: Type          -- Right-hand side of the equality
253     , cab_incomps  :: [CoAxBranch]  -- The previous incompatible branches
254                                     -- See Note [Storing compatibility]
255     }
256   deriving Typeable
257
258 toBranchedAxiom :: CoAxiom br -> CoAxiom Branched
259 toBranchedAxiom (CoAxiom unique name tc branches implicit)
260   = CoAxiom unique name tc (toBranchedList branches) implicit
261
262 toUnbranchedAxiom :: CoAxiom br -> CoAxiom Unbranched
263 toUnbranchedAxiom (CoAxiom unique name tc branches implicit)
264   = CoAxiom unique name tc (toUnbranchedList branches) implicit
265
266 coAxiomNumPats :: CoAxiom br -> Int
267 coAxiomNumPats = length . coAxBranchLHS . (flip coAxiomNthBranch 0)
268
269 coAxiomNthBranch :: CoAxiom br -> BranchIndex -> CoAxBranch
270 coAxiomNthBranch (CoAxiom { co_ax_branches = bs }) index
271   = brListNth bs index
272
273 coAxiomArity :: CoAxiom br -> BranchIndex -> Arity
274 coAxiomArity ax index
275   = length $ cab_tvs $ coAxiomNthBranch ax index
276
277 coAxiomName :: CoAxiom br -> Name
278 coAxiomName = co_ax_name
279
280 coAxiomBranches :: CoAxiom br -> BranchList CoAxBranch br
281 coAxiomBranches = co_ax_branches
282
283 coAxiomSingleBranch_maybe :: CoAxiom br -> Maybe CoAxBranch
284 coAxiomSingleBranch_maybe (CoAxiom { co_ax_branches = branches })
285   | FirstBranch br <- branches
286   = Just br
287   | otherwise
288   = Nothing
289
290 coAxiomSingleBranch :: CoAxiom Unbranched -> CoAxBranch
291 coAxiomSingleBranch (CoAxiom { co_ax_branches = FirstBranch br }) = br
292
293 coAxiomTyCon :: CoAxiom br -> TyCon
294 coAxiomTyCon = co_ax_tc
295
296 coAxBranchTyVars :: CoAxBranch -> [TyVar]
297 coAxBranchTyVars = cab_tvs
298
299 coAxBranchLHS :: CoAxBranch -> [Type]
300 coAxBranchLHS = cab_lhs
301
302 coAxBranchRHS :: CoAxBranch -> Type
303 coAxBranchRHS = cab_rhs
304
305 coAxBranchSpan :: CoAxBranch -> SrcSpan
306 coAxBranchSpan = cab_loc
307
308 isImplicitCoAxiom :: CoAxiom br -> Bool
309 isImplicitCoAxiom = co_ax_implicit
310
311 coAxBranchIncomps :: CoAxBranch -> [CoAxBranch]
312 coAxBranchIncomps = cab_incomps
313
314 placeHolderIncomps :: [CoAxBranch]
315 placeHolderIncomps = panic "placeHolderIncomps"
316
317 \end{code}
318
319 Note [CoAxBranch type variables]
320 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
321 In the case of a CoAxBranch of an associated type-family instance, 
322 we use the *same* type variables (where possible) as the
323 enclosing class or instance.  Consider
324    class C a b where
325      type F x b 
326      type F [y] b = ...     -- Second param must be b
327
328    instance C Int [z] where
329      type F Int [z] = ...   -- Second param must be [z]
330
331 In the CoAxBranch in the instance decl (F Int [z]) we use the
332 same 'z', so that it's easy to check that that type is the same
333 as that in the instance header.  
334
335 Similarly in the CoAxBranch for the default decl for F in the
336 class decl, we use the same 'b' to make the same check easy.
337
338 So, unlike FamInsts, there is no expectation that the cab_tvs
339 are fresh wrt each other, or any other CoAxBranch.
340
341 Note [CoAxiom locations]
342 ~~~~~~~~~~~~~~~~~~~~~~~~
343 The source location of a CoAxiom is stored in two places in the
344 datatype tree. 
345   * The first is in the location info buried in the Name of the
346     CoAxiom. This span includes all of the branches of a branched
347     CoAxiom.
348   * The second is in the cab_loc fields of the CoAxBranches.  
349
350 In the case of a single branch, we can extract the source location of
351 the branch from the name of the CoAxiom. In other cases, we need an
352 explicit SrcSpan to correctly store the location of the equation
353 giving rise to the FamInstBranch.
354
355 Note [Implicit axioms]
356 ~~~~~~~~~~~~~~~~~~~~~~
357 See also Note [Implicit TyThings] in HscTypes
358 * A CoAxiom arising from data/type family instances is not "implicit".
359   That is, it has its own IfaceAxiom declaration in an interface file
360
361 * The CoAxiom arising from a newtype declaration *is* "implicit".
362   That is, it does not have its own IfaceAxiom declaration in an
363   interface file; instead the CoAxiom is generated by type-checking
364   the newtype declaration
365
366 \begin{code}
367 instance Eq (CoAxiom br) where
368     a == b = case (a `compare` b) of { EQ -> True;   _ -> False }
369     a /= b = case (a `compare` b) of { EQ -> False;  _ -> True  }
370
371 instance Ord (CoAxiom br) where
372     a <= b = case (a `compare` b) of { LT -> True;  EQ -> True;  GT -> False }
373     a <  b = case (a `compare` b) of { LT -> True;  EQ -> False; GT -> False }
374     a >= b = case (a `compare` b) of { LT -> False; EQ -> True;  GT -> True  }
375     a >  b = case (a `compare` b) of { LT -> False; EQ -> False; GT -> True  }
376     compare a b = getUnique a `compare` getUnique b
377
378 instance Uniquable (CoAxiom br) where
379     getUnique = co_ax_unique
380
381 instance Outputable (CoAxiom br) where
382     ppr = ppr . getName
383
384 instance NamedThing (CoAxiom br) where
385     getName = co_ax_name
386
387 instance Typeable br => Data.Data (CoAxiom br) where
388     -- don't traverse?
389     toConstr _   = abstractConstr "CoAxiom"
390     gunfold _ _  = error "gunfold"
391     dataTypeOf _ = mkNoRepType "CoAxiom"
392 \end{code}
393