c0c2380bced8159ff0297ece14eba948bd236471Christian Maeder{- |

934473566cf3a8e4044ed10e408b4c44079684b1Christian MaederModule : $Header$

aa4679922a8363b4e494079f53aaf4f64554aae0Christian MaederCopyright : (c) Christian Maeder and Uni Bremen 2003-2005

cf7e0d6750e408ddb47545d6b8349a70cf0b47afChristian MaederLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt

aa4679922a8363b4e494079f53aaf4f64554aae0Christian Maeder

aa4679922a8363b4e494079f53aaf4f64554aae0Christian MaederMaintainer : maeder@tzi.de

934473566cf3a8e4044ed10e408b4c44079684b1Christian MaederStability : experimental

1d581e55c7ec020a445684310394c3a5fc056e96Christian MaederPortability : portable

aa4679922a8363b4e494079f53aaf4f64554aae0Christian Maeder

aa4679922a8363b4e494079f53aaf4f64554aae0Christian Maederconstraint resolution

f3a94a197960e548ecd6520bb768cb0d547457bbChristian Maeder

f3a94a197960e548ecd6520bb768cb0d547457bbChristian Maeder-}

b10d6cef708b7a659f2d3b367e8e0db0d03ae3f5Till Mossakowski

b10d6cef708b7a659f2d3b367e8e0db0d03ae3f5Till Mossakowskimodule HasCASL.Constrain where

b10d6cef708b7a659f2d3b367e8e0db0d03ae3f5Till Mossakowski

b10d6cef708b7a659f2d3b367e8e0db0d03ae3f5Till Mossakowskiimport HasCASL.Unify

b10d6cef708b7a659f2d3b367e8e0db0d03ae3f5Till Mossakowskiimport HasCASL.As

b10d6cef708b7a659f2d3b367e8e0db0d03ae3f5Till Mossakowskiimport HasCASL.AsUtils

7ff59aa438d7a210789cad2c2c745bc9967eff82Till Mossakowskiimport HasCASL.Le

7ff59aa438d7a210789cad2c2c745bc9967eff82Till Mossakowskiimport HasCASL.TypeAna

7ff59aa438d7a210789cad2c2c745bc9967eff82Till Mossakowskiimport HasCASL.ClassAna

7ff59aa438d7a210789cad2c2c745bc9967eff82Till Mossakowski

7ff59aa438d7a210789cad2c2c745bc9967eff82Till Mossakowskiimport qualified Common.Lib.Set as Set

7ff59aa438d7a210789cad2c2c745bc9967eff82Till Mossakowskiimport qualified Common.Lib.Map as Map

7ff59aa438d7a210789cad2c2c745bc9967eff82Till Mossakowskiimport qualified Common.Lib.Rel as Rel

7ff59aa438d7a210789cad2c2c745bc9967eff82Till Mossakowskiimport Common.Lib.State

7ff59aa438d7a210789cad2c2c745bc9967eff82Till Mossakowskiimport Common.PrettyPrint

7ff59aa438d7a210789cad2c2c745bc9967eff82Till Mossakowskiimport Common.Lib.Pretty

b10d6cef708b7a659f2d3b367e8e0db0d03ae3f5Till Mossakowskiimport Common.Keywords

b10d6cef708b7a659f2d3b367e8e0db0d03ae3f5Till Mossakowskiimport Common.Id

1d581e55c7ec020a445684310394c3a5fc056e96Christian Maederimport Common.Result

bf76f4fcf07abaebea587df8135de8356c26a363Till Mossakowski

b10d6cef708b7a659f2d3b367e8e0db0d03ae3f5Till Mossakowskiimport Data.List

b10d6cef708b7a659f2d3b367e8e0db0d03ae3f5Till Mossakowskiimport Data.Maybe

b10d6cef708b7a659f2d3b367e8e0db0d03ae3f5Till Mossakowski

b10d6cef708b7a659f2d3b367e8e0db0d03ae3f5Till Mossakowskidata Constrain = Kinding Type Kind

b10d6cef708b7a659f2d3b367e8e0db0d03ae3f5Till Mossakowski | Subtyping Type Type

b10d6cef708b7a659f2d3b367e8e0db0d03ae3f5Till Mossakowski deriving (Eq, Ord, Show)

aa4679922a8363b4e494079f53aaf4f64554aae0Christian Maeder

