Commit 5822cb8d authored by chak@cse.unsw.edu.au.'s avatar chak@cse.unsw.edu.au.

Type checking for type synonym families

This patch introduces type checking for type families of which associated
type synonyms are a special case. E.g.

        type family Sum n m

        type instance Sum Zero n = n
        type instance Sum (Succ n) m = Succ (Sum n m)

where

        data Zero       -- empty type
        data Succ n     -- empty type

In addition we support equational constraints of the form:

        ty1 ~ ty2

(where ty1 and ty2 are arbitrary tau types) in any context where
type class constraints are already allowed, e.g.

        data Equals a b where
                Equals :: a ~ b => Equals a b

The above two syntactical extensions are disabled by default. Enable
with the -XTypeFamilies flag.

For further documentation about the patch, see:

        * the master plan
          http://hackage.haskell.org/trac/ghc/wiki/TypeFunctions

        * the user-level documentation
          http://haskell.org/haskellwiki/GHC/Indexed_types

The patch is mostly backwards compatible, except for:

        * Some error messages have been changed slightly.

        * Type checking of GADTs now requires a bit more type declarations:
          not only should the type of a GADT case scrutinee be given, but also
          that of any identifiers used in the branches and the return type.

Please report any unexpected behavior and incomprehensible error message 
for existing code.

Contributors (code and/or ideas):
        Tom Schrijvers
        Manuel Chakravarty
        Simon Peyton-Jones
        Martin Sulzmann 
