HaRe-0.6: tools/base/TC/TypeCheck.hs
-- $Id: TypeCheck.hs,v 1.39 2001/09/29 00:08:23 diatchki Exp $
module TypeCheck where
import TypeGenerics
import Monad(mapM, foldM)
import HsName
import HsTypeStruct
import Syntax
import InferenceMonad
import List(nub, find, intersect, (\\), lookup, union)
import ST
import SCC(bindingGroups)
import qualified Scope
import SyntaxUtil(getTyName)
------------------------------------------------------
infix 9 |->
infixr 3 +:
type Kind a = GT K Sort (STRef a)
type Type a = GT T (Kind a) (STRef a)
type NGV a = [(HsName, Type a)]
type Env a = [(HsName, Scheme a)]
type Constrs a = [Pred a]
type Ref a = (Int,STRef a (Maybe(Type a)))
type Ptr2 a = STRef a (Maybe(Type a))
type Genfun a = String -> IM a Error HsName
type KindEnv a = [(HsName, GT K Sort (STRef a))]
data Pred a = IsIn HsName [Type a]
data Scheme a = Sch [Kind a] [Pred a] (Type a)
data Qual a x = [Pred a] :=> x
data Assump name a = name :>: Scheme a
data Error = TCerror String
instance Show Error where
show (TCerror s) = s
fails :: String -> IM a Error x
fails s = raise (TCerror s)
unifyErr x y z = fails ((show x) ++"error in unification " ++ (show y)++", "++(show z))
instance Show (STRef a b) where
show x = "?"
--------------------------------------------------------
newGensym :: IM a Error (Genfun a)
newGensym =
do { seed <- newRef (1::Int)
; let gensym s = do { n <- readVar seed
; writeVar seed (n+1)
; return (UnQual (s ++ (show n)))
}
in return gensym
}
{-gensym s = do { n <- nextN
; return (UnQual (s ++ (show n)))
}
-}
------------------ Kind inference -----------------------
data Sort = Sort deriving Eq
kindA :: A K Sort () (STRef a) (IM a Error)
kindA =
A { sameVarA = refEq
, writeVarA = writeVar
, readVarA = readVar
, newVarA = newRef
, nextA = nextN
, zeroA = ()
, unionA = const ()
, genErrA = unifyErr
, seqA = seqK
, mapA = mapK
, accA f = flip (accK f)
, matchA = matchK
, kindofA = const(return Sort)
, samekindA = (==)
}
refEq :: STRef a b -> STRef a b -> Bool
refEq x y = x==y
eqK :: Kind a -> Kind a -> Bool
B{ unifyGT = unifyKind
, equalGT = eqK
, freshGT = newVarK
, pruneGT = pruneK
, substGT = substK
, genGT = genK } = makeUnify kindA
star = S Kstar
arrowK x y = S(Kfun x y)
predicate = S Kpred
instance Eq (Kind a) where
(==) = eqK
-- Works on HSTypes while inferK2 works on (Type a)
inferK :: [(HsName,Kind a)] -> Kind a -> HsType -> IM a Error (Kind a)
inferK kenv k t =
do { let f (nm,k) = do { v <- newVar k; return (nm,v)}
h :: [(HsName,Type a)] -> HsType -> Type a
h pairs (Typ (HsTyVar x)) = look pairs x
h pairs (Typ x) = S(mapT (h pairs) x)
; pairs <- mapM f kenv
; inferK2 kenv k (h pairs t)
}
inferK2 :: [(HsName, Kind a)] -> Kind a -> (Type a) -> IM a Error (Kind a)
inferK2 env hint t =
do { t' <- prune t
; case t' of
(TVar r k) -> return k
(TGen n) -> return hint
(S typ) ->
case typ of
(HsTyFun x y) ->
do { x' <- inferK2 env star x
; y' <- inferK2 env star y
; unifyKind hint star
; return hint
}
(HsTyTuple ts) ->
do { sequence (map (inferK2 env star) ts)
; unifyKind hint star
; return star
}
(HsTyApp f x) ->
do { a <- newVarK Sort
; inferK2 env (S(Kfun a hint)) f
; inferK2 env a x
; return hint
}
(HsTyVar nm) ->
do { unifyKind hint (lookUpEnv env nm)
; return hint
}
(HsTyCon nm) ->
do { unifyKind hint (lookUpEnv env nm)
; return hint
} }
kindOf2 :: [(HsName,Kind a)] -> Type a -> IM a Error (Kind a)
kindOf2 envf x = do { hint <- newVarK Sort
; inferK2 envf hint x
; (ks,ts,x') <- genK (\ x -> return True) hint
; k' <- substK (repeat star) x'
; return k'
}
getkind :: Type a -> IM a Error (Kind a)
getkind t = kindOf2 kenv0 t
--------------------------------------------------------------
typeA :: A T (Kind c) [Pred c] (STRef c) (IM c Error)
typeA =
A { sameVarA = refEq
, writeVarA = writeVar
, readVarA = readVar
, newVarA = newRef
, nextA = nextN
, zeroA = []
, unionA = concat
, genErrA = unifyErr
, seqA = seqT
, mapA = mapT
, accA = accT
, matchA = matchT
, kindofA = getkind
, samekindA = eqK
}
prune :: Type a -> IM a Error (Type a)
unify :: Type a -> Type a -> IM a Error [Pred a]
subst :: [Type a] -> Type a -> IM a Error (Type a)
B{ unifyGT = unify
, matchGT = matchType
, equalGT = teq
, freshGT = newVar
, colGT = col
, occursGT = occursIn
, pruneGT = prune
, substGT = subst
, genmapGT = gen
} = makeUnify typeA
match :: Type a -> Type a -> IM a Error Bool
match x y = (do { matchType x y; return True}) `handle` (\ _ -> return False)
unifyList xs ys =
if (length xs) == (length ys)
then do { xss <- mapM (uncurry unify) (zip xs ys)
; return (concat xss)
}
else fails "Lists not same length"
---------------------------------------------------------------
class Types t a where
tv :: t -> IM a Error [Ref a]
collapse :: t -> IM a Error t
instance Types (Type a) a where
tv t = do { t' <- prune t
; case t' of
(TVar r k) -> return [r]
(S x) -> do { sh <- seqT (mapT tv x)
; return $ nub (accT (++) sh [])
}
(TGen i) -> return []}
collapse t = col t
instance Types x a => Types [x] a where
tv xs = do { xs' <- mapM tv xs; return(concat xs') }
collapse ts = mapM collapse ts
instance Types (Pred a) a where
tv (IsIn nm xs) = tv xs
collapse (IsIn nm xs) = do {xs' <- collapse xs; return(IsIn nm xs')}
instance Types(Scheme a) a where
tv (Sch ks ps t) = do {ps' <- tv ps; t' <- tv t; return(union ps' t')}
collapse (Sch ks ps t) =
do {ps' <- collapse ps; t' <- collapse t; return(Sch ks ps' t')}
instance Types y a => Types (x,y) a where
tv (x,y) = tv y
collapse (x,y) = do {y' <- collapse y; return (x,y') }
-----------------------------------------------------------------
class Instantiate x a where
inst :: [Type a] -> x -> IM a Error x
instance Instantiate (Pred a) a where
inst ts (IsIn nm xs) = do { xs' <- mapM (inst ts) xs; return (IsIn nm xs') }
instance Instantiate x a => Instantiate [x] a where
inst ts xs = mapM (inst ts) xs
instance Instantiate (Type a) a where
inst = subst
--------------------------------------------------
class Template x a where
fresh :: x -> IM a Error x
instance Template (Scheme a) a where
fresh (Sch free cs t) =
do { sub <- mapM newVar free
; t' <- inst sub t
; cs' <- sequence (map (inst sub) cs)
; return $ Sch free cs' t'
}
instance Template (Inst a) a where
fresh (Inst free ps p) =
do { sub <- mapM newVar free
; p' <- inst sub p
; ps' <- sequence (map (inst sub) ps)
; return $ Inst free ps' p'
}
--------------- Environment function and types --------------------------
extend f s t = (s,t) : f
lambdaExt :: [(name,Scheme a)] -> name -> Type a -> [(name,Scheme a)]
lambdaExt env vname vtyp = extend env vname (Sch [] [] vtyp)
lambdaExtTCE env vname vtyp = extTrm vname (Sch [] [] vtyp) env
envf [] s = error ("variable not found: "++(show s)++"\n")
envf ((x,t):m) s = if x==s then t else envf m s
-------- Type constructors and types of literal constants ------------
starKind = S(Kstar)
arrowKind x y =S(Kfun x y)
predKind = S Kpred
tArrow x y = S(HsTyFun x y)
tTuple ts = S(HsTyTuple ts)
tInteger = S(HsTyCon (UnQual "Integer"))
tInt = S(HsTyCon (UnQual "Int"))
tChar = S(HsTyCon (UnQual "Char"))
tString = tlist tChar
tRational = S(HsTyCon (UnQual "Rational"))
tBool = S(HsTyCon (UnQual "Bool"))
tDouble = S(HsTyCon (UnQual "Double"))
tStringHash = S(HsTyCon (UnQual "stringHash"))
tCharHash = S(HsTyCon (UnQual "CharHash"))
tIntHash = S(HsTyCon (UnQual "IntHash"))
tRationalHash = S(HsTyCon (UnQual "RationalHash"))
tlist x = S(HsTyApp tlistCon x)
tlistCon = (S(HsTyCon (UnQual "[]")))
tcode x = S(HsTyApp tcodeCon x)
tcodeCon = (S(HsTyCon (UnQual "Code")))
litTyp (HsInt _) = tInteger
litTyp (HsChar _) = tChar
litTyp (HsString _) = tString
litTyp (HsFrac _) = tRational
litTyp (HsCharPrim _) = tCharHash
litTyp (HsStringPrim _) = tStringHash
litTyp (HsIntPrim _) = tIntHash
litTyp (HsFloatPrim _) = tRationalHash
litTyp (HsDoublePrim _) = tRationalHash
---------------------------------------------------
-- Kind environment stuff
funkify [] env = env
funkify ((a,b):rest) env = (a,b) +: (funkify rest env)
hsname |-> knd = (hsname,knd)
--(x,y) +: env = \t -> if x == t then y else lookUpEnv env t
(x,y) +: env = (x,y) : env
--emptyKEnv x = error $ "unknown kinnd variable: " ++ (show x)
emptyKEnv = []
lookUpEnv env t =
case List.lookup t env of
Just b -> b
Nothing -> error $ "Kind environment: " ++ (show t) ++ "not found!"
kenv0 =
(UnQual "Integer") |-> star +:
(UnQual "Int") |-> star +:
(UnQual "Char") |-> star +:
(UnQual "Rational") |-> star +:
(UnQual "Bool") |-> star +:
(UnQual "Double") |-> star +:
(UnQual "stringHash") |-> star +:
(UnQual "CharHash") |-> star +:
(UnQual "IntHash") |-> star +:
(UnQual "RationalHash") |-> star +:
(UnQual "[]") |-> arrowK star star +:
(UnQual "Q") |-> arrowK star star +:
(UnQual "X") |-> arrowK star star +:
(UnQual "W") |-> arrowK star star +:
(UnQual "Num") |-> arrowK star predicate +: emptyKEnv
------------------------ Predefined Class predicates ----------------
num x = IsIn (UnQual "Num") [x]
monad x = IsIn (UnQual "Monad") [x]
enum x = IsIn (UnQual "Enum") [x]
-----------------------------------------------------------------------------
-- This mimics the "Class Environments" Section (7.2) of Typing Haskell in
-- Haskell. The differences are:
-- 1) Class environments are lists rather than partial functions
-- 1) Many functions are in the (IM a Error) Monad instead of the Maybe Monad
-- 2) instead of Inst = Qual Pred
-- data INST a = INST [Kind] [Pred a] (Pred a)
-- An instance is like a (Sch ks ps t), a fresh copy of an instance
-- can be made by applying the method "inst". this is usefull for
-- determining if we have overlapping instances. We make fresh copies,
-- and then we unify. Also like Schemes, things of type (Inst a) have a
-- normal form, because of this, and because (Inst a) should be TVar free
-- they can be compared for equality.
data Class a = Class HsName [HsName] [Inst a]
data ClassEnv a = ClassEnv { classList :: [(HsName, Class a)]
, defaults :: [Type a]
}
data Inst a = Inst [Kind a] [Pred a] (Pred a)
instance Instantiate (Inst a) a where
inst ts (Inst ks ps p) =
do { ps' <- (inst ts ps)
; p' <- (inst ts p)
; return (Inst ks ps' p')
}
instance Eq (Inst a) where
(Inst ks1 ps1 p1) == (Inst ks2 ps2 p2) =
listEq (==) ks1 ks2 && listEq (==) ps1 ps2 && p1 == p2
instance Eq (Pred a) where
(IsIn c ts) == (IsIn d xs) = c==d && listEq teq ts xs
listEq eqf [] [] = True
listEq eqf (x:xs) (y :ys) = eqf x y && listEq eqf xs ys
listEq eqf _ _ = False
-----------------------------------------------------------------------
classes :: ClassEnv a -> HsName -> Maybe (Class a)
classes ce i =
case find ( \ (x,y) -> x==i) (classList ce) of
Just (name,cl) -> Just cl
Nothing -> Nothing
super :: ClassEnv a -> HsName -> [HsName]
super ce i = case classes ce i of Just (Class name sup insts) -> sup
insts :: ClassEnv a -> HsName -> [Inst a]
insts ce i = case classes ce i of Just (Class name sup its) -> its
defined :: Maybe a -> Bool
defined (Just _) = True
defined Nothing = False
modify :: ClassEnv a -> HsName -> Class a -> ClassEnv a
modify ce i c = ce {classList = (i,c) : classList ce }
initialEnv :: ClassEnv a
initialEnv = ClassEnv { classList = [], defaults = [tInteger,tDouble] }
type EnvTransformer a = ClassEnv a -> IM a Error (ClassEnv a)
infixr 5 <:>
(<:>) :: EnvTransformer a -> EnvTransformer a -> EnvTransformer a
(f <:> g) ce = do { ce' <- f ce; g ce' }
{- ClassEnv a -> Maybe (ClassEnv a) -}
addClass :: String -> [String] -> EnvTransformer a
addClass i is ce
| defined (classes ce (UnQual i)) =
fails ("Adding class: "++(show i)++
" to class environment failed. Class already defined. ")
| any (not . defined . (classes ce)) (map UnQual is) =
fails("Adding class: "++(show i)++
" to class environment failed. Superclass not defined. ")
| otherwise = return (modify ce (UnQual i) (Class (UnQual i) (map UnQual is) [] ))
addCoreClasses :: EnvTransformer a
addCoreClasses
= addClass "Eq" []
<:> addClass "Ord" ["Eq"]
<:> addClass "Show" []
<:> addClass "Read" []
<:> addClass "Bounded" []
<:> addClass "Enum" []
<:> addClass "Functor" []
<:> addClass "Monad" []
addNumClasses :: EnvTransformer a
addNumClasses
= addClass "Num" ["Eq","Show"]
<:> addClass "Real" ["Num","Ord"]
<:> addClass "Fractional" ["Num"]
<:> addClass "Integral" ["Real","Enum"]
<:> addClass "RealFract" ["Real","Fractional"]
<:> addClass "Floating" ["Fractional"]
<:> addClass "RealFloat" ["RealFract","Floating"]
<:> addInst (Inst [] [] (IsIn (UnQual "Num") [tInteger]))
ce0 = (addCoreClasses <:> addNumClasses) initialEnv
------------------------------------------------------------------
overlap :: Pred a -> Pred a -> IM a Error Bool
overlap (IsIn c ts1) (IsIn d ts2) =
if c==d
then (do { unifyList ts1 ts2; return True}) `handle` (\ _ -> return False)
else return False
addInst :: Inst a -> EnvTransformer a
addInst (x @ (Inst ks ps (p @ (IsIn i _)))) ce
| not (defined (classes ce i)) = fails ("No class: "++(show i)++", for instance")
| otherwise = do { Inst _ _ p' <- fresh x
; qs <- sequence (map getPred its) -- the predicates (without qualifiers)
; lap <- fmap or (sequence (map (overlap p') qs))
; if lap
then fails ("Overlapping instance for: "++(show i)++".")
else return(modify ce i c)
}
where its = insts ce i -- the instances of i
getPred (x @(Inst ks ps q)) = do { Inst _ _ q' <- fresh x; return q' }
c = Class i (super ce i) (x:its) -- the new class with additional instance
bySuper :: ClassEnv a -> Pred a -> [Pred a]
bySuper ce (p @ (IsIn cname ts)) =
p : concat[bySuper ce (IsIn c' ts) | c' <- super ce cname]
lift :: (Type a -> Type b -> IM c Error d) -> Pred a -> Pred b -> IM c Error [d]
lift m (IsIn c1 ts1) (IsIn c2 ts2) =
if (c1==c2) && (length ts1) ==(length ts2)
then sequence (zipWith m ts1 ts2)
else fails "classes do not match"
matchPred :: Pred a -> Pred a -> IM a Error Bool
matchPred x y = fmap and (lift match x y)
byInst :: Pred a -> Inst a -> IM a Error (Maybe [Pred a])
byInst p (x @ (Inst ks ps h)) =
do { Inst _ ps' h' <- fresh x
; b <- matchPred h' p
; if b
then return (Just ps')
else return Nothing
}
reducePred :: ClassEnv a -> Pred a -> IM a Error (Maybe [Pred a])
reducePred ce (p @ (IsIn c ts)) =
let instances = (insts ce c)
first [] = return Nothing
first (i:is) =
do { m <- byInst p i
; case m of
Just ps -> return(Just ps)
Nothing -> first is }
in first instances
anyM p xs = fmap or (sequence (map p xs))
entail :: ClassEnv a -> [Pred a] -> Pred a -> IM a Error Bool
entail ce ps p =
do { let preconditions = (map (bySuper ce) ps) -- all possible preds => by ps
alreadythere = (any (p `elem`) preconditions)
; if alreadythere
then return True
else do { m <- reducePred ce p
; case m of
Nothing -> return False
Just qs -> do { bs <- sequence (map (entail ce ps) qs)
; return (and bs)
} } }
inHnf (IsIn c ts) = all hnf ts
where hnf (TVar _ _) = True
hnf (S(HsTyApp x _)) = hnf x
hnf (S _) = False
hnf (TGen n) = False
toHnf :: ClassEnv a -> Pred a -> IM a Error [Pred a]
toHnf ce p =
if inHnf p
then return [p]
else do { m <- reducePred ce p
; case m of
Nothing -> fails "context reduction"
Just ps -> toHnfs ce ps
}
toHnfs ce ps = fmap concat (mapM (toHnf ce) ps)
simplify :: ClassEnv a -> [Pred a] -> [Pred a] -> [Pred a]
simplify ce rs [] = rs
simplify ce rs (p:ps) = simplify ce (p:(rs \\ qs)) (ps \\ qs)
where qs = bySuper ce p
rs \\ qs = [ r | r <- rs, r `notElem` qs]
numClasses :: [HsName]
numClasses =
map UnQual ["Num","Integral","Floating","Fractional","Real","RealFloat","RealFrac"]
stdClasses :: [HsName]
stdClasses =
map UnQual ["Eq","Ord","Show","Read","Bounded","Enum","Ix","Functor"
,"Monad","MonadPlus"] ++
numClasses
defs :: ClassEnv a -> Ref a -> [Pred a] -> IM a Error [Type a]
defs ce v qs =
if (all (same v) ts) &&
(all (`elem` stdClasses) clnames) &&
(any (`elem` numClasses) clnames)
then fmap concat(sequence (zipWith f (defaults ce) (repeat clnames)))
else return []
where clnames = [ c | (IsIn c t) <- qs ]
ts = [ t | (IsIn c [t]) <- qs ] -- DON"T KNOW if this translates to MPTC
same (n,v) (TVar (m,u) k) = v==u
same v _ = False
f t [] = return []
f t (c:cs) = do { b <- entail ce [] (IsIn c [t])
; if b then do { ts <- f t cs; return(t:ts) }
else f t cs
}
ambig :: ClassEnv a -> [Ref a] -> [Pred a] -> IM a Error [(Ref a,[Pred a],[Type a])]
ambig ce vs ps =
do { psvss <- sequence(map tv ps) -- [[ vars ]]
; let psvs = concat psvss -- [ vars ] all of them in any of the ps
ambigvs = psvs \\ vs -- vars in ps but not in vs
getqs v [] = []
getqs v ((free,p):xs) = if elem v free then p:(getqs v xs) else getqs v xs
f v = let qs = getqs v (zip psvss ps)
in do { ts <- (defs ce v qs)
; ts' <- mapM collapse ts
; return (v,qs,ts') }
; sequence (map f ambigvs)
}
useDefaults :: String -> ClassEnv a -> [Ref a] -> [Pred a] -> IM a Error [Pred a]
useDefaults names ce vs ps =
do { ams <- ambig ce vs ps
-- [(v,ps,ts)] "v" can be resolved to any of the "ts", which then cancels the "ps"
; let tss = [ts | (v,qs,ts) <- ams]
ps' = [p | (v,qs,ts) <- ams, p <- qs]
fix ((n,v),ps,ts) = writeVar v (Just (head ts))
; if any null tss -- if any "v" can't be resolved by some "t" we have to fail
then fails "ambiguity"
else do { cs <- mapM fix ams
; newps <- collapse ((ps \\ ps'))
; return newps -- subtract the cancelled ps
}
}
partitionM p xs = select xs
where select [] = return ([],[])
select (x:xs) =
do { (ys,zs) <- select xs
; b <- p x
; if b then return (x:ys,zs) else return (ys,x:zs)
}
split :: ClassEnv a -> [Ref a] -> [Pred a] -> IM a Error ([Pred a],[Pred a])
split ce fs ps =
do { ps2 <- toHnfs ce ps
; let ps3 = simplify ce [] ps2
; partitionM p ps3
}
where p ps = do { free <- tv ps; return(all (`elem` fs) free) }
reduce :: String -> ClassEnv a -> [Ref a] -> [Ref a] -> [Pred a]
-> IM a Error ([Pred a],[Pred a])
reduce names ce fs gs ps =
do { (ds,rs) <- split ce fs ps
; rs' <- useDefaults names ce (fs ++ gs) rs
; return(ds,rs')
}
----------------------------------------------------------------------------
type NGVars a = [(HsName,Type a)]
emptyNGVars :: NGVars a
emptyNGVars = []
extendNGVars :: HsName -> Type a -> NGVars a -> NGVars a
extendNGVars s t ngvars = (s,t):ngvars
generic :: NGVars a -> Ref a -> IM a Error Bool
generic ngvars (_,v) = do { b <- occursInList v ngvars; return (not b) }
where occursInList v l =
do { bools <- mapM (\ (a,b) -> occursIn v b) l
; return (or bools)
}
-------------------------------------------------------------------------
-- unArrow [p1,p2,p3] (t1 -> t2 -> t3 -> t4) ---> (t4,[(p1,t1),(p2,t2),(p3,t3)])
unArrow :: [HsPat] -> Type a -> IM a Error (Type a,[(HsPat,Type a)])
unArrow ps t = do { t' <- col t; flat ps t' }
where flat (p:ps) (S(HsTyFun dom rng)) =
do { (t,ts) <- (flat ps rng) ; return (t,(p,dom) : ts) }
flat [] t = return (t,[])
flat (p:ps) t = error "Too many arguments to pattern"
patExtTup [] env = return ([],[],[])
patExtTup ((p,t):m) env =
do { (t1,e1,c1) <- patExt p t env
; (ts,e2,cs) <- patExtTup m env
; return(t1:ts,e1++e2,c1 ++ cs)
}
patExtList [] elemtyp env cs = return (tlist elemtyp,[],cs)
patExtList (p:m) elemtyp env cs =
do { (t1,e1,c1) <- patExt p elemtyp env
; (listOfelem,e2,cs) <- patExtList m elemtyp env c1
; return(listOfelem,e1 ++ e2,c1++cs)
}
patExt :: HsPat -> Type a ->TEnv a -> IM a Error (Type a,NGV a,[Pred a])
patExt (Pat p) typ env =
case p of
HsPId(HsVar name) -> return (typ,[(name,typ)],[])
HsPId(HsCon name) ->
case lookTrmOpt env name of
Nothing -> fails $ "Data constructor " ++ (show name) ++ " not defined!!!"
Just (scheme @ (Sch tvars preds typ)) ->
do { newVars <- mapM (\k -> newVar k) tvars
; t' <- inst newVars typ
; ps <- mapM (inst newVars) preds
; return (t',[],ps) }
(HsPLit (HsInt _)) ->
do { nv <- newVar starKind
; cs <- unify nv typ
; return (nv, [], [(num nv)]++cs) }
(HsPLit l) ->
do { let t = litTyp l
; cs <- unify t typ
; return (t,[],cs)
}
(HsPNeg x) -> error "whats this?"
(HsPInfixApp x n y) -> patExt (Pat(HsPApp (getHSName n) [x,y])) typ env
(HsPApp nm ps) ->
do { Sch _ cs1 ctyp <- fresh (lookTrm env nm)
; (t,patTypeList) <- unArrow ps ctyp
; cs2 <- unify t typ
; (ts2,env2,cs3) <- patExtTup patTypeList env
; return (t,env2,cs1 ++ cs2 ++ cs3)
}
(HsPTuple ps) ->
do { ts <- sequence (map (\ x -> (newVar starKind)) ps)
; cs2 <- unify (tTuple ts) typ
; (ts,ngv3,cs3) <- patExtTup (zip ps ts) env
; return (tTuple ts,ngv3,cs2 ++ cs3)
}
(HsPList ps ) ->
do { elemtyp <- newVar starKind
; (listtyp,ngv2,cs) <- patExtList ps elemtyp env []
; cs2 <- unify listtyp (tlist elemtyp)
; cs3 <- unify typ listtyp
; return (listtyp,ngv2,cs ++ cs2++ cs3)
}
(HsPParen x) -> patExt x typ env
(HsPRec n pairs) -> error "not yet"
(HsPRecUpdate nm pairs) -> error "not yet"
(HsPAsPat name x) ->
do { (t,ngv1,cs1) <- patExt x typ env
; return (t,(name,t):ngv1,cs1)
}
(HsPWildCard) -> do { t <- newVar starKind
; cs <- unify typ t
; return (t,[],cs) }
(HsPIrrPat x) -> patExt x typ env
inferPats :: [HsPat] -> NGV a -> TEnv a ->
IM a Error ([Type a],NGV a,TEnv a,[Pred a])
inferPats ps ngvars env =
do { pairs <- sequence (map (\ p -> do { t <- newVar starKind; return (p,t) }) ps)
; (t1,ngv1,cs1) <- patExtTup pairs env
; return (t1,ngv1 ++ ngvars,g ngv1 env,cs1)
} where g [] env = env
g ((v,t):more) env = lambdaExtTCE (g more env) v t
inferPat p ngvars env hint =
do { (t,ngv1,cs1) <- patExt p hint env
; unify t hint
; return (ngv1 ++ ngvars,g ngv1 env,cs1)
} where g [] env = env
g ((v,t):more) env = lambdaExtTCE (g more env) v t
-------------------------------------------------------------
infer :: Genfun a -> NGV a -> TEnv a -> Type a ->
HsExp -> IM a Error (Type a,[Pred a])
infer gensym ngvars env hint (exp @ (Exp e)) =
let check env hint x = infer gensym ngvars env hint x
in
case e of
HsId(HsVar nm) ->
do { Sch _ cs t <- fresh (lookTrm env nm)
; cs2 <- unify t hint
; return (t,cs ++ cs2)
}
HsId(HsCon nm) ->
do { Sch _ cs t <- fresh (lookTrm env nm)
; cs2 <- unify t hint
; return (t,cs++cs2)
}
HsLit (HsInt _) ->
do { nt <- newVar starKind
; unify nt hint
; return (nt, [num nt]) }
HsLit n ->
do { let t = litTyp n
; cs <- unify t hint
; return (t,cs)
}
HsInfixApp x (HsVar f) y -> check env hint (hsApp (hsApp (hsEVar f) x) y)
HsInfixApp x (HsCon f) y -> check env hint (hsApp (hsApp (hsECon f) x) y)
HsApp f x ->
do { xtyp <- newVar starKind
; let ftyp = tArrow xtyp hint
; (_,cs2) <- check env xtyp x
; (_,cs3) <- check env ftyp f
; return (hint,cs2++cs3)
}
HsNegApp x ->
do { (t,cs) <- check env hint x
; return (t,num t : cs)
}
HsLambda ps x ->
do { (ptyps,ngv2,env2,cs) <- inferPats ps ngvars env
; result <- newVar starKind
-- f [t1,t2,t3] r --> (t1 -> t2 -> t3 -> r)
; let f [] rng = rng
f (t:ts) rng = tArrow t (f ts rng)
ans = f ptyps result
; (_,cs2) <- infer gensym ngv2 env2 result x
; cs3 <- unify ans hint
; return (ans,cs ++ cs2 ++ cs3)
}
HsLet ds e ->
do { (ngv2,env2,cs2) <- inferDs gensym ngvars env ds
; (etyp,cs3) <- infer gensym ngv2 env2 hint e
; return (etyp,cs2++cs3)
}
HsIf x y z ->
do { t <- newVar starKind
; (_,cs1) <- check env tBool x
; (_,cs2) <- check env t y
; (_,cs3) <- check env t z
; unify t hint
; return (t,cs1 ++ cs2 ++ cs3)
}
{- HsCase e alts ->
do { argtyp <- newVar starKind
; (ptyp,cs1) <- check env argtyp e
; csAll <- mapM (inferAlt gensym ngvars env ptyp hint) alts
; return (hint, cs1 ++ concat csAll)
}
-}
HsDo stmt ->
do { mtyp <- newVar (arrowKind starKind starKind)
; let m x = (S(HsTyApp mtyp x))
; a <- newVar starKind
; cs2 <- unify hint (m a)
; cs3 <- inferStmt gensym ngvars env mtyp (m a) False stmt
; return (hint,(monad mtyp) : cs2 ++ cs3)
}
HsTuple xs ->
do { pairs <- sequence (map (\ x -> do { t <- newVar starKind; return (t,x) }) xs)
; let tupletyp = tTuple(map fst pairs)
; cs1 <- unify hint tupletyp
; ts <- mapM (uncurry (check env)) pairs
; return (hint,foldr (\ (t,c) cs -> c ++ cs) cs1 ts)
}
HsList xs ->
do { elemtyp <- newVar starKind
; cs1 <- unify hint (tlist elemtyp)
; pairs <- mapM (check env elemtyp) xs
; return (hint,foldr (\ (t,c) cs -> c ++ cs) cs1 pairs)
}
HsParen x -> check env hint x
HsRightSection op arg -> -- i.e. (+ 3) }
do { ltyp <- newVar starKind
; rtyp <- newVar starKind
; anstyp <- newVar starKind
; cs1 <- unify (tArrow ltyp anstyp) hint
; (_,cs2) <- check env (tArrow ltyp (tArrow rtyp anstyp)) (hsId op)
; (_,cs3) <- check env rtyp arg
; return (hint,cs1 ++ cs2 ++ cs3)
}
HsLeftSection arg op -> -- i.e. (3 +)
do { ltyp <- newVar starKind
; rtyp <- newVar starKind
; anstyp <- newVar starKind
; cs1 <- unify (tArrow rtyp anstyp) hint
; (_,cs2) <- check env (tArrow ltyp (tArrow rtyp anstyp)) (hsId op)
; (_,cs3) <- check env ltyp arg
; return (hint,cs1 ++ cs2 ++ cs3)
}
HsRecConstr name fields -> error "not yet"
HsRecUpdate arg fields -> error "not yet"
HsEnumFrom x -> -- [x ..] :: Enum a => [a]
do { a <- newVar starKind
; cs1 <- unify hint (tlist a)
; (_,cs2) <- check env a x
; return (hint,(enum a) : cs1 ++ cs2)
}
HsEnumFromTo x y -> -- [x .. y] :: Enum a => a -> a -> [a]
do { a <- newVar starKind
; cs0 <- unify hint (tlist a)
; (_,cs1) <- check env a x
; (_,cs2) <- check env a y
; return (hint,(enum a) : cs0 ++ cs1 ++ cs2)
}
HsEnumFromThen x y -> -- [x, y ..] : Enum a => a -> a -> [a]
do { a <- newVar starKind
; cs0 <- unify hint (tlist a)
; (_,cs1) <- check env a x
; (_,cs2) <- check env a y
; return (hint,(enum a) : cs0 ++ cs1 ++ cs2)
}
HsEnumFromThenTo x y z -> -- [x,y .. z] :: Enum a => a -> a -> a -> [a]
do { a <- newVar starKind
; cs0 <- unify hint (tlist a)
; (_,cs1) <- check env a x
; (_,cs2) <- check env a y
; (_,cs3) <- check env a z
; return (hint,(enum a) : cs0 ++ cs1 ++ cs2 ++ cs3)
}
HsListComp stmt ->
do { let mtyp = tlistCon
; let m x = (S(HsTyApp mtyp x))
; a <- newVar starKind
; cs2 <- unify hint (m a)
; cs3 <- inferStmt gensym ngvars env mtyp a True stmt
; return (hint,cs2 ++ cs3)
}
HsExpTypeSig loc e qt ->
do { Sch _ cs1 typ <- hsQual2freshSch qt
; cs2 <- unify typ hint
; (_,cs3) <- check env typ e
; return (typ,cs1 ++ cs2 ++ cs3)
}
HsAsPat nm e -> error "pattern only"
HsWildCard -> error "pattern only"
HsIrrPat e -> error "pattern only"
{-
HsMetaBracket e -> -- MetaHUGS extension <<| exp |>
do { a <- newVar starKind
; cs1 <- unify hint (tcode a)
; (_,cs2) <- check env a e
; return (hint,cs1 ++ cs2)
}
HsMetaEscape e -> -- MetaHUGS extansion ^exp
do { (_,cs1) <- check env (tcode hint) e
; return (hint,cs1)
}
-}
isValueDecl (Dec d) =
case d of
HsPatBind _ _ _ _ -> True
HsFunBind _ _ -> True
_ -> False
isTypeDecl (Dec d) =
case d of
HsTypeDecl _ _ _ -> True
HsDataDecl _ _ _ _ _ -> True
HsPrimitiveTypeDecl _ _ _ -> True
_ -> False
isClassInstDecl (Dec d) =
case d of
HsClassDecl _ _ _ _ -> True
HsInstDecl _ _ _ _ -> True
HsDefaultDecl _ _ -> True
_ -> False
--------------------------------------------------------------------
-- InferDs, first breaks the [HsDecl] into strongly connected binding
-- groups, then types each set separately using inferBG
inferDs :: Genfun a -> NGV a -> TEnv a -> [HsDecl] -> IM a Error (NGV a,TEnv a, Constrs a)
inferDs gensym ngv env ds =
let valueDs = filter isValueDecl ds
typeDs = filter isTypeDecl ds
(groups,_) = bindingGroups valueDs
(typeGroups,cyclicSynonyms) = bindingGroups typeDs
f (ngv,env,cs) ds = do { (n,e,c) <- inferBG gensym ngv env ds; return(n,e,c++cs)}
g (env) ds = do { env' <- inferDataTypes gensym env ds
; return env' }
in do { if cyclicSynonyms then fails "Cyclic type synonyms" else return ()
; e <- (foldM g env typeGroups)
; foldM f (ngv,e,[]) groups
}
------------------------------------------------------------------
-- Section 4.5.2 of the Haskell report states that all constraints
-- resulting from typing a single binding group are collected together
-- to form the context of the type for each name bound in the binding
-- group. Thus given a binding group we should construct a delta env
-- with a binding for each name, and a common set of contraints.
pr2 s x = do { x' <- x; pr s x'}
dataTypeName sloc (Typ t) =
case t of
HsTyVar n -> return n
HsTyApp a b -> dataTypeName sloc a
HsTyCon n -> return n
_ -> fails $ show sloc ++ "Error in type pattern: ill formed. "
dataTypeArgs sloc (Typ t) =
case t of
HsTyVar n -> return [n]
HsTyApp a b -> dataTypeArgs sloc b
HsTyCon _ -> return []
_ -> fails $ show sloc ++ "Error in type pattern: ill formed. "
inferDataTypes gensym env [] = return env
inferDataTypes gensym env ds =
do { let (freef, envf) = Scope.freeD ds
freeVars = freef []
; vs <- mapM (\_ -> newVarK Sort) freeVars
; pr "In binding group; type constructors" freeVars
; env' <- return $ foldr (.) id (zipWith extTconstr freeVars vs) env0
; r <- mapM (inferDataType gensym env') ds
; return (foldr (+|+) env r )
}
-- data (Q x, P y) => T x y = C x y | D [y] x
-- tpat = T x y
-- ctxt = [Q x,P y]
-- C :: Sch [*,*] (Q #0,P #1) (#0 -> #1 -> T #0 #1)
-- D :: Sch [*,*] (Q #1,P #0) ([#0] -> #1 -> T #1 #0)
inferDataType gensym env (Dec d) =
case d of
HsDataDecl sloc ctxt (tcon:targs) consdecls derivs ->
do { pr "In Infer Data with " ((show tcon)++" -- "++(show targs))
; let { tpat = foldl hsTyApp tcon targs }
; pairs <- mapM (\ nm -> do { k <- newVarK Sort; return(nm,k)})
(map getTyName targs)
; pr "pairs" pairs
; envd <- return $ (foldr (.) id (map (\ (nm,k) -> extTconstr nm k ) pairs)) env
; let kindCheck k x = (pr "in kindcheck " (show x)) >> inferK (getKindEnv envd) k x
constrs (HsConDecl sloc consname btypes) =
do { let types = (map unBang btypes)
; pr "constr is " ((show consname) ++" with "++(show (length types)))
; pr ("constr arity for" ++ (show consname)++": ") (length types)
; mapM (kindCheck star) types
; return (consname, foldr hsTyFun tpat types)
}
; kindCheck star tpat
; mapM_ (kindCheck predicate) ctxt
; delta <- mapM constrs consdecls
; pr "delta" delta
; let delta2 = foldr (.) id (map (\ (nm,sch) -> extTrm nm sch) (map (hsType2Scheme (lookTconstr envd) ctxt) delta)) env0
; return (delta2 +|+ env)
}
HsTypeDecl sloc (constr : args) body -> return(env)
other -> error "not implemented yet"
hsType2Scheme kenvd ps (nm,t) =
let free (Typ (HsTyVar nm)) ans = union [nm] ans
free (Typ t) ans = accT free t ans
vars = free t []
sigma = zipWith (\ n nm -> (nm,TGen n)) [0..] vars
t' = rebuild sigma t
ps' = map (type2pred (rebuild sigma)) ps
in (nm,Sch (map kenvd vars) ps' t')
unBang (HsBangedType a) = a
unBang (HsUnBangedType a) =a
------------------------------------------------------------------------------
extBGmono :: [HsDecl] -> IM a Error (NGV a,TEnv a,Constrs a,[(Type a,HsDecl)])
extBGmono ds = foldM extB ([],env0,[],[]) ds
where extB (ngvars,env,cs,tds) (dec @ (Dec d)) =
case d of
HsPatBind s pat e ds ->
do { ptype <- newVar starKind
; (ngv2,env2,cs2) <- inferPat pat ngvars env ptype
; return(ngv2,env2,cs2++cs,(ptype,dec):tds)
}
HsFunBind s matches ->
do { let getname ((HsMatch sloc name ps rhs ds):_) = name
name = getname matches
; ftype <- newVar starKind
; let env2 = lambdaExtTCE env name ftype
; return((name,ftype):ngvars,env2,cs,(ftype,dec):tds)
}
inferBG :: Genfun a -> NGV a -> TEnv a -> [HsDecl] -> IM a Error (NGV a,TEnv a, Constrs a)
inferBG gensym ngv env [] = return(ngv,env,[])
inferBG gensym ngv env ds =
do { (ngvDelta,envDelta,cs,tds) <- extBGmono ds
; let names = showl (map show (map fst ngvDelta)) ""
; cs2 <- foldM (inferEach gensym (ngvDelta++ngv) (envDelta +|+ env)) cs tds
; ps' <- sequence (map collapse cs2)
; ts' <- mapM collapse (map snd ( ngvDelta))
; fs <- fmap concat (sequence (map (\ (name,t) -> tv t) ngv))
; vss <- mapM tv ts'
; let inEveryT = foldr1 intersect vss
gs = (foldr List.union [] vss) \\ fs -- In infered types, but not env
-- at this point ps' holds all the constraints resulting from typing
-- the whole binding group. envDelta holds an env with monomorphic types for
-- just the names bound by the binding group, and ngvDelta pairs just those
-- names with their types.
; ce <- ce0
; (deferred,retained) <- reduce names ce fs inEveryT ps'
; let generic x = return True --(x `elem` gs)
genSch (name,t) = do { sch <- quant generic (retained :=> t)
; return (name,sch) }
getngv (x,Sch ks ps t) = (x,t)
; d2 <- mapM genSch ngvDelta
; delta2 <- return $ (foldr (.) id (map (uncurry extTrm) d2) (E [] [] []))
; return (map getngv (getTermEnv delta2) ++ ngv,delta2 +|+ env,deferred)
}
quant :: (Ptr2 a -> IM a Error Bool) -> Qual a (Type a) -> IM a Error (Scheme a)
quant generic (x @ (preds :=> typ)) =
do { free <- newRef []
; z <- col typ
; let genPred (IsIn c ts) =
do {ts' <- mapM (gen generic free) ts
; return (IsIn c ts') }
; typ' <- gen generic free typ
; preds' <- mapM genPred preds
; theta <- readVar free
; x <- col typ'
; return $ Sch (map (\ (t,_,k) -> k) (reverse theta)) preds' x
}
inferEach gensym ngv env cs (t,Dec d) =
do {
case d of
HsPatBind s pat rhs ds ->
do { (ngv1,env1,cs1) <- inferDs gensym ngv env ds
; cs2 <- inferRhs ngv1 env1 t rhs
; return(cs1++cs2)
}
HsFunBind s matches -> foldM (infermatch t) cs matches
other -> error "Only PatBind and FunBind allowed in inferEach"
}
where inferRhs ngv env hint (HsGuard gs) = foldM (inferGuard ngv env hint) cs gs
inferRhs ngv env hint (HsBody e) =
do { (etyp,cs2) <- infer gensym ngv env hint e
; return(cs2++cs) }
inferGuard ngv env hint cs (srloc,guard,body) =
do { (_,cs2) <- infer gensym ngv env tBool guard
; (_,cs3) <- infer gensym ngv env hint body
; return (cs3++cs2++cs) }
infermatch hint cs (HsMatch sloc name ps rhs ds) =
do { (ts,ngv1,env1,cs1) <- inferPats ps ngv env
; (ngv2,env2,cs2) <- inferDs gensym ngv1 env1 ds
; range <- newVar starKind
; cs3 <- unify hint (foldr tArrow range ts)
; cs4 <- inferRhs ngv2 env2 range rhs
; return(cs4++cs3++cs2++cs1++cs)
}
------------------------------------------------------------------
----------------------------------------------------------------------------------
-- inferStmt is used to infer the type of both Do stmts and list comprehensions
-- [ A | p <- e ; f ] has the same structure as (do { P <- e; f ; A })
-- but the type rules differ slightly for both "A" and "f". We've parameterized
-- inferStmt to handle this
inferStmt :: Genfun a -> NGV a -> TEnv a -> Type a -> Type a -> Bool ->
HsStmtR -> IM a Error [Pred a]
inferStmt gensym ngvars env mtyp lasttyp isListComp stmt =
let m x = (S(HsTyApp mtyp x)) in
case stmt of
HsGenerator p e next -> -- p <- e ; next
do { ptyp <- newVar starKind
; (_,cs2) <- infer gensym ngvars env (m ptyp) e
; (ngv2,env2,cs3) <- inferPat p ngvars env ptyp
; cs4 <- inferStmt gensym ngv2 env2 mtyp lasttyp isListComp next
; return (cs2 ++ cs3 ++ cs4)
}
HsQualifier e next -> -- e ; next
do { typ <- if isListComp then return tBool else fmap m (newVar starKind)
; (_,cs2) <- infer gensym ngvars env typ e
; return cs2
}
HsLetStmt ds next -> -- let ds ; next
do { (ngv2,env2,cs2) <- inferDs gensym ngvars env ds
; cs3 <- inferStmt gensym ngv2 env2 mtyp lasttyp isListComp next
; return (cs2 ++ cs3)
}
HsLast e -> do { (_,cs) <- infer gensym ngvars env lasttyp e; return cs }
---------------------------------------------------------------------
-- The Parser produces HsQualType data structures, we must turn these
-- into Scheme data structures, while doing to we should kind-check
-- all the type information.
hstype2Type :: HsType -> Type a
hstype2Type (Typ x) = S(mapT hstype2Type x)
-- Takes [ HsType ] representing qualifying predicates and a (HsType)
-- and produces fresh Scheme for that annotation. used like
-- ( x :: (P,Q) => t )
hsQual2freshSch:: HsTypeId HsType [HsType] -> IM a Error (Scheme a)
hsQual2freshSch x = f (preds x) (types x)
where preds (TypeQual ps x) = ps
preds (TypeUnQual x) = []
types (TypeQual ps x) = x
types (TypeUnQual x) = x
f preds x =
do { let names = freeNames [] x
; let g x = do { v <- newVar starKind; return(x,v) }
; sub <- mapM g names
; let x' = rebuild sub x
preds' = map (type2pred (rebuild sub)) preds
; return(Sch [] preds' x')
}
-----------------------------------------------------------------
-- Helper functions for turning HsType into (Type a) and (Pred a)
type2pred :: (HsType -> Type a) -> HsType -> Pred a
type2pred g (Typ(HsTyApp (Typ(HsTyVar f)) x)) = IsIn f [g x]
type2pred g (Typ(HsTyApp (Typ(HsTyCon f)) x)) = IsIn f [g x]
type2pred g (Typ(HsTyApp f x)) = IsIn h ((g x): ys)
where IsIn h ys = type2pred g f
type2pred g x = error ("type2pred dies: " ++(show x))
freeNames :: [HsName] -> HsType -> [HsName]
freeNames bound (Typ x) =
case x of
HsTyVar n -> if elem n bound then [] else [n]
x -> accT f x []
where f x ans = union (freeNames bound x) ans
rebuild :: [(HsName,Type a)] -> HsType -> Type a
rebuild sub (Typ x) =
case x of
HsTyVar n -> case find (\ (x,y) -> x==n) sub of
Just(_,v) -> v
Nothing -> error "unknown type variable in signature"
x -> S(mapT (rebuild sub) x)
look ((y, e):ys) x = if x == y then e else look ys x
look [] x = error "empty list in look"
--------- Show Instances ----------------------------------
instance Show(Type a) where
showsPrec n (S x) = shows x
showsPrec n (TGen m) = showString "%" . shows m
showsPrec n (TVar (m,r) k) = showString ("("++(show m)++",?)")
instance Show(Pred a) where
showsPrec m (IsIn n ts) =
showString "(" . showsPrec m n . showString " " . shl ts . showString ")"
shl [] ss = ss
shl [x] ss = (showsPrec 0 x . showString " ") ss
shl (x:xs) ss = showsPrec 0 x ( showString ", " (shl xs ss))
showl [] ss = ss
showl [x] ss = showString (x++" ") ss
showl (x:xs) ss = showString (x++", ") (showl xs ss)
instance Show (Scheme a) where
--show (Sch x p t) = "(all " ++ (showString (showList (nums x)"") "") ++"." ++ (show p) ++ " => " ++ (show t) ++ ")"
showsPrec n (Sch x p t) =
showString "(all " . showl (nums x) . showString "." .
showsPrec n p . showString " => " . showsPrec n t . showString ")"
where nums xs = ["%"++(show n) | n <- [0 .. (length xs - 1)]]
toVis map (S x) = VS(map (toVis map) x)
toVis map (TGen n) = VN("v" ++ (show n))
toVis map (TVar _ _) = VN "?"
visKind = toVis mapK
visType = toVis mapT
data Vis s
= VS (s (Vis s))
| VN String
instance Show (Vis T) where
show (VN gen) = gen
show (VS tstruct) = show tstruct
instance Show (Vis K) where
show (VN gen) = gen
show (VS tstruct) = show tstruct
instance Show (Kind a) where
show t = show(visKind t)
---------------------------------------------
a:b:c:d:_ = [ TGen i | i <- [0..] ]
simpleEnv =
[(UnQual "+",Sch[star] [num a] (tArrow a (tArrow a a)))
,(UnQual "*",Sch[star] [num a] (tArrow a (tArrow a a)))
,(UnQual "-",Sch[star] [num a] (tArrow a (tArrow a a)))
,(UnQual ":",Sch[star,star] [] (tArrow a (tArrow (tlist a) (tlist a))))
,(UnQual "True",Sch[] [] tBool)
,(UnQual "False",Sch[] [] tBool)
]
---------------------------------------------------------------
-- a declaration like
-- type T a b = (a,b -> Int)
-- is stored in an environment with type [(HsName,([HsName],HsType))]
-- e.g. (T,([a,b],(a,b -> Int))) :: more
-- expandType walks over a type. At every application it tests if that application
-- matches some fully applied instance of (T a b). Suppose it does and looks like
-- (T Int String). Then we build a substitution [(a,Int),(b,String)] and apply
-- it to (a,b -> Int). If it doesn't, we just recursively expand the sub-types.
expandType :: [(HsName,([HsName],HsType))] -> HsType -> Type a
expandType env (x @ (Typ(HsTyApp f a))) =
case matchApp env x of
Nothing -> S(HsTyApp (expandType env f) (expandType env a))
expandType env (Typ x) = S(mapT (expandType env) x)
matchApp :: [(HsName,([HsName],HsType))] -> HsType -> Maybe (Type a)
matchApp env t = walkSpine t []
where walkSpine (Typ(HsTyApp x y)) ts = walkSpine x (expandType env y : ts)
walkSpine (Typ(HsTyCon nm)) ts = applySub nm env ts
walkSpine _ ts = Nothing
applySub nm env ts =
case lookup nm env of
Nothing -> Nothing
Just(vs,t) -> if length vs == length ts
then Just(rebuild (zip vs ts) t)
else Nothing
--------------------------------------------------------
class TCEnv env where
extTconstr :: HsName -> GT K Sort (STRef a) -> env a -> env a
extTySyn :: HsName -> [HsName] -> Type a -> env a -> env a
extTrm :: HsName -> Scheme a -> env a -> env a
lookTconstr :: env a -> HsName -> GT K Sort (STRef a)
lookTySyn :: env a -> HsName -> ([HsName],Type a)
lookTrm :: env a -> HsName -> Scheme a
lookTconstrOpt :: env a -> HsName -> Maybe (GT K Sort (STRef a))
lookTySynOpt :: env a -> HsName -> Maybe ([HsName],Type a)
lookTrmOpt :: env a -> HsName -> Maybe (Scheme a)
getKindEnv :: env a -> [(HsName, GT K Sort (STRef a))]
getTermEnv :: env a -> [(HsName, Scheme a)]
env0 :: env a
data TEnv a = E { typeSyns :: [(HsName, ([HsName], Type a))]
, termEnv :: [(HsName, Scheme a)]
, kindEnv :: [(HsName,GT K Sort (STRef a))] }
deriving Show
(E a b c) +|+ (E d e f) = E (a++d) (b++e) (c++f)
instance TCEnv TEnv where
env0 = E [] [] []
extTconstr n t env = env { kindEnv = (n,t) : kindEnv env }
extTySyn n ns t env = env { typeSyns = (n, (ns,t)) : typeSyns env }
extTrm n sch env = env { termEnv = (n,sch) : termEnv env}
lookTconstr env n = case lookup n (kindEnv env) of
Just x -> x
Nothing -> error $ "Not found: "++(show n)
lookTySyn env n = case lookup n (typeSyns env) of
Just x -> x
Nothing -> error $ "Not found: type synonym " ++ (show n)
lookTrm env n = case lookup n (termEnv env) of
Just x -> x
Nothing -> error $ "Not found: no type for " ++ (show n)
getKindEnv env = kindEnv env
getTermEnv env = termEnv env
---------------------------------------------------------