aa4679922a8363b4e494079f53aaf4f64554aae0Christian Maederinstance PrettyPrint Constrain where

aa4679922a8363b4e494079f53aaf4f64554aae0Christian Maeder printText0 ga c = case c of

aa4679922a8363b4e494079f53aaf4f64554aae0Christian Maeder Kinding ty k -> printText0 ga ty <+> colon

aa4679922a8363b4e494079f53aaf4f64554aae0Christian Maeder <+> printText0 ga k

aa4679922a8363b4e494079f53aaf4f64554aae0Christian Maeder Subtyping t1 t2 -> printText0 ga t1 <+> text lessS

aa4679922a8363b4e494079f53aaf4f64554aae0Christian Maeder <+> printText0 ga t2

b10d6cef708b7a659f2d3b367e8e0db0d03ae3f5Till Mossakowski

1549f3abf73c1122acff724f718b615c82fa3648Till Mossakowskiinstance PosItem Constrain where

934473566cf3a8e4044ed10e408b4c44079684b1Christian Maeder get_pos c = case c of

b10d6cef708b7a659f2d3b367e8e0db0d03ae3f5Till Mossakowski Kinding ty _ -> get_pos ty

cf7e0d6750e408ddb47545d6b8349a70cf0b47afChristian Maeder Subtyping t1 t2 -> get_pos t1 ++ get_pos t2

cf7e0d6750e408ddb47545d6b8349a70cf0b47afChristian Maeder

cf7e0d6750e408ddb47545d6b8349a70cf0b47afChristian Maedertype Constraints = Set.Set Constrain

96f0ef61a405144ff30a9d77963881dc32113750Klaus Luettich

f2d72b2254513ef810b0951f0b13a62c2921cb4dTill MossakowskinoC :: Constraints

18a4d5cb6828f080db9c5f9551785c5151027271Christian MaedernoC = Set.empty

b10d6cef708b7a659f2d3b367e8e0db0d03ae3f5Till Mossakowski

6d9f68d2b5fafea0b5e0fc59a1d557174e032c02Christian MaederjoinC :: Constraints -> Constraints -> Constraints

b565cd55a13dbccc4e66c344316da525c961e4caTill MossakowskijoinC = Set.union

f04e8f3ff56405901be968fd4c6e9769239f1a9bKlaus Luettich

4336edf6ada5b582667322f91e705b4366798953Dominik LueckeinsertC :: Constrain -> Constraints -> Constraints

aa4679922a8363b4e494079f53aaf4f64554aae0Christian MaederinsertC c = case c of

aa4679922a8363b4e494079f53aaf4f64554aae0Christian Maeder Subtyping t1 t2 -> if t1 == t2 then id else Set.insert c

bb4d3b6e93db1495f02de46aff5076862e30517bChristian Maeder _ -> Set.insert c

aa4679922a8363b4e494079f53aaf4f64554aae0Christian Maeder

c64d33a7fbeae730cbe65193fe3cc24e7aa1ddd6Christian MaedersubstC :: Subst -> Constraints -> Constraints

b565cd55a13dbccc4e66c344316da525c961e4caTill MossakowskisubstC s = Set.fold (insertC . ( \ c -> case c of

b565cd55a13dbccc4e66c344316da525c961e4caTill Mossakowski Kinding ty k -> Kinding (subst s ty) k

fe0e5e7c16ae2d6172cc583e0a9b8a54fce0dd55Christian Maeder Subtyping t1 t2 -> Subtyping (subst s t1) $ subst s t2)) noC

4b3a2c618e849a0ad4fb18eba58d24f37c57272eTill Mossakowski

51e836611726885f6d2719d959ed1b51f8fd06f4Klaus Luettichsimplify :: TypeEnv -> Constraints -> ([Diagnosis], Constraints)

c4e3cade80a00690374e97f050fb5ade9d292850Till Mossakowskisimplify te rs =

b3dca469a9e267d6d71acfdeca7bf284d0581dc7Till Mossakowski if Set.null rs then ([], noC)

cf7e0d6750e408ddb47545d6b8349a70cf0b47afChristian Maeder else let (r, rt) = Set.deleteFindMin rs

c64d33a7fbeae730cbe65193fe3cc24e7aa1ddd6Christian Maeder Result ds m = entail te r

