Commit 2e6dcdf7 authored by Simon Peyton Jones's avatar Simon Peyton Jones

Allow full constraint solving under a for-all (Trac #5595)

The main idea is that when we unify
    forall a. t1  ~  forall a. t2
we get constraints from unifying t1~t2 that mention a.
We are producing a coercion witnessing the equivalence of
the for-alls, and inside *that* coercion we need bindings
for the solved constraints arising from t1~t2.

We didn't have way to do this before.  The big change is
that here's a new type TcEvidence.TcCoercion, which is
much like Coercion.Coercion except that there's a slot
for TcEvBinds in it.

This has a wave of follow-on changes. Not deep but broad.

* New module TcEvidence, which now contains the HsWrapper
  TcEvBinds, EvTerm etc types that used to be in HsBinds

* The typechecker works exclusively in terms of TcCoercion.

* The desugarer converts TcCoercion to Coercion

* The main payload is in TcUnify.unifySigmaTy. This is the
  function that had a gross hack before, but is now beautiful.

* LCoercion is gone!  Hooray.

Many many fiddly changes in conssequence.  But it's nice.
parent 22b317b1
......@@ -120,7 +120,7 @@ deSugar hsc_env
else return (binds, hpcInfo, emptyModBreaks)
initDs hsc_env mod rdr_env type_env $ do
do { ds_ev_binds <- dsEvBinds ev_binds
do { let ds_ev_binds = dsEvBinds ev_binds
; core_prs <- dsTopLHsBinds binds_cvr
; (spec_prs, spec_rules) <- dsImpSpecs imp_specs
; (ds_fords, foreign_prs) <- dsForeigns fords
......
......@@ -32,6 +32,7 @@ import TcHsSyn
import {-# SOURCE #-} DsExpr ( dsExpr, dsLExpr, dsLocalBinds )
import TcType
import TcEvidence
import Type
import CoreSyn
import CoreFVs
......
This diff is collapsed.
......@@ -31,8 +31,8 @@ import HsSyn
-- NB: The desugarer, which straddles the source and Core worlds, sometimes
-- needs to see source types
import TcType
import TcEvidence
import Type
import Coercion
import CoreSyn
import CoreUtils
import CoreFVs
......@@ -79,8 +79,7 @@ dsValBinds (ValBindsIn _ _) _ = panic "dsValBinds ValBindsIn"
-------------------------
dsIPBinds :: HsIPBinds Id -> CoreExpr -> DsM CoreExpr
dsIPBinds (IPBinds ip_binds ev_binds) body
= do { ds_ev_binds <- dsTcEvBinds ev_binds
; let inner = mkCoreLets ds_ev_binds body
= do { let inner = mkCoreLets (dsTcEvBinds ev_binds) body
-- The dict bindings may not be in
-- dependency order; hence Rec
; foldrM ds_ip_bind inner ip_binds }
......@@ -128,12 +127,11 @@ dsStrictBind (AbsBinds { abs_tvs = [], abs_ev_vars = []
, abs_exports = exports
, abs_ev_binds = ev_binds
, abs_binds = binds }) body
= do { ds_ev_binds <- dsTcEvBinds ev_binds
; let body1 = foldr bind_export body exports
= do { let body1 = foldr bind_export body exports
bind_export export b = bindNonRec (abe_poly export) (Var (abe_mono export)) b
; body2 <- foldlBagM (\body bind -> dsStrictBind (unLoc bind) body)
body1 binds
; return (mkCoreLets ds_ev_binds body2) }
; return (mkCoreLets (dsTcEvBinds ev_binds) body2) }
dsStrictBind (FunBind { fun_id = L _ fun, fun_matches = matches, fun_co_fn = co_fn
, fun_tick = tick, fun_infix = inf }) body
......@@ -217,11 +215,11 @@ dsExpr (HsLit lit) = dsLit lit
dsExpr (HsOverLit lit) = dsOverLit lit
dsExpr (HsWrap co_fn e)
= do { co_fn' <- dsHsWrapper co_fn
; e' <- dsExpr e
= do { e' <- dsExpr e
; let wrapped_e = dsHsWrapper co_fn e'
; warn_id <- woptDs Opt_WarnIdentities
; when warn_id $ warnAboutIdentities e' co_fn'
; return (co_fn' e') }
; when warn_id $ warnAboutIdentities e' wrapped_e
; return wrapped_e }
dsExpr (NegApp expr neg_expr)
= App <$> dsExpr neg_expr <*> dsLExpr expr
......@@ -545,12 +543,12 @@ dsExpr expr@(RecordUpd record_expr (HsRecFields { rec_flds = fields })
-- Tediously wrap the application in a cast
-- Note [Update for GADTs]
wrap_co = mkTyConAppCo tycon
wrap_co = mkTcTyConAppCo tycon
[ lookup tv ty | (tv,ty) <- univ_tvs `zip` out_inst_tys ]
lookup univ_tv ty = case lookupVarEnv wrap_subst univ_tv of
Just co' -> co'
Nothing -> mkReflCo ty
wrap_subst = mkVarEnv [ (tv, mkSymCo (mkEqVarLCo eq_var))
Nothing -> mkTcReflCo ty
wrap_subst = mkVarEnv [ (tv, mkTcSymCo (mkTcCoVarCo eq_var))
| ((tv,_),eq_var) <- eq_spec `zip` eqs_vars ]
pat = noLoc $ ConPatOut { pat_con = noLoc con, pat_tvs = ex_tvs
......@@ -805,14 +803,15 @@ mk_fail_msg pat = "Pattern match failure in do expression at " ++
%* *
%************************************************************************
Warn about functions that convert between one type and another
when the to- and from- types are the same. Then it's probably
(albeit not definitely) the identity
Warn about functions like toInteger, fromIntegral, that convert
between one type and another when the to- and from- types are the
same. Then it's probably (albeit not definitely) the identity
\begin{code}
warnAboutIdentities :: CoreExpr -> (CoreExpr -> CoreExpr) -> DsM ()
warnAboutIdentities (Var v) co_fn
warnAboutIdentities :: CoreExpr -> CoreExpr -> DsM ()
warnAboutIdentities (Var v) wrapped_fun
| idName v `elem` conversionNames
, let fun_ty = exprType (co_fn (Var v))
, let fun_ty = exprType wrapped_fun
, Just (arg_ty, res_ty) <- splitFunTy_maybe fun_ty
, arg_ty `eqType` res_ty -- So we are converting ty -> ty
= warnDs (vcat [ ptext (sLit "Call of") <+> ppr v <+> dcolon <+> ppr fun_ty
......
......@@ -19,6 +19,7 @@ import TcHsSyn
import CoreSyn
import MkCore
import TcEvidence
import DsMonad -- the monadery used in the desugarer
import DsUtils
......
......@@ -22,6 +22,7 @@ import {-#SOURCE#-} DsExpr (dsLExpr)
import DynFlags
import HsSyn
import TcHsSyn
import TcEvidence
import Check
import CoreSyn
import Literal
......@@ -36,7 +37,6 @@ import DataCon
import MatchCon
import MatchLit
import Type
import Coercion
import TysWiredIn
import ListSetOps
import SrcLoc
......@@ -356,8 +356,7 @@ matchCoercion (var:vars) ty (eqns@(eqn1:_))
; var' <- newUniqueId var (hsPatType pat)
; match_result <- match (var':vars) ty $
map (decomposeFirstPat getCoPat) eqns
; co' <- dsHsWrapper co
; let rhs' = co' (Var var)
; let rhs' = dsHsWrapper co (Var var)
; return (mkCoLetMatchResult (NonRec var' rhs') match_result) }
matchCoercion _ _ _ = panic "matchCoercion"
......@@ -919,7 +918,7 @@ viewLExprEq (e1,_) (e2,_) = lexp e1 e2
-- equating different ways of writing a coercion)
wrap WpHole WpHole = True
wrap (WpCompose w1 w2) (WpCompose w1' w2') = wrap w1 w1' && wrap w2 w2'
wrap (WpCast co) (WpCast co') = co `coreEqCoercion` co'
wrap (WpCast co) (WpCast co') = co `eq_co` co'
wrap (WpEvApp et1) (WpEvApp et2) = et1 `ev_term` et2
wrap (WpTyApp t) (WpTyApp t') = eqType t t'
-- Enhancement: could implement equality for more wrappers
......@@ -928,8 +927,8 @@ viewLExprEq (e1,_) (e2,_) = lexp e1 e2
---------
ev_term :: EvTerm -> EvTerm -> Bool
ev_term (EvId a) (EvId b) = a==b
ev_term (EvCoercionBox a) (EvCoercionBox b) = coreEqCoercion a b
ev_term (EvId a) (EvId b) = a==b
ev_term (EvCoercion a) (EvCoercion b) = a `eq_co` b
ev_term _ _ = False
---------
......@@ -939,6 +938,15 @@ viewLExprEq (e1,_) (e2,_) = lexp e1 e2
eq_list _ (_:_) [] = False
eq_list eq (x:xs) (y:ys) = eq x y && eq_list eq xs ys
---------
eq_co :: TcCoercion -> TcCoercion -> Bool
-- Just some simple cases
eq_co (TcRefl t1) (TcRefl t2) = eqType t1 t2
eq_co (TcCoVarCo v1) (TcCoVarCo v2) = v1==v2
eq_co (TcSymCo co1) (TcSymCo co2) = co1 `eq_co` co2
eq_co (TcTyConAppCo tc1 cos1) (TcTyConAppCo tc2 cos2) = tc1==tc2 && eq_list eq_co cos1 cos2
eq_co _ _ = False
patGroup :: Pat Id -> PatGroup
patGroup (WildPat {}) = PgAny
patGroup (BangPat {}) = PgBang
......
......@@ -131,19 +131,18 @@ matchOneCon vars ty (eqn1 : eqns) -- All eqns for a single constructor
match_group :: [Id] -> [(ConArgPats, EquationInfo)] -> DsM MatchResult
-- All members of the group have compatible ConArgPats
match_group arg_vars arg_eqn_prs
= do { (wraps, eqns') <- mapAndUnzipM shift arg_eqn_prs
; let group_arg_vars = select_arg_vars arg_vars arg_eqn_prs
= do { let (wraps, eqns') = unzip (map shift arg_eqn_prs)
group_arg_vars = select_arg_vars arg_vars arg_eqn_prs
; match_result <- match (group_arg_vars ++ vars) ty eqns'
; return (adjustMatchResult (foldr1 (.) wraps) match_result) }
shift (_, eqn@(EqnInfo { eqn_pats = ConPatOut{ pat_tvs = tvs, pat_dicts = ds,
pat_binds = bind, pat_args = args
} : pats }))
= do { ds_ev_binds <- dsTcEvBinds bind
; return (wrapBinds (tvs `zip` tvs1)
. wrapBinds (ds `zip` dicts1)
. mkCoreLets ds_ev_binds,
eqn { eqn_pats = conArgPats arg_tys args ++ pats }) }
= ( wrapBinds (tvs `zip` tvs1)
. wrapBinds (ds `zip` dicts1)
. mkCoreLets (dsTcEvBinds bind)
, eqn { eqn_pats = conArgPats arg_tys args ++ pats })
shift (_, (EqnInfo { eqn_pats = ps })) = pprPanic "matchOneCon/shift" (ppr ps)
-- Choose the right arg_vars in the right order for this group
......
......@@ -411,6 +411,7 @@ Library
TcTyClsDecls
TcTyDecls
TcType
TcEvidence
TcUnify
TcInteract
TcCanonical
......
......@@ -27,7 +27,7 @@ import HsLit
import HsTypes
import PprCore ()
import CoreSyn
import Coercion
import TcEvidence
import Type
import Name
import NameSet
......@@ -35,15 +35,11 @@ import BasicTypes
import Outputable
import SrcLoc
import Util
import VarEnv
import Var
import Bag
import Unique
import FastString
import Data.IORef( IORef )
import Data.Data hiding ( Fixity )
import Data.List ( intersect )
\end{code}
......@@ -438,227 +434,6 @@ instance (OutputableBndr id) => Outputable (IPBind id) where
\end{code}
%************************************************************************
%* *
\subsection{Coercion functions}
%* *
%************************************************************************
\begin{code}
data HsWrapper
= WpHole -- The identity coercion
| WpCompose HsWrapper HsWrapper
-- (wrap1 `WpCompose` wrap2)[e] = wrap1[ wrap2[ e ]]
--
-- Hence (\a. []) `WpCompose` (\b. []) = (\a b. [])
-- But ([] a) `WpCompose` ([] b) = ([] b a)
| WpCast LCoercion -- 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
-- Kind and Type abstraction and application
| WpTyLam TyVar -- \a. [] the 'a' is a type/kind variable (not coercion var)
| WpTyApp KindOrType -- [] 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
-----------------
newtype EvBindMap = EvBindMap { ev_bind_varenv :: VarEnv EvBind } -- Map from evidence variables to evidence terms
emptyEvBindMap :: EvBindMap
emptyEvBindMap = EvBindMap { ev_bind_varenv = emptyVarEnv }
extendEvBinds :: EvBindMap -> EvVar -> EvTerm -> EvBindMap
extendEvBinds bs v t
= EvBindMap { ev_bind_varenv = extendVarEnv (ev_bind_varenv bs) v (EvBind v t) }
lookupEvBind :: EvBindMap -> EvVar -> Maybe EvBind
lookupEvBind bs = lookupVarEnv (ev_bind_varenv bs)
evBindMapBinds :: EvBindMap -> Bag EvBind
evBindMapBinds bs
= foldVarEnv consBag emptyBag (ev_bind_varenv bs)
-----------------
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 EvCoercionBox)
| EvCoercionBox LCoercion -- (Boxed) coercion bindings
| EvCast EvVar LCoercion -- d |> co
| EvDFunApp DFunId -- Dictionary instance application
[Type] [EvVar]
| EvTupleSel EvId Int -- n'th component of the tuple
| EvTupleMk [EvId] -- tuple built from this stuff
| 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)
\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}
mkEvCast :: EvVar -> LCoercion -> EvTerm
mkEvCast ev lco
| isReflCo lco = EvId ev
| otherwise = EvCast ev lco
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 EvId 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 <.> 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 <.> f x) WpHole as
idHsWrapper :: HsWrapper
idHsWrapper = WpHole
isIdHsWrapper :: HsWrapper -> Bool
isIdHsWrapper WpHole = True
isIdHsWrapper _ = False
\end{code}
Pretty printing
\begin{code}
instance Outputable HsWrapper where
ppr co_fn = pprHsWrapper (ptext (sLit "<>")) co_fn
pprHsWrapper :: SDoc -> HsWrapper -> SDoc
-- In debug mode, print the wrapper
-- otherwise just print what's inside
pprHsWrapper doc wrap
= getPprStyle (\ s -> if debugStyle s then (help (add_parens doc) wrap False) else doc)
where
help :: (Bool -> SDoc) -> HsWrapper -> Bool -> SDoc
-- True <=> appears in function application position
-- False <=> appears as body of let or lambda
help it WpHole = it
help it (WpCompose f1 f2) = help (help it f2) f1
help it (WpCast co) = add_parens $ sep [it False, nest 2 (ptext (sLit "|>")
<+> pprParendCo co)]
help it (WpEvApp id) = no_parens $ sep [it True, nest 2 (ppr id)]
help it (WpTyApp ty) = no_parens $ sep [it True, ptext (sLit "@") <+> pprParendType ty]
help it (WpEvLam id) = add_parens $ sep [ ptext (sLit "\\") <> pp_bndr id, it False]
help it (WpTyLam tv) = add_parens $ sep [ptext (sLit "/\\") <> pp_bndr tv, it False]
help it (WpLet binds) = add_parens $ sep [ptext (sLit "let") <+> braces (ppr binds), it False]
pp_bndr v = pprBndr LambdaBind v <> dot
add_parens, no_parens :: SDoc -> Bool -> SDoc
add_parens d True = parens d
add_parens d False = d
no_parens d _ = d
instance Outputable TcEvBinds where
ppr (TcEvBinds v) = ppr v
ppr (EvBinds bs) = ptext (sLit "EvBinds") <> braces (ppr bs)
instance Outputable EvBindsVar where
ppr (EvBindsVar _ u) = ptext (sLit "EvBindsVar") <> angleBrackets (ppr u)
instance Outputable EvBind where
ppr (EvBind v e) = ppr v <+> equals <+> ppr e
-- We cheat a bit and pretend EqVars are CoVars for the purposes of pretty printing
instance Outputable EvTerm where
ppr (EvId v) = ppr v
ppr (EvCast v co) = ppr v <+> (ptext (sLit "`cast`")) <+> pprParendCo co
ppr (EvCoercionBox co) = ptext (sLit "CO") <+> ppr co
ppr (EvTupleSel v n) = ptext (sLit "tupsel") <> parens (ppr (v,n))
ppr (EvTupleMk vs) = ptext (sLit "tupmk") <+> ppr vs
ppr (EvSuperClass d n) = ptext (sLit "sc") <> parens (ppr (d,n))
ppr (EvDFunApp df tys ts) = ppr df <+> sep [ char '@' <> ppr tys, ppr ts ]
\end{code}
%************************************************************************
%* *
\subsection{@Sig@: type signatures and value-modifying user pragmas}
......
......@@ -25,6 +25,7 @@ import HsTypes
import HsBinds
-- others:
import TcEvidence
import CoreSyn
import Var
import Name
......
......@@ -29,6 +29,7 @@ import {-# SOURCE #-} HsExpr (SyntaxExpr, LHsExpr, pprLExpr)
import HsBinds
import HsLit
import HsTypes
import TcEvidence
import BasicTypes
-- others:
import PprCore ( {- instance OutputableBndr TyVar -} )
......
......@@ -82,9 +82,9 @@ import HsPat
import HsTypes
import HsLit
import TcEvidence
import RdrName
import Var
import Coercion
import TypeRep
import DataCon
import Name
......@@ -172,37 +172,6 @@ mkParPat :: LPat name -> LPat name
mkParPat lp@(L loc p) | hsPatNeedsParens p = L loc (ParPat lp)
| otherwise = lp
--------- HsWrappers: type args, dict args, casts ---------
mkLHsWrap :: HsWrapper -> LHsExpr id -> LHsExpr id
mkLHsWrap co_fn (L loc e) = L loc (mkHsWrap co_fn e)
mkHsWrap :: HsWrapper -> HsExpr id -> HsExpr id
mkHsWrap co_fn e | isIdHsWrapper co_fn = e
| otherwise = HsWrap co_fn e
mkHsWrapCo :: LCoercion -> HsExpr id -> HsExpr id
mkHsWrapCo (Refl _) e = e
mkHsWrapCo co e = mkHsWrap (WpCast co) e
mkLHsWrapCo :: LCoercion -> LHsExpr id -> LHsExpr id
mkLHsWrapCo (Refl _) e = e
mkLHsWrapCo co (L loc e) = L loc (mkHsWrap (WpCast co) e)
coToHsWrapper :: LCoercion -> HsWrapper
coToHsWrapper (Refl _) = idHsWrapper
coToHsWrapper co = WpCast co
mkHsWrapPat :: HsWrapper -> Pat id -> Type -> Pat id
mkHsWrapPat co_fn p ty | isIdHsWrapper co_fn = p
| otherwise = CoPat co_fn p ty
mkHsWrapPatCo :: LCoercion -> Pat id -> Type -> Pat id
mkHsWrapPatCo (Refl _) pat _ = pat
mkHsWrapPatCo co pat ty = CoPat (WpCast co) pat ty
mkHsDictLet :: TcEvBinds -> LHsExpr Id -> LHsExpr Id
mkHsDictLet ev_binds expr = mkLHsWrap (mkWpLet ev_binds) expr
-------------------------------
-- These are the bits of syntax that contain rebindable names
......@@ -404,6 +373,39 @@ missingTupArg :: HsTupArg a
missingTupArg = Missing placeHolderType
\end{code}
\begin{code}
--------- HsWrappers: type args, dict args, casts ---------
mkLHsWrap :: HsWrapper -> LHsExpr id -> LHsExpr id
mkLHsWrap co_fn (L loc e) = L loc (mkHsWrap co_fn e)
mkHsWrap :: HsWrapper -> HsExpr id -> HsExpr id
mkHsWrap co_fn e | isIdHsWrapper co_fn = e
| otherwise = HsWrap co_fn e
mkHsWrapCo :: TcCoercion -> HsExpr id -> HsExpr id
mkHsWrapCo co e | isTcReflCo co = e
| otherwise = mkHsWrap (WpCast co) e
mkLHsWrapCo :: TcCoercion -> LHsExpr id -> LHsExpr id
mkLHsWrapCo co (L loc e) | isTcReflCo co = L loc e
| otherwise = L loc (mkHsWrap (WpCast co) e)
coToHsWrapper :: TcCoercion -> HsWrapper
coToHsWrapper co | isTcReflCo co = idHsWrapper
| otherwise = WpCast co
mkHsWrapPat :: HsWrapper -> Pat id -> Type -> Pat id
mkHsWrapPat co_fn p ty | isIdHsWrapper co_fn = p
| otherwise = CoPat co_fn p ty
mkHsWrapPatCo :: TcCoercion -> Pat id -> Type -> Pat id
mkHsWrapPatCo co pat ty | isTcReflCo co = pat
| otherwise = CoPat (WpCast co) pat ty
mkHsDictLet :: TcEvBinds -> LHsExpr Id -> LHsExpr Id
mkHsDictLet ev_binds expr = mkLHsWrap (mkWpLet ev_binds) expr
\end{code}
l
%************************************************************************
%* *
Bindings; with a location at the top
......
......@@ -262,7 +262,7 @@ import Packages
import NameSet
import RdrName
import qualified HsSyn -- hack as we want to reexport the whole module
import HsSyn hiding ((<.>))
import HsSyn
import Type hiding( typeKind )
import Kind ( synTyConResKind )
import TcType hiding( typeKind )
......
......@@ -38,7 +38,7 @@ import Module
import HscTypes
import ErrUtils
import DynFlags
import HsSyn hiding ((<.>))
import HsSyn
import Finder
import HeaderInfo
import TcIface ( typecheckIface )
......
......@@ -32,6 +32,7 @@ import RdrHsSyn
import HscTypes ( IsBootInterface, WarningTxt(..) )
import Lexer
import RdrName
import TcEvidence ( emptyTcEvBinds )
import TysPrim ( liftedTypeKindTyConName, eqPrimTyCon )
import TysWiredIn ( unitTyCon, unitDataCon, tupleTyCon, tupleCon, nilDataCon,
unboxedSingletonTyCon, unboxedSingletonDataCon,
......
......@@ -54,6 +54,7 @@ import RdrName ( RdrName, isRdrTyVar, isRdrTc, mkUnqual, rdrNameOcc,
import Name ( Name )
import BasicTypes ( maxPrecedence, Activation(..), RuleMatchInfo,
InlinePragma(..), InlineSpec(..) )
import TcEvidence ( idHsWrapper )
import Lexer
import TysWiredIn ( unitTyCon )
import ForeignCall
......
......@@ -35,6 +35,7 @@ import {-# SOURCE #-} RnExpr( rnLExpr, rnStmts )
import HsSyn
import RnHsSyn
import TcRnMonad
import TcEvidence ( emptyTcEvBinds )
import RnTypes ( rnIPName, rnHsSigType, rnLHsType, checkPrecMatch )
import RnPat
import RnEnv
......
......@@ -48,6 +48,7 @@ import HsSyn
import TcHsSyn
import TcRnMonad
import TcEnv
import TcEvidence
import InstEnv
import FunDeps
import TcMType
......@@ -223,7 +224,7 @@ instCallConstraints origin (pred : preds)
= do { traceTc "instCallConstraints" $ ppr (mkEqPred (ty1, ty2))
; co <- unifyType ty1 ty2
; co_fn <- instCallConstraints origin preds
; return (co_fn <.> WpEvApp (EvCoercionBox co)) }
; return (co_fn <.> WpEvApp (EvCoercion co)) }
| otherwise
= do { ev_var <- emitWanted origin pred
......
......@@ -25,7 +25,7 @@ import TcPat
import TcUnify
import TcRnMonad
import TcEnv
import Coercion
import TcEvidence
import Id( mkLocalId )
import Inst
import Name
......@@ -50,7 +50,7 @@ import Control.Monad
\begin{code}
tcProc :: InPat Name -> LHsCmdTop Name -- proc pat -> expr
-> TcRhoType -- Expected type of whole proc expression
-> TcM (OutPat TcId, LHsCmdTop TcId, LCoercion)
-> TcM (OutPat TcId, LHsCmdTop TcId, TcCoercion)
tcProc pat cmd exp_ty
= newArrowScope $
......@@ -59,7 +59,7 @@ tcProc pat cmd exp_ty
; let cmd_env = CmdEnv { cmd_arr = arr_ty }
; (pat', cmd') <- tcPat ProcExpr pat arg_ty $
tcCmdTop cmd_env cmd [] res_ty
; let res_co = mkTransCo co (mkAppCo co1 (mkReflCo res_ty))
; let res_co = mkTcTransCo co (mkTcAppCo co1 (mkTcReflCo res_ty))
; return (pat', cmd', res_co) }
\end{code}
......
......@@ -21,6 +21,7 @@ import TcRnMonad
import TcEnv
import TcUnify
import TcSimplify
import TcEvidence
import TcHsType
import TcPat
import TcMType
......
This diff is collapsed.
......@@ -24,6 +24,7 @@ module TcClassDcl ( tcClassSigs, tcClassDecl2,
import HsSyn
import TcEnv
import TcPat( addInlinePrags )
import TcEvidence( idHsWrapper )
import TcBinds
import TcUnify
import TcHsType
......
......@@ -32,6 +32,7 @@ import FamInstEnv
import TcHsType
import TcMType
import TcSimplify
import TcEvidence
import RnBinds
import RnEnv
......@@ -40,7 +41,6 @@ import HscTypes
import Class
import Type
import Coercion
import ErrUtils
import MkId
import DataCon
......@@ -1443,7 +1443,7 @@ genInst :: Bool -- True <=> standalone deriving
-> OverlapFlag
-> DerivSpec -> TcM (InstInfo RdrName, BagDerivStuff)
genInst standalone_deriv oflag
spec@(DS { ds_tc = rep_tycon, ds_tc_args = rep_tc_args
spec@(DS { ds_tvs = tvs, ds_tc = rep_tycon, ds_tc_args = rep_tc_args
, ds_theta = theta, ds_newtype = is_newtype
, ds_name = name, ds_cls = clas })
| is_newtype
......@@ -1462,12 +1462,12 @@ genInst standalone_deriv oflag
inst_spec = mkInstance oflag theta spec
co1 = case tyConFamilyCoercion_maybe rep_tycon of
Just co_con -> mkAxInstCo co_con rep_tc_args
Just co_con -> mkTcAxInstCo co_con rep_tc_args
Nothing -> id_co
-- Not a family => rep_tycon = main tycon
co2 = mkAxInstCo (newTyConCo rep_tycon) rep_tc_args
co = co1 `mkTransCo` co2
id_co = mkReflCo (mkTyConApp rep_tycon rep_tc_args)
co2 = mkTcAxInstCo (newTyConCo rep_tycon) rep_tc_args
co = mkTcForAllCos tvs (co1 `mkTcTransCo` co2)
id_co = mkTcReflCo (mkTyConApp rep_tycon rep_tc_args)
-- Example: newtype instance N [a] = N1 (Tree a)
-- deriving instance Eq b => Eq (N [(b,b)])
......
......@@ -60,7 +60,7 @@ import TcIface
import PrelNames
import TysWiredIn
import Id
import Coercion
import TcEvidence
import Var
import VarSet
import RdrName
......@@ -629,10 +629,10 @@ data InstBindings a
-- witness dictionary is identical to the argument
-- dictionary. Hence no bindings, no pragmas.
Coercion -- The coercion maps from newtype to the representation type
-- (mentioning type variables bound by the forall'd iSpec variables)
TcCoercion -- The coercion maps from newtype to the representation type
-- (quantified over type variables bound by the forall'd iSpec variables)
-- E.g. newtype instance N [a] = N1 (Tree a)
-- co : N [a] ~ Tree a
-- co : forall a. N [a] ~ Tree a
TyCon -- The TyCon is the newtype N. If it's indexed, then it's the