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