c0c2380bced8159ff0297ece14eba948bd236471Christian Maeder (es, cs) = simplify te rt

c0c2380bced8159ff0297ece14eba948bd236471Christian Maeder in (ds ++ es, case m of

410307167d116ddab45e02698eac31043619ed05Christian Maeder Just _ -> cs

58b429c45eeb9eea394b6efb521e7489feef75a6Christian Maeder Nothing -> insertC r cs)

d000408bc0e4519f75e60555c69d5a0d1a1dd67cKlaus Luettich

ad270004874ce1d0697fb30d7309f180553bb315Christian Maederentail :: Monad m => TypeEnv -> Constrain -> m ()

d000408bc0e4519f75e60555c69d5a0d1a1dd67cKlaus Luettichentail te p =

b10d6cef708b7a659f2d3b367e8e0db0d03ae3f5Till Mossakowski do is <- byInst te p

bf76f4fcf07abaebea587df8135de8356c26a363Till Mossakowski mapM_ (entail te) $ Set.toList is

bf76f4fcf07abaebea587df8135de8356c26a363Till Mossakowski

b10d6cef708b7a659f2d3b367e8e0db0d03ae3f5Till MossakowskibyInst :: Monad m => TypeEnv -> Constrain -> m Constraints

aa4679922a8363b4e494079f53aaf4f64554aae0Christian MaederbyInst te c = let cm = classMap te in case c of

b10d6cef708b7a659f2d3b367e8e0db0d03ae3f5Till Mossakowski Kinding ty k -> case ty of

aa4679922a8363b4e494079f53aaf4f64554aae0Christian Maeder ExpandedType _ t -> byInst te $ Kinding t k

aa4679922a8363b4e494079f53aaf4f64554aae0Christian Maeder _ -> if k == star then return noC else case k of

b10d6cef708b7a659f2d3b367e8e0db0d03ae3f5Till Mossakowski ExtKind ek _ _ -> byInst te (Kinding ty ek)

aa4679922a8363b4e494079f53aaf4f64554aae0Christian Maeder ClassKind _ -> let (topTy, args) = getTypeAppl ty in

aa4679922a8363b4e494079f53aaf4f64554aae0Christian Maeder case topTy of

aa4679922a8363b4e494079f53aaf4f64554aae0Christian Maeder TypeName i _ _ -> let Result _ mk = getIdKind te i in

aa4679922a8363b4e494079f53aaf4f64554aae0Christian Maeder case mk of

aa4679922a8363b4e494079f53aaf4f64554aae0Christian Maeder Nothing -> fail $ "remaining variable '"

aa4679922a8363b4e494079f53aaf4f64554aae0Christian Maeder ++ showPretty i "'"

aa4679922a8363b4e494079f53aaf4f64554aae0Christian Maeder Just ((_, ks), _) -> do

b10d6cef708b7a659f2d3b367e8e0db0d03ae3f5Till Mossakowski if null args then

2b565fe5cfb9f99857fd25b52304758d8544e266Mihai Codescu if any ( \ j -> lesserKind cm j k) ks

2b565fe5cfb9f99857fd25b52304758d8544e266Mihai Codescu then return noC

2b565fe5cfb9f99857fd25b52304758d8544e266Mihai Codescu else fail $ "constrain '" ++

2b565fe5cfb9f99857fd25b52304758d8544e266Mihai Codescu showPretty c "' is unprovable"

2b565fe5cfb9f99857fd25b52304758d8544e266Mihai Codescu ++ "\n known kinds are: " ++

2b565fe5cfb9f99857fd25b52304758d8544e266Mihai Codescu showPretty ks ""

bf76f4fcf07abaebea587df8135de8356c26a363Till Mossakowski else do

aa4679922a8363b4e494079f53aaf4f64554aae0Christian Maeder let kas = concatMap ( \ j ->

aa4679922a8363b4e494079f53aaf4f64554aae0Christian Maeder getKindAppl cm j args) ks

aa4679922a8363b4e494079f53aaf4f64554aae0Christian Maeder newKs <- dom cm k kas

aa4679922a8363b4e494079f53aaf4f64554aae0Christian Maeder return $ Set.fromList $ zipWith Kinding args newKs

c64d33a7fbeae730cbe65193fe3cc24e7aa1ddd6Christian Maeder _ -> error "byInst: unexpected Type"