with special thanks to Roman Leshchinskiy
parent db14f9df
Type functions
~~~~~~~~~~~~~~
* A Given inst should be a CoVar, not a coercion
* finaliseEqInst should not need to call zonk
* Why do we need fromGivenEqDict? How could we construct
a Dict that had an EqPred?
newDictBndr should make an EqInst directly
* tc_co should be accessed only inside Inst
* Inst.mkImplicTy needs a commment about filtering out EqInsts
How *do* we deal with wanted equalities?
* Inst.instType behaves inconsistently for EqInsts: it should
return an EqPred, like the instType' hack in pprDictsTheta
Consequences: adjust the uses of instType in TcSimplify
* tcDeref* functions are unused, except in tcGenericNormalizeFamInst, when
we can equally well use TcMType.lookupTcTyVar
* Coercion.mkEqPredCoI looks very peculiar.
-------------------------
*** unexpected failure for jtod_circint(opt)
......@@ -46,18 +73,6 @@ Cmm parser notes
do we need to assign to Node?
-------------------------
* Relation between separate type sigs and pattern type sigs
f :: forall a. a->a
f :: b->b = e -- No: monomorphic
f :: forall a. a->a
f :: forall a. a->a -- OK
f :: forall a. [a] -> [a]
f :: forall b. b->b = e ???
-------------------------------
NB: all floats are let-binds, but some non-rec lets
may be unlifted (with RHS ok-for-speculation)
......@@ -118,46 +133,6 @@ completeLazyBind: [given a simplified RHS]
Right hand sides and arguments
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
In many ways we want to treat
(a) the right hand side of a let(rec), and
(b) a function argument
in the same way. But not always! In particular, we would
like to leave these arguments exactly as they are, so they
will match a RULE more easily.
f (g x, h x)
g (+ x)
It's harder to make the rule match if we ANF-ise the constructor,
or eta-expand the PAP:
f (let { a = g x; b = h x } in (a,b))
g (\y. + x y)
On the other hand if we see the let-defns
p = (g x, h x)
q = + x
then we *do* want to ANF-ise and eta-expand, so that p and q
can be safely inlined.
Even floating lets out is a bit dubious. For let RHS's we float lets
out if that exposes a value, so that the value can be inlined more vigorously.
For example
r = let x = e in (x,x)
Here, if we float the let out we'll expose a nice constructor. We did experiments
that showed this to be a generally good thing. But it was a bad thing to float
lets out unconditionally, because that meant they got allocated more often.
For function arguments, there's less reason to expose a constructor (it won't
get inlined). Just possibly it might make a rule match, but I'm pretty skeptical.
So for the moment we don't float lets out of function arguments either.
Eta expansion
~~~~~~~~~~~~~~
......
......@@ -12,9 +12,10 @@ module DataCon (
dataConRepType, dataConSig, dataConFullSig,
dataConName, dataConIdentity, dataConTag, dataConTyCon, dataConUserType,
dataConUnivTyVars, dataConExTyVars, dataConAllTyVars,
dataConEqSpec, eqSpecPreds, dataConTheta, dataConStupidTheta,
dataConEqSpec, eqSpecPreds, dataConEqTheta, dataConDictTheta, dataConStupidTheta,
dataConInstArgTys, dataConOrigArgTys, dataConOrigResTy,
dataConInstOrigArgTys, dataConRepArgTys,
dataConInstOrigArgTys, dataConInstOrigDictsAndArgTys,
dataConRepArgTys,
dataConFieldLabels, dataConFieldType,
dataConStrictMarks, dataConExStricts,
dataConSourceArity, dataConRepArity,
......@@ -48,6 +49,7 @@ import Module
import Data.Char
import Data.Word
import Data.List ( partition )
\end{code}
......@@ -224,11 +226,11 @@ data DataCon
--
-- *** As declared by the user
-- data T a where
-- MkT :: forall x y. (Ord x) => x -> y -> T (x,y)
-- MkT :: forall x y. (x~y,Ord x) => x -> y -> T (x,y)
-- *** As represented internally
-- data T a where
-- MkT :: forall a. forall x y. (a:=:(x,y), Ord x) => x -> y -> T a
-- MkT :: forall a. forall x y. (a:=:(x,y),x~y,Ord x) => x -> y -> T a
--
-- The next six fields express the type of the constructor, in pieces
-- e.g.
......@@ -236,7 +238,8 @@ data DataCon
-- dcUnivTyVars = [a]
-- dcExTyVars = [x,y]
-- dcEqSpec = [a:=:(x,y)]
-- dcTheta = [Ord x]
-- dcEqTheta = [x~y]
-- dcDictTheta = [Ord x]
-- dcOrigArgTys = [a,List b]
-- dcRepTyCon = T
......@@ -244,7 +247,7 @@ data DataCon
-- Its type is of form
-- forall a1..an . t1 -> ... tm -> T a1..an
-- No existentials, no coercions, nothing.
-- That is: dcExTyVars = dcEqSpec = dcTheta = []
-- That is: dcExTyVars = dcEqSpec = dcEqTheta = dcDictTheta = []
-- NB 1: newtypes always have a vanilla data con
-- NB 2: a vanilla constructor can still be declared in GADT-style
-- syntax, provided its type looks like the above.
......@@ -272,11 +275,14 @@ data DataCon
-- Each equality is of the form (a :=: ty), where 'a' is one of
-- the universally quantified type variables
dcTheta :: ThetaType, -- The context of the constructor
-- The next two fields give the type context of the data constructor
-- (aside from the GADT constraints,
-- which are given by the dcExpSpec)
-- In GADT form, this is *exactly* what the programmer writes, even if
-- the context constrains only universally quantified variables
-- MkT :: forall a. Eq a => a -> T a
-- It may contain user-written equality predicates too
-- MkT :: forall a b. (a ~ b, Ord b) => a -> T a b
dcEqTheta :: ThetaType, -- The *equational* constraints
dcDictTheta :: ThetaType, -- The *type-class and implicit-param* constraints
dcStupidTheta :: ThetaType, -- The context of the data type declaration
-- data Eq a => T a = ...
......@@ -460,7 +466,7 @@ mkDataCon name declared_infix
-- so the error is detected properly... it's just that asaertions here
-- are a little dodgy.
= ASSERT( not (any isEqPred theta) )
= -- ASSERT( not (any isEqPred theta) )
-- We don't currently allow any equality predicates on
-- a data constructor (apart from the GADT ones in eq_spec)
con
......@@ -470,7 +476,8 @@ mkDataCon name declared_infix
dcVanilla = is_vanilla, dcInfix = declared_infix,
dcUnivTyVars = univ_tvs, dcExTyVars = ex_tvs,
dcEqSpec = eq_spec,
dcStupidTheta = stupid_theta, dcTheta = theta,
dcStupidTheta = stupid_theta,
dcEqTheta = eq_theta, dcDictTheta = dict_theta,
dcOrigArgTys = orig_arg_tys, dcOrigResTy = orig_res_ty,
dcRepTyCon = tycon,
dcRepArgTys = rep_arg_tys,
......@@ -486,9 +493,10 @@ mkDataCon name declared_infix
-- The 'arg_stricts' passed to mkDataCon are simply those for the
-- source-language arguments. We add extra ones for the
-- dictionary arguments right here.
dict_tys = mkPredTys theta
real_arg_tys = dict_tys ++ orig_arg_tys
real_stricts = map mk_dict_strict_mark theta ++ arg_stricts
(eq_theta,dict_theta) = partition isEqPred theta
dict_tys = mkPredTys dict_theta
real_arg_tys = dict_tys ++ orig_arg_tys
real_stricts = map mk_dict_strict_mark dict_theta ++ arg_stricts
-- Example
-- data instance T (b,c) where
......@@ -497,6 +505,7 @@ mkDataCon name declared_infix
-- The representation tycon looks like this:
-- data :R7T b c where
-- TI :: forall b1 c1. (b1 ~ c1) => b1 -> :R7T b1 c1
-- In this case orig_res_ty = T (e,e)
orig_res_ty = mkFamilyTyConApp tycon (substTyVars (mkTopTvSubst eq_spec) univ_tvs)
-- Representation arguments and demands
......@@ -506,6 +515,7 @@ mkDataCon name declared_infix
tag = assoc "mkDataCon" (tyConDataCons tycon `zip` [fIRST_TAG..]) con
ty = mkForAllTys univ_tvs $ mkForAllTys ex_tvs $
mkFunTys (mkPredTys (eqSpecPreds eq_spec)) $
mkFunTys (mkPredTys eq_theta) $
-- NB: the dict args are already in rep_arg_tys
-- because they might be flattened..
-- but the equality predicates are not
......@@ -548,8 +558,11 @@ dataConAllTyVars (MkData { dcUnivTyVars = univ_tvs, dcExTyVars = ex_tvs })
dataConEqSpec :: DataCon -> [(TyVar,Type)]
dataConEqSpec = dcEqSpec
dataConTheta :: DataCon -> ThetaType
dataConTheta = dcTheta
dataConEqTheta :: DataCon -> ThetaType
dataConEqTheta = dcEqTheta
dataConDictTheta :: DataCon -> ThetaType
dataConDictTheta = dcDictTheta
dataConWorkId :: DataCon -> Id
dataConWorkId dc = case dcIds dc of
......@@ -585,7 +598,7 @@ dataConStrictMarks = dcStrictMarks
dataConExStricts :: DataCon -> [StrictnessMark]
-- Strictness of *existential* arguments only
-- Usually empty, so we don't bother to cache this
dataConExStricts dc = map mk_dict_strict_mark (dcTheta dc)
dataConExStricts dc = map mk_dict_strict_mark $ dcDictTheta dc
dataConSourceArity :: DataCon -> Arity
-- Source-level arity of the data constructor
......@@ -608,14 +621,14 @@ dataConRepStrictness dc = dcRepStrictness dc
dataConSig :: DataCon -> ([TyVar], ThetaType, [Type], Type)
dataConSig (MkData {dcUnivTyVars = univ_tvs, dcExTyVars = ex_tvs, dcEqSpec = eq_spec,
dcTheta = theta, dcOrigArgTys = arg_tys, dcOrigResTy = res_ty})
= (univ_tvs ++ ex_tvs, eqSpecPreds eq_spec ++ theta, arg_tys, res_ty)
dcEqTheta = eq_theta, dcDictTheta = dict_theta, dcOrigArgTys = arg_tys, dcOrigResTy = res_ty})
= (univ_tvs ++ ex_tvs, eqSpecPreds eq_spec ++ eq_theta ++ dict_theta, arg_tys, res_ty)
dataConFullSig :: DataCon
-> ([TyVar], [TyVar], [(TyVar,Type)], ThetaType, [Type], Type)
-> ([TyVar], [TyVar], [(TyVar,Type)], ThetaType, ThetaType, [Type], Type)
dataConFullSig (MkData {dcUnivTyVars = univ_tvs, dcExTyVars = ex_tvs, dcEqSpec = eq_spec,
dcTheta = theta, dcOrigArgTys = arg_tys, dcOrigResTy = res_ty})
= (univ_tvs, ex_tvs, eq_spec, theta, arg_tys, res_ty)
dcEqTheta = eq_theta, dcDictTheta = dict_theta, dcOrigArgTys = arg_tys, dcOrigResTy = res_ty})
= (univ_tvs, ex_tvs, eq_spec, eq_theta, dict_theta, arg_tys, res_ty)
dataConOrigResTy :: DataCon -> Type
dataConOrigResTy dc = dcOrigResTy dc
......@@ -633,10 +646,11 @@ dataConUserType :: DataCon -> Type
-- mentions the family tycon, not the internal one.
dataConUserType (MkData { dcUnivTyVars = univ_tvs,
dcExTyVars = ex_tvs, dcEqSpec = eq_spec,
dcTheta = theta, dcOrigArgTys = arg_tys,
dcEqTheta = eq_theta, dcDictTheta = dict_theta, dcOrigArgTys = arg_tys,
dcOrigResTy = res_ty })
= mkForAllTys ((univ_tvs `minusList` map fst eq_spec) ++ ex_tvs) $
mkFunTys (mkPredTys theta) $
mkFunTys (mkPredTys eq_theta) $
mkFunTys (mkPredTys dict_theta) $
mkFunTys arg_tys $
res_ty
......@@ -671,6 +685,21 @@ dataConInstOrigArgTys dc@(MkData {dcOrigArgTys = arg_tys,
map (substTyWith tyvars inst_tys) arg_tys
where
tyvars = univ_tvs ++ ex_tvs
dataConInstOrigDictsAndArgTys
:: DataCon -- Works for any DataCon
-> [Type] -- Includes existential tyvar args, but NOT
-- equality constraints or dicts
-> [Type] -- Returns just the instsantiated dicts and *value* arguments
dataConInstOrigDictsAndArgTys dc@(MkData {dcOrigArgTys = arg_tys,
dcDictTheta = dicts,
dcUnivTyVars = univ_tvs,
dcExTyVars = ex_tvs}) inst_tys
= ASSERT2( length tyvars == length inst_tys
, ptext SLIT("dataConInstOrigDictsAndArgTys") <+> ppr dc $$ ppr tyvars $$ ppr inst_tys )
map (substTyWith tyvars inst_tys) (mkPredTys dicts ++ arg_tys)
where
tyvars = univ_tvs ++ ex_tvs
\end{code}
These two functions get the real argument types of the constructor,
......
......@@ -44,6 +44,7 @@ import TysPrim
import TysWiredIn
import PrelRules
import Type
import TypeRep
import TcGadt
import Coercion
import TcType
......@@ -59,7 +60,7 @@ import PrimOp
import ForeignCall
import DataCon
import Id
import Var ( Var, TyVar)
import Var ( Var, TyVar, mkCoVar)
import IdInfo
import NewDemand
import DmdAnal
......@@ -223,7 +224,7 @@ mkDataConIds wrap_name wkr_name data_con
= DCIds Nothing wrk_id
where
(univ_tvs, ex_tvs, eq_spec,
theta, orig_arg_tys, res_ty) = dataConFullSig data_con
eq_theta, dict_theta, orig_arg_tys, res_ty) = dataConFullSig data_con
tycon = dataConTyCon data_con -- The representation TyCon (not family)
----------- Worker (algebraic data types only) --------------
......@@ -270,8 +271,11 @@ mkDataConIds wrap_name wkr_name data_con
nt_work_info = noCafIdInfo -- The NoCaf-ness is set by noCafIdInfo
`setArityInfo` 1 -- Arity 1
`setUnfoldingInfo` newtype_unf
newtype_unf = ASSERT( isVanillaDataCon data_con &&
isSingleton orig_arg_tys )
newtype_unf = -- The assertion below is no longer correct:
-- there may be a dict theta rather than a singleton orig_arg_ty
-- ASSERT( isVanillaDataCon data_con &&
-- isSingleton orig_arg_tys )
--
-- No existentials on a newtype, but it can have a context
-- e.g. newtype Eq a => T a = MkT (...)
mkCompulsoryUnfolding $
......@@ -279,7 +283,11 @@ mkDataConIds wrap_name wkr_name data_con
wrapNewTypeBody tycon res_ty_args
(Var id_arg1)
id_arg1 = ASSERT( not (null orig_arg_tys) ) mkTemplateLocal 1 (head orig_arg_tys)
id_arg1 = mkTemplateLocal 1
(if null orig_arg_tys
then ASSERT(not (null $ dataConDictTheta data_con)) mkPredTy $ head (dataConDictTheta data_con)
else head orig_arg_tys
)
----------- Wrapper --------------
-- We used to include the stupid theta in the wrapper's args
......@@ -287,8 +295,9 @@ mkDataConIds wrap_name wkr_name data_con
-- extra constraints where necessary.
wrap_tvs = (univ_tvs `minusList` map fst eq_spec) ++ ex_tvs
res_ty_args = substTyVars (mkTopTvSubst eq_spec) univ_tvs
dict_tys = mkPredTys theta
wrap_ty = mkForAllTys wrap_tvs $ mkFunTys dict_tys $
eq_tys = mkPredTys eq_theta
dict_tys = mkPredTys dict_theta
wrap_ty = mkForAllTys wrap_tvs $ mkFunTys eq_tys $ mkFunTys dict_tys $
mkFunTys orig_arg_tys $ res_ty
-- NB: watch out here if you allow user-written equality
-- constraints in data constructor signatures
......@@ -318,6 +327,7 @@ mkDataConIds wrap_name wkr_name data_con
wrap_unf = mkTopUnfolding $ Note InlineMe $
mkLams wrap_tvs $
mkLams eq_args $
mkLams dict_args $ mkLams id_args $
foldr mk_case con_app
(zip (dict_args ++ id_args) all_strict_marks)
......@@ -327,11 +337,18 @@ mkDataConIds wrap_name wkr_name data_con
Var wrk_id `mkTyApps` res_ty_args
`mkVarApps` ex_tvs
`mkTyApps` map snd eq_spec -- Equality evidence
`mkVarApps` eq_args
`mkVarApps` reverse rep_ids
(dict_args,i2) = mkLocals 1 dict_tys
(id_args,i3) = mkLocals i2 orig_arg_tys
wrap_arity = i3-1
(eq_args,_) = mkCoVarLocals i3 eq_tys
mkCoVarLocals i [] = ([],i)
mkCoVarLocals i (x:xs) = let (ys,j) = mkCoVarLocals (i+1) xs
y = mkCoVar (mkSysTvName (mkBuiltinUnique i) FSLIT("dc_co")) x
in (y:ys,j)
mk_case
:: (Id, StrictnessMark) -- Arg, strictness
......@@ -493,7 +510,7 @@ mkRecordSelId tycon field_label
has_field con = field_label `elem` dataConFieldLabels con
con1 = ASSERT( not (null data_cons_w_field) ) head data_cons_w_field
(univ_tvs, _, eq_spec, _, _, data_ty) = dataConFullSig con1
(univ_tvs, _, eq_spec, _, _, _, data_ty) = dataConFullSig con1
-- For a data type family, the data_ty (and hence selector_ty) mentions
-- only the family TyCon, not the instance TyCon
data_tv_set = tyVarsOfType data_ty
......@@ -792,7 +809,7 @@ mkDictSelId name clas
-- C a -> C a
-- for a single-op class (after all, the selector is the identity)
-- But it's type must expose the representation of the dictionary
-- to gat (say) C a -> (a -> a)
-- to get (say) C a -> (a -> a)
info = noCafIdInfo
`setArityInfo` 1
......@@ -814,16 +831,24 @@ mkDictSelId name clas
tycon = classTyCon clas
[data_con] = tyConDataCons tycon
tyvars = dataConUnivTyVars data_con
arg_tys = ASSERT( isVanillaDataCon data_con ) dataConRepArgTys data_con
arg_tys = {- ASSERT( isVanillaDataCon data_con ) -} dataConRepArgTys data_con
eq_theta = dataConEqTheta data_con
the_arg_id = assoc "MkId.mkDictSelId" (map idName (classSelIds clas) `zip` arg_ids) name
pred = mkClassPred clas (mkTyVarTys tyvars)
(dict_id:arg_ids) = mkTemplateLocals (mkPredTy pred : arg_tys)
pred = mkClassPred clas (mkTyVarTys tyvars)
dict_id = mkTemplateLocal 1 $ mkPredTy pred
(eq_ids,n) = mkCoVarLocals 2 $ mkPredTys eq_theta
arg_ids = mkTemplateLocalsNum n arg_tys
mkCoVarLocals i [] = ([],i)
mkCoVarLocals i (x:xs) = let (ys,j) = mkCoVarLocals (i+1) xs
y = mkCoVar (mkSysTvName (mkBuiltinUnique i) FSLIT("dc_co")) x
in (y:ys,j)
rhs = mkLams tyvars (Lam dict_id rhs_body)
rhs = mkLams tyvars (Lam dict_id rhs_body)
rhs_body | isNewTyCon tycon = unwrapNewTypeBody tycon (map mkTyVarTy tyvars) (Var dict_id)
| otherwise = Case (Var dict_id) dict_id (idType the_arg_id)
[(DataAlt data_con, arg_ids, Var the_arg_id)]
[(DataAlt data_con, eq_ids ++ arg_ids, Var the_arg_id)]
\end{code}
......
......@@ -201,7 +201,8 @@ mkTyVar name kind = ASSERT( not (isCoercionKind kind ) )
mkTcTyVar :: Name -> Kind -> TcTyVarDetails -> TyVar
mkTcTyVar name kind details
= ASSERT( not (isCoercionKind kind) )
= -- TOM: no longer valid assertion?
-- ASSERT( not (isCoercionKind kind) )
TcTyVar { varName = name,
realUnique = getKey# (nameUnique name),
varType = kind,
......
......@@ -664,7 +664,7 @@ dataConRepInstPat = dataConInstPat dataConRepArgTys (repeat (FSLIT("ipv")))
dataConRepFSInstPat = dataConInstPat dataConRepArgTys
dataConOrigInstPat = dataConInstPat dc_arg_tys (repeat (FSLIT("ipv")))
where
dc_arg_tys dc = map mkPredTy (dataConTheta dc) ++ dataConOrigArgTys dc
dc_arg_tys dc = map mkPredTy (dataConEqTheta dc) ++ map mkPredTy (dataConDictTheta dc) ++ dataConOrigArgTys dc
-- Remember to include the existential dictionaries
dataConInstPat :: (DataCon -> [Type]) -- function used to find arg tys
......@@ -680,9 +680,13 @@ dataConInstPat :: (DataCon -> [Type]) -- function used to find arg tys
--
-- co_tvs are intended to be used as binders for coercion args and the kinds
-- of these vars have been instantiated by the inst_tys and the ex_tys
-- The co_tvs include both GADT equalities (dcEqSpec) and
-- programmer-specified equalities (dcEqTheta)
--
-- arg_ids are indended to be used as binders for value arguments, including
-- dicts, and their types have been instantiated with inst_tys and ex_tys
-- arg_ids are indended to be used as binders for value arguments,
-- and their types have been instantiated with inst_tys and ex_tys
-- The arg_ids include both dicts (dcDictTheta) and
-- programmer-specified arguments (after rep-ing) (deRepArgTys)
--
-- Example.
-- The following constructor T1
......@@ -702,16 +706,17 @@ dataConInstPat :: (DataCon -> [Type]) -- function used to find arg tys
-- where the double-primed variables are created with the FastStrings and
-- Uniques given as fss and us
dataConInstPat arg_fun fss uniqs con inst_tys
= (ex_bndrs, co_bndrs, id_bndrs)
= (ex_bndrs, co_bndrs, arg_ids)
where
univ_tvs = dataConUnivTyVars con
ex_tvs = dataConExTyVars con
arg_tys = arg_fun con
eq_spec = dataConEqSpec con
eq_preds = eqSpecPreds eq_spec
eq_theta = dataConEqTheta con
eq_preds = eqSpecPreds eq_spec ++ eq_theta
n_ex = length ex_tvs
n_co = length eq_spec
n_co = length eq_preds
-- split the Uniques and FastStrings
(ex_uniqs, uniqs') = splitAt n_ex uniqs
......@@ -739,7 +744,7 @@ dataConInstPat arg_fun fss uniqs con inst_tys
-- make value vars, instantiating types
mk_id_var uniq fs ty = mkUserLocal (mkVarOccFS fs) uniq (substTy subst ty) noSrcSpan
id_bndrs = zipWith3 mk_id_var id_uniqs id_fss arg_tys
arg_ids = zipWith3 mk_id_var id_uniqs id_fss arg_tys
exprIsConApp_maybe :: CoreExpr -> Maybe (DataCon, [CoreExpr])
-- Returns (Just (dc, [x1..xn])) if the argument expression is
......
......@@ -468,6 +468,8 @@ instScheme ty | (tvs, rho) <- tcSplitForAllTys ty = liftTcM$ do
-- do its magic.
addConstraint :: TcType -> TcType -> TR ()
addConstraint t1 t2 = congruenceNewtypes t1 t2 >>= uncurry unifyType
>> return () -- TOMDO: what about the coercion?
-- we should consider family instances
......
......@@ -100,7 +100,7 @@ mkHsDictLet binds expr
val_binds = ValBindsOut [(Recursive, binds)] []
mkHsConApp :: DataCon -> [Type] -> [HsExpr Id] -> LHsExpr Id
-- Used for constructing dictinoary terms etc, so no locations
-- Used for constructing dictionary terms etc, so no locations
mkHsConApp data_con tys args
= foldl mk_app (nlHsTyApp (dataConWrapId data_con) tys) args
where
......
......@@ -29,6 +29,9 @@ import TyCon
import Type
import Coercion
import TcRnMonad
import Outputable
import Data.List
\end{code}
......@@ -132,6 +135,7 @@ mkNewTyConRhs tycon_name tycon con
= Just co_tycon
| otherwise
= Nothing
; traceIf (text "mkNewTyConRhs" <+> ppr cocon_maybe)
; return (NewTyCon { data_con = con,
nt_rhs = rhs_ty,
nt_etad_rhs = (etad_tvs, etad_rhs),
......@@ -145,7 +149,9 @@ mkNewTyConRhs tycon_name tycon con
-- non-recursive newtypes
all_coercions = True
tvs = tyConTyVars tycon
rhs_ty = head (dataConInstOrigArgTys con (mkTyVarTys tvs))
rhs_ty = ASSERT(not (null (dataConInstOrigDictsAndArgTys con (mkTyVarTys tvs))))
-- head (dataConInstOrigArgTys con (mkTyVarTys tvs))
head (dataConInstOrigDictsAndArgTys con (mkTyVarTys tvs))
-- Instantiate the data con with the
-- type variables from the tycon
-- NB: a newtype DataCon has no existentials; hence the
......@@ -274,44 +280,48 @@ buildClass :: Name -> [TyVar] -> ThetaType
-> TcRnIf m n Class
buildClass class_name tvs sc_theta fds ats sig_stuff tc_isrec
= do { tycon_name <- newImplicitBinder class_name mkClassTyConOcc
= do { traceIf (text "buildClass")
; tycon_name <- newImplicitBinder class_name mkClassTyConOcc
; datacon_name <- newImplicitBinder class_name mkClassDataConOcc
-- The class name is the 'parent' for this datacon, not its tycon,
-- because one should import the class to get the binding for
-- the datacon
; sc_sel_names <- mapM (newImplicitBinder class_name . mkSuperDictSelOcc)
[1..length sc_theta]
-- We number off the superclass selectors, 1, 2, 3 etc so that we
-- can construct names for the selectors. Thus
-- class (C a, C b) => D a b where ...
-- gives superclass selectors
-- D_sc1, D_sc2
-- (We used to call them D_C, but now we can have two different
-- superclasses both called C!)
; fixM (\ rec_clas -> do { -- Only name generation inside loop
let { rec_tycon = classTyCon rec_clas
; op_tys = [ty | (_,_,ty) <- sig_stuff]
; sc_tys = mkPredTys sc_theta
; dict_component_tys = sc_tys ++ op_tys
; sc_sel_ids = [mkDictSelId sc_name rec_clas | sc_name <- sc_sel_names]
; op_items = [ (mkDictSelId op_name rec_clas, dm_info)
| (op_name, dm_info, _) <- sig_stuff ] }
let { rec_tycon = classTyCon rec_clas
; op_tys = [ty | (_,_,ty) <- sig_stuff]
; op_items = [ (mkDictSelId op_name rec_clas, dm_info)
| (op_name, dm_info, _) <- sig_stuff ] }
-- Build the selector id and default method id
; dict_con <- buildDataCon datacon_name
False -- Not declared infix
(map (const NotMarkedStrict) dict_component_tys)
(map (const NotMarkedStrict) op_tys)
[{- No labelled fields -}]
tvs [{- no existentials -}]
[{- No equalities -}] [{-No context-}]
dict_component_tys
[{- No GADT equalities -}] sc_theta
op_tys
rec_tycon
; rhs <- case dict_component_tys of
[rep_ty] -> mkNewTyConRhs tycon_name rec_tycon dict_con
other -> return (mkDataTyConRhs [dict_con])
; sc_sel_names <- mapM (newImplicitBinder class_name . mkSuperDictSelOcc)
[1..length (dataConDictTheta dict_con)]
-- We number off the Dict superclass selectors, 1, 2, 3 etc so that we
-- can construct names for the selectors. Thus
-- class (C a, C b) => D a b where ...
-- gives superclass selectors
-- D_sc1, D_sc2
-- (We used to call them D_C, but now we can have two different
-- superclasses both called C!)
; let sc_sel_ids = [mkDictSelId sc_name rec_clas | sc_name <- sc_sel_names]
-- Use a newtype if the class constructor has exactly one field:
-- i.e. exactly one operation or superclass taken together
-- Watch out: the sc_theta includes equality predicates,
-- which don't count for this purpose; hence dataConDictTheta
; rhs <- if ((length $ dataConDictTheta dict_con) + length sig_stuff) == 1
then mkNewTyConRhs tycon_name rec_tycon dict_con
else return (mkDataTyConRhs [dict_con])
; let { clas_kind = mkArrowKinds (map tyVarKind tvs) liftedTypeKind
......@@ -326,10 +336,13 @@ buildClass class_name tvs sc_theta fds ats sig_stuff tc_isrec
-- newtype like a synonym, but that will lead to an infinite
-- type]
; atTyCons = [tycon | ATyCon tycon <- ats]
; result = mkClass class_name tvs fds
sc_theta sc_sel_ids atTyCons
op_items tycon
}
; return (mkClass class_name tvs fds
sc_theta sc_sel_ids atTyCons op_items
tycon)
; traceIf (text "buildClass" <+> ppr tycon)
; return result
})}
\end{code}
......
......@@ -1218,7 +1218,7 @@ tyThingToIfaceDecl (ATyCon tycon)
ifConUnivTvs = toIfaceTvBndrs (dataConUnivTyVars data_con),
ifConExTvs = toIfaceTvBndrs (dataConExTyVars data_con),
ifConEqSpec = to_eq_spec (dataConEqSpec data_con),
ifConCtxt = toIfaceContext (dataConTheta data_con),
ifConCtxt = toIfaceContext (dataConEqTheta data_con ++ dataConDictTheta data_con),
ifConArgTys = map toIfaceType (dataConOrigArgTys data_con),
ifConFields = map getOccName
(dataConFieldLabels data_con),
......
......@@ -29,20 +29,29 @@ module Inst (
lookupSimpleInst, LookupInstResult(..),
tcExtendLocalInstEnv, tcGetInstEnvs, getOverlapFlag,
isAbstractableInst, isEqInst,
isDict, isClassDict, isMethod, isImplicInst,
isIPDict, isInheritableInst, isMethodOrLit,
isTyVarDict, isMethodFor,
zonkInst, zonkInsts,
instToId, instToVar, instName,
instToId, instToVar, instType, instName,
InstOrigin(..), InstLoc, pprInstLoc
InstOrigin(..), InstLoc, pprInstLoc,
mkWantedCo, mkGivenCo,
fromWantedCo, fromGivenCo,
eitherEqInst, mkEqInst, mkEqInsts,
finalizeEqInst, writeWantedCoercion,
eqInstType, updateEqInstCoercion,
eqInstCoercion,
eqInstLeftTy, eqInstRightTy
) where
#include "HsVersions.h"
import {-# SOURCE #-} TcExpr( tcPolyExpr )
import {-# SOURCE #-} TcUnify( unifyType )
import {-# SOURCE #-} TcUnify( boxyUnify, unifyType )
import FastString(FastString)
import HsSyn
......@@ -54,6 +63,8 @@ import FunDeps
import TcMType
import TcType