never executed always true always false
1 {-# LANGUAGE DataKinds #-}
2 {-# LANGUAGE DeriveDataTypeable #-}
3 {-# LANGUAGE GADTs #-}
4 {-# LANGUAGE KindSignatures #-}
5 {-# LANGUAGE RoleAnnotations #-}
6 {-# LANGUAGE ScopedTypeVariables #-}
7
8 -- (c) The University of Glasgow 2012
9
10 -- | Module for coercion axioms, used to represent type family instances
11 -- and newtypes
12
13 module GHC.Core.Coercion.Axiom (
14 BranchFlag, Branched, Unbranched, BranchIndex, Branches(..),
15 manyBranches, unbranched,
16 fromBranches, numBranches,
17 mapAccumBranches,
18
19 CoAxiom(..), CoAxBranch(..),
20
21 toBranchedAxiom, toUnbranchedAxiom,
22 coAxiomName, coAxiomArity, coAxiomBranches,
23 coAxiomTyCon, isImplicitCoAxiom, coAxiomNumPats,
24 coAxiomNthBranch, coAxiomSingleBranch_maybe, coAxiomRole,
25 coAxiomSingleBranch, coAxBranchTyVars, coAxBranchCoVars,
26 coAxBranchRoles,
27 coAxBranchLHS, coAxBranchRHS, coAxBranchSpan, coAxBranchIncomps,
28 placeHolderIncomps,
29
30 Role(..), fsFromRole,
31
32 CoAxiomRule(..), TypeEqn,
33 BuiltInSynFamily(..), trivialBuiltInFamily
34 ) where
35
36 import GHC.Prelude
37
38 import {-# SOURCE #-} GHC.Core.TyCo.Rep ( Type )
39 import {-# SOURCE #-} GHC.Core.TyCo.Ppr ( pprType )
40 import {-# SOURCE #-} GHC.Core.TyCon ( TyCon )
41 import GHC.Utils.Outputable
42 import GHC.Data.FastString
43 import GHC.Types.Name
44 import GHC.Types.Unique
45 import GHC.Types.Var
46 import GHC.Utils.Misc
47 import GHC.Utils.Binary
48 import GHC.Utils.Panic
49 import GHC.Utils.Panic.Plain
50 import GHC.Data.Pair
51 import GHC.Types.Basic
52 import Data.Typeable ( Typeable )
53 import GHC.Types.SrcLoc
54 import qualified Data.Data as Data
55 import Data.Array
56 import Data.List ( mapAccumL )
57
58 {-
59 Note [Coercion axiom branches]
60 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
61 In order to allow closed type families, an axiom needs to contain an
62 ordered list of alternatives, called branches. The kind of the coercion built
63 from an axiom is determined by which index is used when building the coercion
64 from the axiom.
65
66 For example, consider the axiom derived from the following declaration:
67
68 type family F a where
69 F [Int] = Bool
70 F [a] = Double
71 F (a b) = Char
72
73 This will give rise to this axiom:
74
75 axF :: { F [Int] ~ Bool
76 ; forall (a :: *). F [a] ~ Double
77 ; forall (k :: *) (a :: k -> *) (b :: k). F (a b) ~ Char
78 }
79
80 The axiom is used with the AxiomInstCo constructor of Coercion. If we wish
81 to have a coercion showing that F (Maybe Int) ~ Char, it will look like
82
83 axF[2] <*> <Maybe> <Int> :: F (Maybe Int) ~ Char
84 -- or, written using concrete-ish syntax --
85 AxiomInstCo axF 2 [Refl *, Refl Maybe, Refl Int]
86
87 Note that the index is 0-based.
88
89 For type-checking, it is also necessary to check that no previous pattern
90 can unify with the supplied arguments. After all, it is possible that some
91 of the type arguments are lambda-bound type variables whose instantiation may
92 cause an earlier match among the branches. We wish to prohibit this behavior,
93 so the type checker rules out the choice of a branch where a previous branch
94 can unify. See also [Apartness] in GHC.Core.FamInstEnv.
95
96 For example, the following is malformed, where 'a' is a lambda-bound type
97 variable:
98
99 axF[2] <*> <a> <Bool> :: F (a Bool) ~ Char
100
101 Why? Because a might be instantiated with [], meaning that branch 1 should
102 apply, not branch 2. This is a vital consistency check; without it, we could
103 derive Int ~ Bool, and that is a Bad Thing.
104
105 Note [Branched axioms]
106 ~~~~~~~~~~~~~~~~~~~~~~
107 Although a CoAxiom has the capacity to store many branches, in certain cases,
108 we want only one. These cases are in data/newtype family instances, newtype
109 coercions, and type family instances.
110 Furthermore, these unbranched axioms are used in a
111 variety of places throughout GHC, and it would difficult to generalize all of
112 that code to deal with branched axioms, especially when the code can be sure
113 of the fact that an axiom is indeed a singleton. At the same time, it seems
114 dangerous to assume singlehood in various places through GHC.
115
116 The solution to this is to label a CoAxiom with a phantom type variable
117 declaring whether it is known to be a singleton or not. The branches
118 are stored using a special datatype, declared below, that ensures that the
119 type variable is accurate.
120
121 ************************************************************************
122 * *
123 Branches
124 * *
125 ************************************************************************
126 -}
127
128 type BranchIndex = Int -- The index of the branch in the list of branches
129 -- Counting from zero
130
131 -- promoted data type
132 data BranchFlag = Branched | Unbranched
133 type Branched = 'Branched
134 type Unbranched = 'Unbranched
135 -- By using type synonyms for the promoted constructors, we avoid needing
136 -- DataKinds and the promotion quote in client modules. This also means that
137 -- we don't need to export the term-level constructors, which should never be used.
138
139 newtype Branches (br :: BranchFlag)
140 = MkBranches { unMkBranches :: Array BranchIndex CoAxBranch }
141 type role Branches nominal
142
143 manyBranches :: [CoAxBranch] -> Branches Branched
144 manyBranches brs = assert (snd bnds >= fst bnds )
145 MkBranches (listArray bnds brs)
146 where
147 bnds = (0, length brs - 1)
148
149 unbranched :: CoAxBranch -> Branches Unbranched
150 unbranched br = MkBranches (listArray (0, 0) [br])
151
152 toBranched :: Branches br -> Branches Branched
153 toBranched = MkBranches . unMkBranches
154
155 toUnbranched :: Branches br -> Branches Unbranched
156 toUnbranched (MkBranches arr) = assert (bounds arr == (0,0) )
157 MkBranches arr
158
159 fromBranches :: Branches br -> [CoAxBranch]
160 fromBranches = elems . unMkBranches
161
162 branchesNth :: Branches br -> BranchIndex -> CoAxBranch
163 branchesNth (MkBranches arr) n = arr ! n
164
165 numBranches :: Branches br -> Int
166 numBranches (MkBranches arr) = snd (bounds arr) + 1
167
168 -- | The @[CoAxBranch]@ passed into the mapping function is a list of
169 -- all previous branches, reversed
170 mapAccumBranches :: ([CoAxBranch] -> CoAxBranch -> CoAxBranch)
171 -> Branches br -> Branches br
172 mapAccumBranches f (MkBranches arr)
173 = MkBranches (listArray (bounds arr) (snd $ mapAccumL go [] (elems arr)))
174 where
175 go :: [CoAxBranch] -> CoAxBranch -> ([CoAxBranch], CoAxBranch)
176 go prev_branches cur_branch = ( cur_branch : prev_branches
177 , f prev_branches cur_branch )
178
179
180 {-
181 ************************************************************************
182 * *
183 Coercion axioms
184 * *
185 ************************************************************************
186
187 Note [Storing compatibility]
188 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~
189 During axiom application, we need to be aware of which branches are compatible
190 with which others. The full explanation is in Note [Compatibility] in
191 GHc.Core.FamInstEnv. (The code is placed there to avoid a dependency from
192 GHC.Core.Coercion.Axiom on the unification algorithm.) Although we could
193 theoretically compute compatibility on the fly, this is silly, so we store it
194 in a CoAxiom.
195
196 Specifically, each branch refers to all other branches with which it is
197 incompatible. This list might well be empty, and it will always be for the
198 first branch of any axiom.
199
200 CoAxBranches that do not (yet) belong to a CoAxiom should have a panic thunk
201 stored in cab_incomps. The incompatibilities are properly a property of the
202 axiom as a whole, and they are computed only when the final axiom is built.
203
204 During serialization, the list is converted into a list of the indices
205 of the branches.
206
207 Note [CoAxioms are homogeneous]
208 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
209 All axioms must be *homogeneous*, meaning that the kind of the LHS must
210 match the kind of the RHS. In practice, this means:
211
212 Given a CoAxiom { co_ax_tc = ax_tc },
213 for every branch CoAxBranch { cab_lhs = lhs, cab_rhs = rhs }:
214 typeKind (mkTyConApp ax_tc lhs) `eqType` typeKind rhs
215
216 This is checked in FamInstEnv.mkCoAxBranch.
217 -}
218
219 -- | A 'CoAxiom' is a \"coercion constructor\", i.e. a named equality axiom.
220
221 -- If you edit this type, you may need to update the GHC formalism
222 -- See Note [GHC Formalism] in GHC.Core.Lint
223 data CoAxiom br
224 = CoAxiom -- Type equality axiom.
225 { co_ax_unique :: Unique -- Unique identifier
226 , co_ax_name :: Name -- Name for pretty-printing
227 , co_ax_role :: Role -- Role of the axiom's equality
228 , co_ax_tc :: TyCon -- The head of the LHS patterns
229 -- e.g. the newtype or family tycon
230 , co_ax_branches :: Branches br -- The branches that form this axiom
231 , co_ax_implicit :: Bool -- True <=> the axiom is "implicit"
232 -- See Note [Implicit axioms]
233 -- INVARIANT: co_ax_implicit == True implies length co_ax_branches == 1.
234 }
235
236 data CoAxBranch
237 = CoAxBranch
238 { cab_loc :: SrcSpan -- Location of the defining equation
239 -- See Note [CoAxiom locations]
240 , cab_tvs :: [TyVar] -- Bound type variables; not necessarily fresh
241 -- See Note [CoAxBranch type variables]
242 , cab_eta_tvs :: [TyVar] -- Eta-reduced tyvars
243 -- cab_tvs and cab_lhs may be eta-reduced; see
244 -- Note [Eta reduction for data families]
245 , cab_cvs :: [CoVar] -- Bound coercion variables
246 -- Always empty, for now.
247 -- See Note [Constraints in patterns]
248 -- in GHC.Tc.TyCl
249 , cab_roles :: [Role] -- See Note [CoAxBranch roles]
250 , cab_lhs :: [Type] -- Type patterns to match against
251 , cab_rhs :: Type -- Right-hand side of the equality
252 -- See Note [CoAxioms are homogeneous]
253 , cab_incomps :: [CoAxBranch] -- The previous incompatible branches
254 -- See Note [Storing compatibility]
255 }
256 deriving Data.Data
257
258 toBranchedAxiom :: CoAxiom br -> CoAxiom Branched
259 toBranchedAxiom (CoAxiom unique name role tc branches implicit)
260 = CoAxiom unique name role tc (toBranched branches) implicit
261
262 toUnbranchedAxiom :: CoAxiom br -> CoAxiom Unbranched
263 toUnbranchedAxiom (CoAxiom unique name role tc branches implicit)
264 = CoAxiom unique name role tc (toUnbranched 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 = branchesNth bs index
272
273 coAxiomArity :: CoAxiom br -> BranchIndex -> Arity
274 coAxiomArity ax index
275 = length tvs + length cvs
276 where
277 CoAxBranch { cab_tvs = tvs, cab_cvs = cvs } = coAxiomNthBranch ax index
278
279 coAxiomName :: CoAxiom br -> Name
280 coAxiomName = co_ax_name
281
282 coAxiomRole :: CoAxiom br -> Role
283 coAxiomRole = co_ax_role
284
285 coAxiomBranches :: CoAxiom br -> Branches br
286 coAxiomBranches = co_ax_branches
287
288 coAxiomSingleBranch_maybe :: CoAxiom br -> Maybe CoAxBranch
289 coAxiomSingleBranch_maybe (CoAxiom { co_ax_branches = MkBranches arr })
290 | snd (bounds arr) == 0
291 = Just $ arr ! 0
292 | otherwise
293 = Nothing
294
295 coAxiomSingleBranch :: CoAxiom Unbranched -> CoAxBranch
296 coAxiomSingleBranch (CoAxiom { co_ax_branches = MkBranches arr })
297 = arr ! 0
298
299 coAxiomTyCon :: CoAxiom br -> TyCon
300 coAxiomTyCon = co_ax_tc
301
302 coAxBranchTyVars :: CoAxBranch -> [TyVar]
303 coAxBranchTyVars = cab_tvs
304
305 coAxBranchCoVars :: CoAxBranch -> [CoVar]
306 coAxBranchCoVars = cab_cvs
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 -- See Note [Compatibility checking] in GHC.Core.FamInstEnv
327 placeHolderIncomps :: [CoAxBranch]
328 placeHolderIncomps = panic "placeHolderIncomps"
329
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
337 instance C Int [z] where
338 type F Int [z] = ... -- Second param must be [z]
339
340 In the CoAxBranch in the instance decl (F Int [z]) we use the
341 same 'z', so that it's easy to check that that type is the same
342 as that in the instance header.
343
344 So, unlike FamInsts, there is no expectation that the cab_tvs
345 are fresh wrt each other, or any other CoAxBranch.
346
347 Note [CoAxBranch roles]
348 ~~~~~~~~~~~~~~~~~~~~~~~
349 Consider this code:
350
351 newtype Age = MkAge Int
352 newtype Wrap a = MkWrap a
353
354 convert :: Wrap Age -> Int
355 convert (MkWrap (MkAge i)) = i
356
357 We want this to compile to:
358
359 NTCo:Wrap :: forall a. Wrap a ~R a
360 NTCo:Age :: Age ~R Int
361 convert = \x -> x |> (NTCo:Wrap[0] NTCo:Age[0])
362
363 But, note that NTCo:Age is at role R. Thus, we need to be able to pass
364 coercions at role R into axioms. However, we don't *always* want to be able to
365 do this, as it would be disastrous with type families. The solution is to
366 annotate the arguments to the axiom with roles, much like we annotate tycon
367 tyvars. Where do these roles get set? Newtype axioms inherit their roles from
368 the newtype tycon; family axioms are all at role N.
369
370 Note [CoAxiom locations]
371 ~~~~~~~~~~~~~~~~~~~~~~~~
372 The source location of a CoAxiom is stored in two places in the
373 datatype tree.
374 * The first is in the location info buried in the Name of the
375 CoAxiom. This span includes all of the branches of a branched
376 CoAxiom.
377 * The second is in the cab_loc fields of the CoAxBranches.
378
379 In the case of a single branch, we can extract the source location of
380 the branch from the name of the CoAxiom. In other cases, we need an
381 explicit SrcSpan to correctly store the location of the equation
382 giving rise to the FamInstBranch.
383
384 Note [Implicit axioms]
385 ~~~~~~~~~~~~~~~~~~~~~~
386 See also Note [Implicit TyThings] in GHC.Types.TyThing
387 * A CoAxiom arising from data/type family instances is not "implicit".
388 That is, it has its own IfaceAxiom declaration in an interface file
389
390 * The CoAxiom arising from a newtype declaration *is* "implicit".
391 That is, it does not have its own IfaceAxiom declaration in an
392 interface file; instead the CoAxiom is generated by type-checking
393 the newtype declaration
394
395 Note [Eta reduction for data families]
396 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
397 Consider this
398 data family T a b :: *
399 newtype instance T Int a = MkT (IO a) deriving( Monad )
400 We'd like this to work.
401
402 From the 'newtype instance' you might think we'd get:
403 newtype TInt a = MkT (IO a)
404 axiom ax1 a :: T Int a ~ TInt a -- The newtype-instance part
405 axiom ax2 a :: TInt a ~ IO a -- The newtype part
406
407 But now what can we do? We have this problem
408 Given: d :: Monad IO
409 Wanted: d' :: Monad (T Int) = d |> ????
410 What coercion can we use for the ???
411
412 Solution: eta-reduce both axioms, thus:
413 axiom ax1 :: T Int ~ TInt
414 axiom ax2 :: TInt ~ IO
415 Now
416 d' = d |> Monad (sym (ax2 ; ax1))
417
418 ----- Bottom line ------
419
420 For a CoAxBranch for a data family instance with representation
421 TyCon rep_tc:
422
423 - cab_tvs (of its CoAxiom) may be shorter
424 than tyConTyVars of rep_tc.
425
426 - cab_lhs may be shorter than tyConArity of the family tycon
427 i.e. LHS is unsaturated
428
429 - cab_rhs will be (rep_tc cab_tvs)
430 i.e. RHS is un-saturated
431
432 - This eta reduction happens for data instances as well
433 as newtype instances. Here we want to eta-reduce the data family axiom.
434
435 - This eta-reduction is done in GHC.Tc.TyCl.Instance.tcDataFamInstDecl.
436
437 But for a /type/ family
438 - cab_lhs has the exact arity of the family tycon
439
440 There are certain situations (e.g., pretty-printing) where it is necessary to
441 deal with eta-expanded data family instances. For these situations, the
442 cab_eta_tvs field records the stuff that has been eta-reduced away.
443 So if we have
444 axiom forall a b. F [a->b] = D b a
445 and cab_eta_tvs is [p,q], then the original user-written definition
446 looked like
447 axiom forall a b p q. F [a->b] p q = D b a p q
448 (See #9692, #14179, and #15845 for examples of what can go wrong if
449 we don't eta-expand when showing things to the user.)
450
451 See also:
452
453 * Note [Newtype eta] in GHC.Core.TyCon. This is notionally separate
454 and deals with the axiom connecting a newtype with its representation
455 type; but it too is eta-reduced.
456 * Note [Implementing eta reduction for data families] in "GHC.Tc.TyCl.Instance". This
457 describes the implementation details of this eta reduction happen.
458 -}
459
460 instance Eq (CoAxiom br) where
461 a == b = getUnique a == getUnique b
462 a /= b = getUnique a /= getUnique b
463
464 instance Uniquable (CoAxiom br) where
465 getUnique = co_ax_unique
466
467 instance Outputable (CoAxiom br) where
468 ppr = ppr . getName
469
470 instance NamedThing (CoAxiom br) where
471 getName = co_ax_name
472
473 instance Typeable br => Data.Data (CoAxiom br) where
474 -- don't traverse?
475 toConstr _ = abstractConstr "CoAxiom"
476 gunfold _ _ = error "gunfold"
477 dataTypeOf _ = mkNoRepType "CoAxiom"
478
479 instance Outputable CoAxBranch where
480 ppr (CoAxBranch { cab_loc = loc
481 , cab_lhs = lhs
482 , cab_rhs = rhs }) =
483 text "CoAxBranch" <+> parens (ppr loc) <> colon
484 <+> brackets (fsep (punctuate comma (map pprType lhs)))
485 <+> text "=>" <+> pprType rhs
486
487 {-
488 ************************************************************************
489 * *
490 Roles
491 * *
492 ************************************************************************
493
494 Roles are defined here to avoid circular dependencies.
495 -}
496
497 -- See Note [Roles] in GHC.Core.Coercion
498 -- defined here to avoid cyclic dependency with GHC.Core.Coercion
499 --
500 -- Order of constructors matters: the Ord instance coincides with the *super*typing
501 -- relation on roles.
502 data Role = Nominal | Representational | Phantom
503 deriving (Eq, Ord, Data.Data)
504
505 -- These names are slurped into the parser code. Changing these strings
506 -- will change the **surface syntax** that GHC accepts! If you want to
507 -- change only the pretty-printing, do some replumbing. See
508 -- mkRoleAnnotDecl in GHC.Parser.PostProcess
509 fsFromRole :: Role -> FastString
510 fsFromRole Nominal = fsLit "nominal"
511 fsFromRole Representational = fsLit "representational"
512 fsFromRole Phantom = fsLit "phantom"
513
514 instance Outputable Role where
515 ppr = ftext . fsFromRole
516
517 instance Binary Role where
518 put_ bh Nominal = putByte bh 1
519 put_ bh Representational = putByte bh 2
520 put_ bh Phantom = putByte bh 3
521
522 get bh = do tag <- getByte bh
523 case tag of 1 -> return Nominal
524 2 -> return Representational
525 3 -> return Phantom
526 _ -> panic ("get Role " ++ show tag)
527
528 {-
529 ************************************************************************
530 * *
531 CoAxiomRule
532 Rules for building Evidence
533 * *
534 ************************************************************************
535
536 Conditional axioms. The general idea is that a `CoAxiomRule` looks like this:
537
538 forall as. (r1 ~ r2, s1 ~ s2) => t1 ~ t2
539
540 My intention is to reuse these for both (~) and (~#).
541 The short-term plan is to use this datatype to represent the type-nat axioms.
542 In the longer run, it may be good to unify this and `CoAxiom`,
543 as `CoAxiom` is the special case when there are no assumptions.
544 -}
545
546 -- | A more explicit representation for `t1 ~ t2`.
547 type TypeEqn = Pair Type
548
549 -- | For now, we work only with nominal equality.
550 data CoAxiomRule = CoAxiomRule
551 { coaxrName :: FastString
552 , coaxrAsmpRoles :: [Role] -- roles of parameter equations
553 , coaxrRole :: Role -- role of resulting equation
554 , coaxrProves :: [TypeEqn] -> Maybe TypeEqn
555 -- ^ coaxrProves returns @Nothing@ when it doesn't like
556 -- the supplied arguments. When this happens in a coercion
557 -- that means that the coercion is ill-formed, and Core Lint
558 -- checks for that.
559 }
560
561 instance Data.Data CoAxiomRule where
562 -- don't traverse?
563 toConstr _ = abstractConstr "CoAxiomRule"
564 gunfold _ _ = error "gunfold"
565 dataTypeOf _ = mkNoRepType "CoAxiomRule"
566
567 instance Uniquable CoAxiomRule where
568 getUnique = getUnique . coaxrName
569
570 instance Eq CoAxiomRule where
571 x == y = coaxrName x == coaxrName y
572
573 instance Ord CoAxiomRule where
574 -- we compare lexically to avoid non-deterministic output when sets of rules
575 -- are printed
576 compare x y = lexicalCompareFS (coaxrName x) (coaxrName y)
577
578 instance Outputable CoAxiomRule where
579 ppr = ppr . coaxrName
580
581
582 -- Type checking of built-in families
583 data BuiltInSynFamily = BuiltInSynFamily
584 { sfMatchFam :: [Type] -> Maybe (CoAxiomRule, [Type], Type)
585 -- Does this reduce on the given arguments?
586 -- If it does, returns (CoAxiomRule, types to instantiate the rule at, rhs type)
587 -- That is: mkAxiomRuleCo coax (zipWith mkReflCo (coaxrAsmpRoles coax) ts)
588 -- :: F tys ~r rhs,
589 -- where the r in the output is coaxrRole of the rule. It is up to the
590 -- caller to ensure that this role is appropriate.
591
592 , sfInteractTop :: [Type] -> Type -> [TypeEqn]
593 -- If given these type arguments and RHS, returns the equalities that
594 -- are guaranteed to hold.
595
596 , sfInteractInert :: [Type] -> Type ->
597 [Type] -> Type -> [TypeEqn]
598 -- If given one set of arguments and result, and another set of arguments
599 -- and result, returns the equalities that are guaranteed to hold.
600 }
601
602 -- Provides default implementations that do nothing.
603 trivialBuiltInFamily :: BuiltInSynFamily
604 trivialBuiltInFamily = BuiltInSynFamily
605 { sfMatchFam = \_ -> Nothing
606 , sfInteractTop = \_ _ -> []
607 , sfInteractInert = \_ _ _ _ -> []
608 }