aa4679922a8363b4e494079f53aaf4f64554aae0Christian Maeder _ -> error "byInst: unexpected Kind"

aa4679922a8363b4e494079f53aaf4f64554aae0Christian Maeder Subtyping t1 t2 -> if lesserType te t1 t2 then return noC

aa4679922a8363b4e494079f53aaf4f64554aae0Christian Maeder else fail ("unable to prove: " ++ showPretty t1 " < "

aa4679922a8363b4e494079f53aaf4f64554aae0Christian Maeder ++ showPretty t2 "")

c64d33a7fbeae730cbe65193fe3cc24e7aa1ddd6Christian Maeder

aa4679922a8363b4e494079f53aaf4f64554aae0Christian MaedermaxKind :: ClassMap -> Kind -> Kind -> Maybe Kind

aa4679922a8363b4e494079f53aaf4f64554aae0Christian MaedermaxKind cm k1 k2 = if lesserKind cm k1 k2 then Just k1 else

aa4679922a8363b4e494079f53aaf4f64554aae0Christian Maeder if lesserKind cm k2 k1 then Just k2 else Nothing

bf76f4fcf07abaebea587df8135de8356c26a363Till Mossakowski

6e29f2565572024b963af2f6d486b567307dc770Till MossakowskimaxKinds :: ClassMap -> [Kind] -> Maybe Kind

aa4679922a8363b4e494079f53aaf4f64554aae0Christian MaedermaxKinds cm l = case l of

aa4679922a8363b4e494079f53aaf4f64554aae0Christian Maeder [] -> Nothing

bb4d3b6e93db1495f02de46aff5076862e30517bChristian Maeder [k] -> Just k

7ff59aa438d7a210789cad2c2c745bc9967eff82Till Mossakowski [k1, k2] -> maxKind cm k1 k2

7ff59aa438d7a210789cad2c2c745bc9967eff82Till Mossakowski k1 : k2 : ks -> case maxKind cm k1 k2 of

b565cd55a13dbccc4e66c344316da525c961e4caTill Mossakowski Just k -> maxKinds cm (k : ks)

aa4679922a8363b4e494079f53aaf4f64554aae0Christian Maeder Nothing -> do k <- maxKinds cm (k2 : ks)

aa4679922a8363b4e494079f53aaf4f64554aae0Christian Maeder maxKind cm k1 k

7ff59aa438d7a210789cad2c2c745bc9967eff82Till Mossakowski

7ff59aa438d7a210789cad2c2c745bc9967eff82Till MossakowskimaxKindss :: ClassMap -> [[Kind]] -> Maybe [Kind]

7ff59aa438d7a210789cad2c2c745bc9967eff82Till MossakowskimaxKindss cm l = let margs = map (maxKinds cm) $ transpose l in

7ff59aa438d7a210789cad2c2c745bc9967eff82Till Mossakowski if all isJust margs then Just $ map fromJust margs

7ff59aa438d7a210789cad2c2c745bc9967eff82Till Mossakowski else Nothing

7ff59aa438d7a210789cad2c2c745bc9967eff82Till Mossakowski

b565cd55a13dbccc4e66c344316da525c961e4caTill Mossakowskidom :: Monad m => ClassMap -> Kind -> [([Kind], Kind)] -> m [Kind]

aa4679922a8363b4e494079f53aaf4f64554aae0Christian Maederdom cm k ks =

7c8e78fd66aca3d24b77a9f9635f201e2f576d27Christian Maeder let fks = filter ( \ (_, rk) -> lesserKind cm rk k ) ks

7c8e78fd66aca3d24b77a9f9635f201e2f576d27Christian Maeder margs = maxKindss cm $ map fst fks

7c8e78fd66aca3d24b77a9f9635f201e2f576d27Christian Maeder in if null fks then fail ("class not found " ++ showPretty k "")

cf7e0d6750e408ddb47545d6b8349a70cf0b47afChristian Maeder else case margs of

6e29f2565572024b963af2f6d486b567307dc770Till Mossakowski Nothing -> fail "dom: maxKind"

bf76f4fcf07abaebea587df8135de8356c26a363Till Mossakowski Just args -> if any ((args ==) . fst) fks then return args

6e29f2565572024b963af2f6d486b567307dc770Till Mossakowski else fail "dom: not coregular"

