-data ExprCoFn
- = CoHole -- The identity coercion
-
- | CoCompose ExprCoFn ExprCoFn -- (\a1..an. []) `CoCompose` (\x1..xn. [])
- -- = (\a1..an \x1..xn. [])
-
- | ExprCoFn Coercion -- A cast: [] `cast` co
- -- Guaranteedn not the identity coercion
-
- -- Non-empty list in all of these, so that the identity coercion
- -- is always exactly CoHole, not, say, (CoTyLams [])
- | CoApps [Var] -- [] x1 .. xn; the xi are dicts or coercions
- | CoTyApps [Type] -- [] t1 .. tn
- | CoLams [Id] -- \x1..xn. []; the xi are dicts or coercions
- | CoTyLams [TyVar] -- \a1..an. []
- | CoLet (LHsBinds Id) -- let binds in []
- -- (ould be nicer to be core bindings)
-
-instance Outputable ExprCoFn where
- ppr CoHole = ptext SLIT("<>")
- ppr (ExprCoFn co) = ppr co
- ppr (CoApps ids) = ppr CoHole <+> interppSP ids
- ppr (CoTyApps tys) = ppr CoHole <+> hsep (map pprParendType tys)
- ppr (CoTyLams tvs) = sep [ptext SLIT("/\\") <> hsep (map (pprBndr LambdaBind) tvs),
- ptext SLIT("->") <+> ppr CoHole]
- ppr (CoLams ids) = sep [ptext SLIT("\\") <> hsep (map (pprBndr LambdaBind) ids),
- ptext SLIT("->") <+> ppr CoHole]
- ppr (CoLet binds) = sep [ptext SLIT("let") <+> braces (ppr binds),
- ppr CoHole]
- ppr (CoCompose co1 co2) = sep [ppr co1, ptext SLIT("<.>"), ppr co2]
-
-(<.>) :: ExprCoFn -> ExprCoFn -> ExprCoFn
-CoHole <.> c = c
-c <.> CoHole = c
-c1 <.> c2 = c1 `CoCompose` c2
-
-idCoercion :: ExprCoFn
-idCoercion = CoHole
-
-isIdCoercion :: ExprCoFn -> Bool
-isIdCoercion CoHole = True
-isIdCoercion other = False
+data HsWrapper
+ = WpHole -- The identity coercion
+
+ | WpCompose HsWrapper HsWrapper
+ -- (wrap1 `WpCompse` wrap2)[e] = wrap1[ wrap2[ e ]]
+ --
+ -- Hence (\a. []) `WpCompose` (\b. []) = (\a b. [])
+ -- But ([] a) `WpCompose` ([] b) = ([] b a)
+
+ | WpCast Coercion -- A cast: [] `cast` co
+ -- Guaranteed not the identity coercion
+
+ -- Evidence abstraction and application
+ -- (both dictionaries and coercions)
+ | WpEvLam EvVar -- \d. [] the 'd' is an evidence variable
+ | WpEvApp EvTerm -- [] d the 'd' is evidence for a constraint
+
+ -- Type abstraction and application
+ | WpTyLam TyVar -- \a. [] the 'a' is a type variable (not coercion var)
+ | WpTyApp Type -- [] t the 't' is a type (not coercion)
+
+
+ | WpLet TcEvBinds -- Non-empty (or possibly non-empty) evidence bindings,
+ -- so that the identity coercion is always exactly WpHole
+ deriving (Data, Typeable)
+
+
+data TcEvBinds
+ = TcEvBinds -- Mutable evidence bindings
+ EvBindsVar -- Mutable because they are updated "later"
+ -- when an implication constraint is solved
+
+ | EvBinds -- Immutable after zonking
+ (Bag EvBind)
+
+ deriving( Typeable )
+
+data EvBindsVar = EvBindsVar (IORef EvBindMap) Unique
+ -- The Unique is only for debug printing
+
+-----------------
+type EvBindMap = VarEnv EvBind
+
+emptyEvBindMap :: EvBindMap
+emptyEvBindMap = emptyVarEnv
+
+extendEvBinds :: EvBindMap -> EvVar -> EvTerm -> EvBindMap
+extendEvBinds bs v t = extendVarEnv bs v (EvBind v t)
+
+lookupEvBind :: EvBindMap -> EvVar -> Maybe EvBind
+lookupEvBind = lookupVarEnv
+
+evBindMapBinds :: EvBindMap -> Bag EvBind
+evBindMapBinds = foldVarEnv consBag emptyBag
+
+-----------------
+instance Data TcEvBinds where
+ -- Placeholder; we can't travers into TcEvBinds
+ toConstr _ = abstractConstr "TcEvBinds"
+ gunfold _ _ = error "gunfold"
+ dataTypeOf _ = mkNoRepType "TcEvBinds"
+
+-- All evidence is bound by EvBinds; no side effects
+data EvBind = EvBind EvVar EvTerm
+
+data EvTerm
+ = EvId EvId -- Term-level variable-to-variable bindings
+ -- (no coercion variables! they come via EvCoercion)
+
+ | EvCoercion Coercion -- Coercion bindings
+
+ | EvCast EvVar Coercion -- d |> co
+
+ | EvDFunApp DFunId -- Dictionary instance application
+ [Type] [EvVar]
+
+ | EvSuperClass DictId Int -- n'th superclass. Used for both equalities and
+ -- dictionaries, even though the former have no
+ -- selector Id. We count up from _0_
+
+ deriving( Data, Typeable)
+
+evVarTerm :: EvVar -> EvTerm
+evVarTerm v | isCoVar v = EvCoercion (mkCoVarCoercion v)
+ | otherwise = EvId v
+\end{code}
+
+Note [EvBinds/EvTerm]
+~~~~~~~~~~~~~~~~~~~~~
+How evidence is created and updated. Bindings for dictionaries,
+and coercions and implicit parameters are carried around in TcEvBinds
+which during constraint generation and simplification is always of the
+form (TcEvBinds ref). After constraint simplification is finished it
+will be transformed to t an (EvBinds ev_bag).
+
+Evidence for coercions *SHOULD* be filled in using the TcEvBinds
+However, all EvVars that correspond to *wanted* coercion terms in
+an EvBind must be mutable variables so that they can be readily
+inlined (by zonking) after constraint simplification is finished.
+
+Conclusion: a new wanted coercion variable should be made mutable.
+[Notice though that evidence variables that bind coercion terms
+ from super classes will be "given" and hence rigid]
+
+
+\begin{code}
+emptyTcEvBinds :: TcEvBinds
+emptyTcEvBinds = EvBinds emptyBag
+
+isEmptyTcEvBinds :: TcEvBinds -> Bool
+isEmptyTcEvBinds (EvBinds b) = isEmptyBag b
+isEmptyTcEvBinds (TcEvBinds {}) = panic "isEmptyTcEvBinds"
+
+(<.>) :: HsWrapper -> HsWrapper -> HsWrapper
+WpHole <.> c = c
+c <.> WpHole = c
+c1 <.> c2 = c1 `WpCompose` c2
+
+mkWpTyApps :: [Type] -> HsWrapper
+mkWpTyApps tys = mk_co_app_fn WpTyApp tys
+
+mkWpEvApps :: [EvTerm] -> HsWrapper
+mkWpEvApps args = mk_co_app_fn WpEvApp args
+
+mkWpEvVarApps :: [EvVar] -> HsWrapper
+mkWpEvVarApps vs = mkWpEvApps (map evVarTerm vs)
+
+mkWpTyLams :: [TyVar] -> HsWrapper
+mkWpTyLams ids = mk_co_lam_fn WpTyLam ids
+
+mkWpLams :: [Var] -> HsWrapper
+mkWpLams ids = mk_co_lam_fn WpEvLam ids
+
+mkWpLet :: TcEvBinds -> HsWrapper
+-- This no-op is a quite a common case
+mkWpLet (EvBinds b) | isEmptyBag b = WpHole
+mkWpLet ev_binds = WpLet ev_binds
+
+mk_co_lam_fn :: (a -> HsWrapper) -> [a] -> HsWrapper
+mk_co_lam_fn f as = foldr (\x wrap -> f x `WpCompose` wrap) WpHole as
+
+mk_co_app_fn :: (a -> HsWrapper) -> [a] -> HsWrapper
+-- For applications, the *first* argument must
+-- come *last* in the composition sequence
+mk_co_app_fn f as = foldr (\x wrap -> wrap `WpCompose` f x) WpHole as
+
+idHsWrapper :: HsWrapper
+idHsWrapper = WpHole
+
+isIdHsWrapper :: HsWrapper -> Bool
+isIdHsWrapper WpHole = True
+isIdHsWrapper _ = False