Updated documentation; changed "group" to "branched" in type families
[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(..), 
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 [Branched instance checking] 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; not necessarily fresh
223                                    -- See Note [CoAxBranch type variables]
224     , cab_lhs      :: [Type]       -- Type patterns to match against
225     , cab_rhs      :: Type         -- Right-hand side of the equality
226     }
227   deriving Typeable
228
229 toBranchedAxiom :: CoAxiom br -> CoAxiom Branched
230 toBranchedAxiom (CoAxiom unique name tc branches implicit)
231   = CoAxiom unique name tc (toBranchedList branches) implicit
232
233 toUnbranchedAxiom :: CoAxiom br -> CoAxiom Unbranched
234 toUnbranchedAxiom (CoAxiom unique name tc branches implicit)
235   = CoAxiom unique name tc (toUnbranchedList branches) implicit
236
237 coAxiomNthBranch :: CoAxiom br -> BranchIndex -> CoAxBranch
238 coAxiomNthBranch (CoAxiom { co_ax_branches = bs }) index
239   = brListNth bs index
240
241 coAxiomArity :: CoAxiom br -> BranchIndex -> Arity
242 coAxiomArity ax index
243   = length $ cab_tvs $ coAxiomNthBranch ax index
244
245 coAxiomName :: CoAxiom br -> Name
246 coAxiomName = co_ax_name
247
248 coAxiomBranches :: CoAxiom br -> BranchList CoAxBranch br
249 coAxiomBranches = co_ax_branches
250
251 coAxiomSingleBranch_maybe :: CoAxiom br -> Maybe CoAxBranch
252 coAxiomSingleBranch_maybe (CoAxiom { co_ax_branches = branches })
253   | FirstBranch br <- branches
254   = Just br
255   | otherwise
256   = Nothing
257
258 coAxiomSingleBranch :: CoAxiom Unbranched -> CoAxBranch
259 coAxiomSingleBranch (CoAxiom { co_ax_branches = FirstBranch br }) = br
260
261 coAxiomTyCon :: CoAxiom br -> TyCon
262 coAxiomTyCon = co_ax_tc
263
264 coAxBranchTyVars :: CoAxBranch -> [TyVar]
265 coAxBranchTyVars = cab_tvs
266
267 coAxBranchLHS :: CoAxBranch -> [Type]
268 coAxBranchLHS = cab_lhs
269
270 coAxBranchRHS :: CoAxBranch -> Type
271 coAxBranchRHS = cab_rhs
272
273 coAxBranchSpan :: CoAxBranch -> SrcSpan
274 coAxBranchSpan = cab_loc
275
276 isImplicitCoAxiom :: CoAxiom br -> Bool
277 isImplicitCoAxiom = co_ax_implicit
278
279 \end{code}
280
281 Note [CoAxBranch type variables]
282 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
283 In the case of a CoAxBranch of an associated type-family instance, 
284 we use the *same* type variables (where possible) as the
285 enclosing class or instance.  Consider
286    class C a b where
287      type F x b 
288      type F [y] b = ...     -- Second param must be b
289
290    instance C Int [z] where
291      type F Int [z] = ...   -- Second param must be [z]
292
293 In the CoAxBranch in the instance decl (F Int [z]) we use the
294 same 'z', so that it's easy to check that that type is the same
295 as that in the instance header.  
296
297 Similarly in the CoAxBranch for the default decl for F in the
298 class decl, we use the same 'b' to make the same check easy.
299
300 So, unlike FamInsts, there is no expectation that the cab_tvs
301 are fresh wrt each other, or any other CoAxBranch.
302
303 Note [CoAxiom locations]
304 ~~~~~~~~~~~~~~~~~~~~~~~~
305 The source location of a CoAxiom is stored in two places in the
306 datatype tree. 
307   * The first is in the location info buried in the Name of the
308     CoAxiom. This span includes all of the branches of a branched
309     CoAxiom.
310   * The second is in the cab_loc fields of the CoAxBranches.  
311
312 In the case of a single branch, we can extract the source location of
313 the branch from the name of the CoAxiom. In other cases, we need an
314 explicit SrcSpan to correctly store the location of the equation
315 giving rise to the FamInstBranch.
316
317 Note [Implicit axioms]
318 ~~~~~~~~~~~~~~~~~~~~~~
319 See also Note [Implicit TyThings] in HscTypes
320 * A CoAxiom arising from data/type family instances is not "implicit".
321   That is, it has its own IfaceAxiom declaration in an interface file
322
323 * The CoAxiom arising from a newtype declaration *is* "implicit".
324   That is, it does not have its own IfaceAxiom declaration in an
325   interface file; instead the CoAxiom is generated by type-checking
326   the newtype declaration
327
328 \begin{code}
329 instance Eq (CoAxiom br) where
330     a == b = case (a `compare` b) of { EQ -> True;   _ -> False }
331     a /= b = case (a `compare` b) of { EQ -> False;  _ -> True  }
332
333 instance Ord (CoAxiom br) where
334     a <= b = case (a `compare` b) of { LT -> True;  EQ -> True;  GT -> False }
335     a <  b = case (a `compare` b) of { LT -> True;  EQ -> False; GT -> False }
336     a >= b = case (a `compare` b) of { LT -> False; EQ -> True;  GT -> True  }
337     a >  b = case (a `compare` b) of { LT -> False; EQ -> False; GT -> True  }
338     compare a b = getUnique a `compare` getUnique b
339
340 instance Uniquable (CoAxiom br) where
341     getUnique = co_ax_unique
342
343 instance Outputable (CoAxiom br) where
344     ppr = ppr . getName
345
346 instance NamedThing (CoAxiom br) where
347     getName = co_ax_name
348
349 instance Typeable br => Data.Data (CoAxiom br) where
350     -- don't traverse?
351     toConstr _   = abstractConstr "CoAxiom"
352     gunfold _ _  = error "gunfold"
353     dataTypeOf _ = mkNoRepType "CoAxiom"
354 \end{code}
355