bf76f4fcf07abaebea587df8135de8356c26a363Till Mossakowski

6e29f2565572024b963af2f6d486b567307dc770Till MossakowskifreshTypeVarT :: Type -> State Int Type

934473566cf3a8e4044ed10e408b4c44079684b1Christian MaederfreshTypeVarT t =

6e29f2565572024b963af2f6d486b567307dc770Till Mossakowski do (var, c) <- freshVar $ posOfType t

6e29f2565572024b963af2f6d486b567307dc770Till Mossakowski return $ TypeName var (rawKindOfType t) c

aa4679922a8363b4e494079f53aaf4f64554aae0Christian Maeder

9d34a8049237647d0188ee2ec88db2dc45f1f848Till MossakowskifreshVarsT :: [Type] -> State Int [Type]

cf7e0d6750e408ddb47545d6b8349a70cf0b47afChristian MaederfreshVarsT l = mapM freshTypeVarT l

2b565fe5cfb9f99857fd25b52304758d8544e266Mihai Codescu

cf7e0d6750e408ddb47545d6b8349a70cf0b47afChristian MaedertoPairState :: State Int a -> State (Int, b) a

2b565fe5cfb9f99857fd25b52304758d8544e266Mihai CodescutoPairState p =

2b565fe5cfb9f99857fd25b52304758d8544e266Mihai Codescu do (a, b) <- get

2b565fe5cfb9f99857fd25b52304758d8544e266Mihai Codescu let (r, c) = runState p a

9d34a8049237647d0188ee2ec88db2dc45f1f848Till Mossakowski put (c, b)

b10d6cef708b7a659f2d3b367e8e0db0d03ae3f5Till Mossakowski return r

aa4679922a8363b4e494079f53aaf4f64554aae0Christian Maeder

aa4679922a8363b4e494079f53aaf4f64554aae0Christian MaederaddSubst :: Subst -> State (Int, Subst) ()

aa4679922a8363b4e494079f53aaf4f64554aae0Christian MaederaddSubst s = do

aa4679922a8363b4e494079f53aaf4f64554aae0Christian Maeder (c, o) <- get

aa4679922a8363b4e494079f53aaf4f64554aae0Christian Maeder put (c, compSubst o s)

cf7e0d6750e408ddb47545d6b8349a70cf0b47afChristian Maeder

cf7e0d6750e408ddb47545d6b8349a70cf0b47afChristian Maederswap :: (a, b) -> (b, a)

cf7e0d6750e408ddb47545d6b8349a70cf0b47afChristian Maederswap (a, b) = (b, a)

1549f3abf73c1122acff724f718b615c82fa3648Till Mossakowski

aa4679922a8363b4e494079f53aaf4f64554aae0Christian Maeder-- pre: shapeMatch succeeds

shapeMgu :: TypeEnv -> [(Type, Type)] -> State (Int, Subst) [(Type, Type)]

shapeMgu te cs =

let (atoms, structs) = partition ( \ p -> case p of

(TypeName _ _ _, TypeName _ _ _) -> True

_ -> False) cs

in if null structs then return atoms else

let p@(t1, t2) = head structs

tl = tail structs

rest = tl ++ atoms

in case p of

(ExpandedType _ t, _) -> shapeMgu te ((t, t2) : rest)

(_, ExpandedType _ t) -> shapeMgu te ((t1, t) : rest)

(LazyType t _, _) -> shapeMgu te ((t, t2) : rest)

(_, LazyType t _) -> shapeMgu te ((t1, t) : rest)

(KindedType t _ _, _) -> shapeMgu te ((t, t2) : rest)

(_, KindedType t _ _) -> shapeMgu te ((t1, t) : rest)

(TypeName _ _ v1, _) -> if (v1 > 0) then case t2 of

ProductType ts ps -> do

nts <- toPairState $ freshVarsT ts

let s = Map.singleton v1 $ ProductType nts ps

addSubst s

shapeMgu te (zip nts ts ++ subst s rest)

FunType t3 ar t4 ps -> do

v3 <- toPairState $ freshTypeVarT t3

v4 <- toPairState $ freshTypeVarT t4

let s = Map.singleton v1 $ FunType v3 ar v4 ps

addSubst s

shapeMgu te ((t3, v3) : (v4, t4) : subst s rest)

