-Here is the overall algorithm.
-Assume that we have an instance declaration
-
- instance c => k (t tvs) where b
-
-\begin{enumerate}
-\item
-$LIE_c$ is the LIE for the context of class $c$
-\item
-$betas_bar$ is the free variables in the class method type, excluding the
- class variable
-\item
-$LIE_cop$ is the LIE constraining a particular class method
-\item
-$tau_cop$ is the tau type of a class method
-\item
-$LIE_i$ is the LIE for the context of instance $i$
-\item
-$X$ is the instance constructor tycon
-\item
-$gammas_bar$ is the set of type variables of the instance
-\item
-$LIE_iop$ is the LIE for a particular class method instance
-\item
-$tau_iop$ is the tau type for this instance of a class method
-\item
-$alpha$ is the class variable
-\item
-$LIE_cop' = LIE_cop [X gammas_bar / alpha, fresh betas_bar]$
-\item
-$tau_cop' = tau_cop [X gammas_bar / alpha, fresh betas_bar]$
-\end{enumerate}
-
-ToDo: Update the list above with names actually in the code.
-
-\begin{enumerate}
-\item
-First, make the LIEs for the class and instance contexts, which means
-instantiate $thetaC [X inst_tyvars / alpha ]$, yielding LIElistC' and LIEC',
-and make LIElistI and LIEI.
-\item
-Then process each method in turn.
-\item
-order the instance methods according to the ordering of the class methods
-\item
-express LIEC' in terms of LIEI, yielding $dbinds_super$ or an error
-\item
-Create final dictionary function from bindings generated already
-\begin{pseudocode}
-df = lambda inst_tyvars
- lambda LIEI
- let Bop1
- Bop2
- ...
- Bopn
- and dbinds_super
- in <op1,op2,...,opn,sd1,...,sdm>
-\end{pseudocode}
-Here, Bop1 \ldots Bopn bind the methods op1 \ldots opn,
-and $dbinds_super$ bind the superclass dictionaries sd1 \ldots sdm.
-\end{enumerate}
+
+Note [How instance declarations are translated]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Here is how we translation instance declarations into Core
+
+Running example:
+ class C a where
+ op1, op2 :: Ix b => a -> b -> b
+ op2 = <dm-rhs>
+
+ instance C a => C [a]
+ {-# INLINE [2] op1 #-}
+ op1 = <rhs>
+===>
+ -- Method selectors
+ op1,op2 :: forall a. C a => forall b. Ix b => a -> b -> b
+ op1 = ...
+ op2 = ...
+
+ -- Default methods get the 'self' dictionary as argument
+ -- so they can call other methods at the same type
+ -- Default methods get the same type as their method selector
+ $dmop2 :: forall a. C a => forall b. Ix b => a -> b -> b
+ $dmop2 = /\a. \(d:C a). /\b. \(d2: Ix b). <dm-rhs>
+ -- NB: type variables 'a' and 'b' are *both* in scope in <dm-rhs>
+ -- Note [Tricky type variable scoping]
+
+ -- A top-level definition for each instance method
+ -- Here op1_i, op2_i are the "instance method Ids"
+ -- The INLINE pragma comes from the user pragma
+ {-# INLINE [2] op1_i #-} -- From the instance decl bindings
+ op1_i, op2_i :: forall a. C a => forall b. Ix b => [a] -> b -> b
+ op1_i = /\a. \(d:C a).
+ let this :: C [a]
+ this = df_i a d
+ -- Note [Subtle interaction of recursion and overlap]
+
+ local_op1 :: forall b. Ix b => [a] -> b -> b
+ local_op1 = <rhs>
+ -- Source code; run the type checker on this
+ -- NB: Type variable 'a' (but not 'b') is in scope in <rhs>
+ -- Note [Tricky type variable scoping]
+
+ in local_op1 a d
+
+ op2_i = /\a \d:C a. $dmop2 [a] (df_i a d)
+
+ -- The dictionary function itself
+ {-# NOINLINE CONLIKE df_i #-} -- Never inline dictionary functions
+ df_i :: forall a. C a -> C [a]
+ df_i = /\a. \d:C a. MkC (op1_i a d) (op2_i a d)
+ -- But see Note [Default methods in instances]
+ -- We can't apply the type checker to the default-method call
+
+ -- Use a RULE to short-circuit applications of the class ops
+ {-# RULE "op1@C[a]" forall a, d:C a.
+ op1 [a] (df_i d) = op1_i a d #-}
+
+Note [Instances and loop breakers]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+* Note that df_i may be mutually recursive with both op1_i and op2_i.
+ It's crucial that df_i is not chosen as the loop breaker, even
+ though op1_i has a (user-specified) INLINE pragma.
+
+* Instead the idea is to inline df_i into op1_i, which may then select
+ methods from the MkC record, and thereby break the recursion with
+ df_i, leaving a *self*-recurisve op1_i. (If op1_i doesn't call op at
+ the same type, it won't mention df_i, so there won't be recursion in
+ the first place.)
+
+* If op1_i is marked INLINE by the user there's a danger that we won't
+ inline df_i in it, and that in turn means that (since it'll be a
+ loop-breaker because df_i isn't), op1_i will ironically never be
+ inlined. But this is OK: the recursion breaking happens by way of
+ a RULE (the magic ClassOp rule above), and RULES work inside InlineRule
+ unfoldings. See Note [RULEs enabled in SimplGently] in SimplUtils
+
+Note [ClassOp/DFun selection]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+One thing we see a lot is stuff like
+ op2 (df d1 d2)
+where 'op2' is a ClassOp and 'df' is DFun. Now, we could inline *both*
+'op2' and 'df' to get
+ case (MkD ($cop1 d1 d2) ($cop2 d1 d2) ... of
+ MkD _ op2 _ _ _ -> op2
+And that will reduce to ($cop2 d1 d2) which is what we wanted.
+
+But it's tricky to make this work in practice, because it requires us to
+inline both 'op2' and 'df'. But neither is keen to inline without having
+seen the other's result; and it's very easy to get code bloat (from the
+big intermediate) if you inline a bit too much.
+
+Instead we use a cunning trick.
+ * We arrange that 'df' and 'op2' NEVER inline.
+
+ * We arrange that 'df' is ALWAYS defined in the sylised form
+ df d1 d2 = MkD ($cop1 d1 d2) ($cop2 d1 d2) ...
+
+ * We give 'df' a magical unfolding (DFunUnfolding [$cop1, $cop2, ..])
+ that lists its methods.
+
+ * We make CoreUnfold.exprIsConApp_maybe spot a DFunUnfolding and return
+ a suitable constructor application -- inlining df "on the fly" as it
+ were.
+
+ * We give the ClassOp 'op2' a BuiltinRule that extracts the right piece
+ iff its argument satisfies exprIsConApp_maybe. This is done in
+ MkId mkDictSelId
+
+ * We make 'df' CONLIKE, so that shared uses stil match; eg
+ let d = df d1 d2
+ in ...(op2 d)...(op1 d)...
+
+Note [Single-method classes]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+If the class has just one method (or, more accurately, just one element
+of {superclasses + methods}), then we still use the *same* strategy
+
+ class C a where op :: a -> a
+ instance C a => C [a] where op = <blah>
+
+We translate the class decl into a newtype, which just gives
+a top-level axiom:
+
+ axiom Co:C a :: C a ~ (a->a)
+
+ op :: forall a. C a -> (a -> a)
+ op a d = d |> (Co:C a)
+
+ MkC :: forall a. (a->a) -> C a
+ MkC = /\a.\op. op |> (sym Co:C a)
+
+ df :: forall a. C a => C [a]
+ {-# NOINLINE df DFun[ $cop_list ] #-}
+ df = /\a. \d. MkC ($cop_list a d)
+
+ $cop_list :: forall a. C a => [a] -> [a]
+ $cop_list = <blah>
+
+The "constructor" MkC expands to a cast, as does the class-op selector.
+The RULE works just like for multi-field dictionaries:
+
+ * (df a d) returns (Just (MkC,..,[$cop_list a d]))
+ to exprIsConApp_Maybe
+
+ * The RULE for op picks the right result
+
+This is a bit of a hack, because (df a d) isn't *really* a constructor
+application. But it works just fine in this case, exprIsConApp_maybe
+is otherwise used only when we hit a case expression which will have
+a real data constructor in it.
+
+The biggest reason for doing it this way, apart from uniformity, is
+that we want to be very careful when we have
+ instance C a => C [a] where
+ {-# INLINE op #-}
+ op = ...
+then we'll get an INLINE pragma on $cop_list but it's important that
+$cop_list only inlines when it's applied to *two* arguments (the
+dictionary and the list argument
+
+The danger is that we'll get something like
+ op_list :: C a => [a] -> [a]
+ op_list = /\a.\d. $cop_list a d
+and then we'll eta expand, and then we'll inline TOO EARLY. This happened in
+Trac #3772 and I spent far too long fiddling around trying to fix it.
+Look at the test for Trac #3772.
+
+ (Note: re-reading the above, I can't see how using the
+ uniform story solves the problem.)
+
+Note [Subtle interaction of recursion and overlap]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Consider this
+ class C a where { op1,op2 :: a -> a }
+ instance C a => C [a] where
+ op1 x = op2 x ++ op2 x
+ op2 x = ...
+ instance C [Int] where
+ ...
+
+When type-checking the C [a] instance, we need a C [a] dictionary (for
+the call of op2). If we look up in the instance environment, we find
+an overlap. And in *general* the right thing is to complain (see Note
+[Overlapping instances] in InstEnv). But in *this* case it's wrong to
+complain, because we just want to delegate to the op2 of this same
+instance.
+
+Why is this justified? Because we generate a (C [a]) constraint in
+a context in which 'a' cannot be instantiated to anything that matches
+other overlapping instances, or else we would not be excecuting this
+version of op1 in the first place.
+
+It might even be a bit disguised:
+
+ nullFail :: C [a] => [a] -> [a]
+ nullFail x = op2 x ++ op2 x
+
+ instance C a => C [a] where
+ op1 x = nullFail x
+
+Precisely this is used in package 'regex-base', module Context.hs.
+See the overlapping instances for RegexContext, and the fact that they
+call 'nullFail' just like the example above. The DoCon package also
+does the same thing; it shows up in module Fraction.hs
+
+Conclusion: when typechecking the methods in a C [a] instance, we want
+to have C [a] available. That is why we have the strange local
+definition for 'this' in the definition of op1_i in the example above.
+We can typecheck the defintion of local_op1, and when doing tcSimplifyCheck
+we supply 'this' as a given dictionary. Only needed, though, if there
+are some type variables involved; otherwise there can be no overlap and
+none of this arises.
+
+Note [Tricky type variable scoping]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+In our example
+ class C a where
+ op1, op2 :: Ix b => a -> b -> b
+ op2 = <dm-rhs>
+
+ instance C a => C [a]
+ {-# INLINE [2] op1 #-}
+ op1 = <rhs>
+
+note that 'a' and 'b' are *both* in scope in <dm-rhs>, but only 'a' is
+in scope in <rhs>. In particular, we must make sure that 'b' is in
+scope when typechecking <dm-rhs>. This is achieved by subFunTys,
+which brings appropriate tyvars into scope. This happens for both
+<dm-rhs> and for <rhs>, but that doesn't matter: the *renamer* will have
+complained if 'b' is mentioned in <rhs>.
+
projects / ghc-hetmet.git / blobdiff