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