_ -> do

let (topTy, args) = getTypeAppl t2

(_, ks) = getRawKindAppl (rawKindOfType topTy) args

vs <- toPairState $ freshVarsT args

let s = Map.singleton v1 $ mkTypeAppl topTy vs

addSubst s

shapeMgu te (concat (zipWith zipC ks $ zip vs args)

++ subst s rest)

else error ("shapeMgu: " ++ showPretty t1 " < " ++ showPretty t2 "")

(_, TypeName _ _ _) -> do ats <- shapeMgu te ((t2, t1) : map swap rest)

return $ map swap ats

(ProductType s1 _, ProductType s2 _) -> shapeMgu te (zip s1 s2 ++ rest)

(FunType t3 a1 t4 _, FunType t5 a2 t6 _) ->

let arr a = TypeName (arrowId a) funKind 0 in

shapeMgu te ((arr a1, arr a2) : (t5, t3) : (t4, t6) : rest)

_ -> let (top1, as1) = getTypeAppl t1

(top2, as2) = getTypeAppl t2

in case (top1, top2) of

(TypeName _ r1 _, TypeName _ r2 _) ->

let (_, ks) = getRawKindAppl r1 as1

in if (r1 == r2 && length as1 == length as2) then

shapeMgu te ((top1, top2) :

concat (zipWith zipC ks $ zip as1 as2)

++ rest)

else error "shapeMgu"

_ -> error ("shapeMgu: " ++ showPretty t1 " < " ++ showPretty t2 "")

zipC :: Kind -> (Type, Type) -> [(Type, Type)]

zipC k p = let q = swap p in case k of

ExtKind _ CoVar _ -> [p]

ExtKind _ ContraVar _ -> [q]

_ -> [p,q]

shapeUnify :: TypeEnv -> [(Type, Type)] -> State Int (Subst, [(Type, Type)])

shapeUnify te l = do

c <- get

let (r, (n, s)) = runState (shapeMgu te l) (c, eps)

put n

return (s, r)

getRawKindAppl :: Kind -> [a] -> (Kind, [Kind])

getRawKindAppl k args = if null args then (k, []) else

case k of

FunKind k1 k2 _ -> let (rk, ks) = getRawKindAppl k2 (tail args)

in (rk, k1 : ks)

ExtKind ek _ _ -> getRawKindAppl ek args

_ -> error ("getRawKindAppl " ++ show k)

-- input an atomized constraint list

collapser :: Rel.Rel Type -> Result Subst

collapser r =

let t = Rel.sccOfClosure r

ks = map (Set.partition ( \ e -> case e of

TypeName _ _ n -> n==0

_ -> error "collapser")) t

ws = filter (\ p -> Set.size (fst p) > 1) ks

in if null ws then

return $ foldr ( \ (cs, vs) s ->

if Set.null cs then

extendSubst s $ Set.deleteFindMin vs

else extendSubst s (Set.findMin cs, vs)) eps ks

else Result

(map ( \ (cs, _) ->

let (c1, rs) = Set.deleteFindMin cs

c2 = Set.findMin rs

in Diag Hint ("contradicting type inclusions for '"

++ showPretty c1 "' and '"

++ showPretty c2 "'") []) ws) Nothing

extendSubst :: Subst -> (Type, Set.Set Type) -> Subst

extendSubst s (t, vs) = Set.fold ( \ (TypeName _ _ n) ->

Map.insert n t) s vs

-- | partition into qualification and subtyping constraints

partitionC :: Constraints -> (Constraints, Constraints)

partitionC = Set.partition ( \ c -> case c of

Kinding _ _ -> True

Subtyping _ _ -> False)

-- | convert subtypings constrains to a pair list

toListC :: Constraints -> [(Type, Type)]

toListC l = [ (t1, t2) | Subtyping t1 t2 <- Set.toList l ]

shapeRel :: TypeEnv -> Constraints

-> State Int (Result (Subst, Constraints, Rel.Rel Type))

shapeRel te cs =

let (qs, subS) = partitionC cs

subL = toListC subS

in case shapeMatch (typeMap te) (map fst subL) $ map snd subL of

Result ds Nothing -> return $ Result ds Nothing

_ -> do (s1, atoms) <- shapeUnify te subL

let r = Rel.transClosure $ Rel.fromList atoms

es = Map.foldWithKey ( \ t1 st l1 ->

case t1 of

TypeName _ _ 0 -> Set.fold ( \ t2 l2 ->

case t2 of

TypeName _ _ 0 -> if lesserType te t1 t2

then l2 else (t1, t2) : l2

_ -> l2) l1 st

_ -> l1) [] $ Rel.toMap r

return $ if null es then

case collapser r of

Result ds Nothing -> Result ds Nothing

Result _ (Just s2) ->

let s = compSubst s1 s2

in return (s, substC s qs,

Rel.fromList $ subst s2 atoms)

else Result (map ( \ (t1, t2) ->

mkDiag Hint "rejected" $

Subtyping t1 t2) es) Nothing

-- | compute monotonicity of a type variable

monotonic :: TypeEnv -> Int -> Type -> (Bool, Bool)

monotonic te v t =

case t of

TypeName _ _ i -> (True, i /= v)

ExpandedType _ t2 -> monotonic te v t2

KindedType tk _ _ -> monotonic te v tk

LazyType tl _ -> monotonic te v tl

_ -> let (top, args) = getTypeAppl t in case top of

TypeName _ k _ ->

let ks = snd $ getRawKindAppl k args

(bs1, bs2) = unzip $ zipWith ( \ rk a ->

let (b1, b2) = monotonic te v a

in case rk of

ExtKind _ CoVar _ -> (b1, b2)

ExtKind _ ContraVar _ -> (b2, b1)

_ -> (b1 && b2, b1 && b2)) ks args

in (and bs1, and bs2)

_ -> error "monotonic"

-- | find monotonicity based instantiation

monoSubst :: TypeEnv -> Rel.Rel Type -> Type -> Subst

monoSubst te r t =

let varSet = Set.fromList . leaves (> 0)

vs = Set.toList $ Set.union (varSet t) $ Set.unions $ map varSet

$ Set.toList $ Rel.nodes r

monos = filter ( \ (i, (n, rk)) -> case monotonic te i t of

(True, _) -> 1 == Set.size

(Rel.predecessors r $

TypeName n rk i)

_ -> False) vs

antis = filter ( \ (i, (n, rk)) -> case monotonic te i t of

(_, True) -> 1 == Set.size

(Rel.succs r $

TypeName n rk i)

_ -> False) vs

resta = filter ( \ (i, (n, rk)) -> case monotonic te i t of

(True, True) -> 1 < Set.size

(Rel.succs r $

TypeName n rk i)

_ -> False) vs

restb = filter ( \ (i, (n, rk)) -> case monotonic te i t of

(True, True) -> 1 < Set.size

(Rel.predecessors r $

TypeName n rk i)

_ -> False) vs

in if null antis then

if null monos then

if null resta then

if null restb then eps else

let (i, (n, rk)) = head restb

tn = TypeName n rk i

s = Rel.predecessors r tn

sl = Set.delete tn $ foldl1 Set.intersection

$ map (Rel.succs r)

$ Set.toList s

in Map.singleton i $ Set.findMin $ if Set.null sl then s

else sl

else let (i, (n, rk)) = head resta

tn = TypeName n rk i

s = Rel.succs r tn

sl = Set.delete tn $ foldl1 Set.intersection

$ map (Rel.predecessors r)

$ Set.toList s

in Map.singleton i $ Set.findMin $ if Set.null sl then s

else sl

else Map.fromAscList $ map ( \ (i, (n, rk)) ->

(i, Set.findMin $ Rel.predecessors r $

TypeName n rk i)) monos

else Map.fromAscList $ map ( \ (i, (n, rk)) ->

(i, Set.findMin $ Rel.succs r $

TypeName n rk i)) antis

monoSubsts :: TypeEnv -> Rel.Rel Type -> Type -> Subst

monoSubsts te r t =

let s = monoSubst te (Rel.transReduce $ Rel.irreflex r) t in

if Map.null s then s else

compSubst s $

monoSubsts te (Rel.transClosure $ Rel.map (subst s) r)

$ subst s t

fromTypeMap :: TypeMap -> Rel.Rel Type

fromTypeMap = Map.foldWithKey (\ t ti r ->

foldr (Rel.insert (TypeName t (typeKind ti) 0)) r

[ ty | ty@(TypeName _ _ _) <-

superTypes ti ]) Rel.empty