bbae6e6ca0de7f2ffbb44d2c8da179f2b717237fChristian Maeder{- |

bbae6e6ca0de7f2ffbb44d2c8da179f2b717237fChristian MaederModule : $Header$

bbae6e6ca0de7f2ffbb44d2c8da179f2b717237fChristian MaederDescription : infer the kinds of types

75a6279dbae159d018ef812185416cf6df386c10Till MossakowskiCopyright : (c) Christian Maeder and Uni Bremen 2003-2005

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

bbae6e6ca0de7f2ffbb44d2c8da179f2b717237fChristian Maeder

bbae6e6ca0de7f2ffbb44d2c8da179f2b717237fChristian MaederMaintainer : Christian.Maeder@dfki.de

bbae6e6ca0de7f2ffbb44d2c8da179f2b717237fChristian MaederStability : experimental

bbae6e6ca0de7f2ffbb44d2c8da179f2b717237fChristian MaederPortability : portable

bbae6e6ca0de7f2ffbb44d2c8da179f2b717237fChristian Maeder

bbae6e6ca0de7f2ffbb44d2c8da179f2b717237fChristian Maederanalyse types

bbae6e6ca0de7f2ffbb44d2c8da179f2b717237fChristian Maeder-}

bbae6e6ca0de7f2ffbb44d2c8da179f2b717237fChristian Maeder

bbae6e6ca0de7f2ffbb44d2c8da179f2b717237fChristian Maedermodule HasCASL.TypeAna where

bbae6e6ca0de7f2ffbb44d2c8da179f2b717237fChristian Maeder

5e26bfc8d7b18cf3a3fa7b919b4450fb669f37a5Christian Maederimport HasCASL.As

ee9eddfa6953868fd6fbaff0d9ff68675a13675aChristian Maederimport HasCASL.AsUtils

1d589334ba6b4a4cbfb35307a7a732261e77b0cdChristian Maederimport HasCASL.Le

1d589334ba6b4a4cbfb35307a7a732261e77b0cdChristian Maederimport HasCASL.ClassAna

bbae6e6ca0de7f2ffbb44d2c8da179f2b717237fChristian Maederimport HasCASL.TypeMixAna

bbae6e6ca0de7f2ffbb44d2c8da179f2b717237fChristian Maederimport qualified Data.Map as Map

715ffaf874309df081d1e1cd8e05073fc1227729Christian Maederimport qualified Data.Set as Set

5e26bfc8d7b18cf3a3fa7b919b4450fb669f37a5Christian Maederimport Common.DocUtils

ee9eddfa6953868fd6fbaff0d9ff68675a13675aChristian Maederimport Common.Id

bbae6e6ca0de7f2ffbb44d2c8da179f2b717237fChristian Maederimport Common.Result

5e26bfc8d7b18cf3a3fa7b919b4450fb669f37a5Christian Maederimport Data.List as List

33a5d53a412ba0a4e5847f7538d6da2e22bd116cChristian Maederimport Data.Maybe

715ffaf874309df081d1e1cd8e05073fc1227729Christian Maederimport Common.Lib.State

e774ab5733a1d673b123b0e63b14dd533e6fd4fcChristian Maeder

bbae6e6ca0de7f2ffbb44d2c8da179f2b717237fChristian Maeder-- * infer kind

715ffaf874309df081d1e1cd8e05073fc1227729Christian Maeder

715ffaf874309df081d1e1cd8e05073fc1227729Christian Maeder-- | extract kinds of type identifier

715ffaf874309df081d1e1cd8e05073fc1227729Christian MaedergetIdKind :: Env -> Id -> Result ((Variance, RawKind, Set.Set Kind), Type)

715ffaf874309df081d1e1cd8e05073fc1227729Christian MaedergetIdKind te i =

715ffaf874309df081d1e1cd8e05073fc1227729Christian Maeder case Map.lookup i $ localTypeVars te of

715ffaf874309df081d1e1cd8e05073fc1227729Christian Maeder Nothing -> case Map.lookup i $ typeMap te of

715ffaf874309df081d1e1cd8e05073fc1227729Christian Maeder Nothing -> mkError "unknown type" i

715ffaf874309df081d1e1cd8e05073fc1227729Christian Maeder Just (TypeInfo rk l _ _) ->

715ffaf874309df081d1e1cd8e05073fc1227729Christian Maeder return ((InVar, rk, l), TypeName i rk 0)

715ffaf874309df081d1e1cd8e05073fc1227729Christian Maeder Just (TypeVarDefn v vk rk c) ->

715ffaf874309df081d1e1cd8e05073fc1227729Christian Maeder return ((v, rk, Set.singleton $ toKind vk), TypeName i rk c)

715ffaf874309df081d1e1cd8e05073fc1227729Christian Maeder

715ffaf874309df081d1e1cd8e05073fc1227729Christian Maeder-- | extract kinds of co- or invariant type identifiers

715ffaf874309df081d1e1cd8e05073fc1227729Christian MaedergetCoVarKind :: Maybe Bool -> Env -> Id

715ffaf874309df081d1e1cd8e05073fc1227729Christian Maeder -> Result ((RawKind, Set.Set Kind), Type)

715ffaf874309df081d1e1cd8e05073fc1227729Christian MaedergetCoVarKind b te i = do

2a598ff0c1b7b51c33aee7029b43bc5cfcbea6b8Christian Maeder ((v, rk, l), ty) <- getIdKind te i

38775225cf810f5895cc03b4acbcfe8f84f2513aChristian Maeder case (v, b) of

ccf3de3d66b521a260e5c22d335c64a48e3f0195Christian Maeder (ContraVar, Just True) -> Result

ccf3de3d66b521a260e5c22d335c64a48e3f0195Christian Maeder [mkDiag Hint "wrong contravariance of" i]

ccf3de3d66b521a260e5c22d335c64a48e3f0195Christian Maeder $ Just ((rk, Set.empty), ty)

aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder (CoVar, Just False) -> Result

aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder [mkDiag Hint "wrong covariance of" i]

2a598ff0c1b7b51c33aee7029b43bc5cfcbea6b8Christian Maeder $ Just ((rk, Set.empty), ty)

ccf3de3d66b521a260e5c22d335c64a48e3f0195Christian Maeder _ -> return ((rk, l), ty)

2a598ff0c1b7b51c33aee7029b43bc5cfcbea6b8Christian Maeder

2a598ff0c1b7b51c33aee7029b43bc5cfcbea6b8Christian Maeder-- | check if there is at least one solution

2a598ff0c1b7b51c33aee7029b43bc5cfcbea6b8Christian MaedersubKinds :: DiagKind -> ClassMap -> Type -> Set.Set Kind -> Set.Set Kind

2a598ff0c1b7b51c33aee7029b43bc5cfcbea6b8Christian Maeder -> Set.Set Kind -> Result (Set.Set Kind)

2a598ff0c1b7b51c33aee7029b43bc5cfcbea6b8Christian MaedersubKinds dk cm ty sk ks res =

2a598ff0c1b7b51c33aee7029b43bc5cfcbea6b8Christian Maeder if Set.null $ Set.filter (flip (newKind cm) ks) sk then return res

2a598ff0c1b7b51c33aee7029b43bc5cfcbea6b8Christian Maeder else Result [Diag dk

2a598ff0c1b7b51c33aee7029b43bc5cfcbea6b8Christian Maeder ("no kind found for '" ++ showDoc ty "'" ++

2a598ff0c1b7b51c33aee7029b43bc5cfcbea6b8Christian Maeder if Set.null ks then "" else expected sk ks)

2a598ff0c1b7b51c33aee7029b43bc5cfcbea6b8Christian Maeder $ getRange ty] $ Just Set.empty

2a598ff0c1b7b51c33aee7029b43bc5cfcbea6b8Christian Maeder

715ffaf874309df081d1e1cd8e05073fc1227729Christian Maeder-- | add an analysed type argument (warn on redeclared types)

715ffaf874309df081d1e1cd8e05073fc1227729Christian MaederaddTypeVarDecl :: Bool -> TypeArg -> State Env ()

d17834302eaa101395b4b806cd73670fd864445fChristian MaederaddTypeVarDecl warn (TypeArg i v vk rk c _ _) =

ccf3de3d66b521a260e5c22d335c64a48e3f0195Christian Maeder addLocalTypeVar warn (TypeVarDefn v vk rk c) i

aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder

aff01ee50b66032469c232e00c945d1fd4f57d1bChristian MaederaddLocalTypeVar :: Bool -> TypeVarDefn -> Id -> State Env ()

aff01ee50b66032469c232e00c945d1fd4f57d1bChristian MaederaddLocalTypeVar warn tvd i = do

715ffaf874309df081d1e1cd8e05073fc1227729Christian Maeder tvs <- gets localTypeVars

aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder if warn then do

aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder tm <- gets typeMap

715ffaf874309df081d1e1cd8e05073fc1227729Christian Maeder case Map.lookup i tm of

2a598ff0c1b7b51c33aee7029b43bc5cfcbea6b8Christian Maeder Nothing -> case Map.lookup i tvs of

2a598ff0c1b7b51c33aee7029b43bc5cfcbea6b8Christian Maeder Nothing -> return ()

715ffaf874309df081d1e1cd8e05073fc1227729Christian Maeder Just _ -> addDiags [mkDiag Hint "rebound type variable" i]

2a598ff0c1b7b51c33aee7029b43bc5cfcbea6b8Christian Maeder Just _ -> addDiags [mkDiag Hint

715ffaf874309df081d1e1cd8e05073fc1227729Christian Maeder "type variable shadows type constructor" i]

2a598ff0c1b7b51c33aee7029b43bc5cfcbea6b8Christian Maeder else return ()

5e26bfc8d7b18cf3a3fa7b919b4450fb669f37a5Christian Maeder putLocalTypeVars $ Map.insert i tvd tvs

5e26bfc8d7b18cf3a3fa7b919b4450fb669f37a5Christian Maeder

5e26bfc8d7b18cf3a3fa7b919b4450fb669f37a5Christian Maeder-- | infer all minimal kinds

aff01ee50b66032469c232e00c945d1fd4f57d1bChristian MaederinferKinds :: Maybe Bool -> Type -> Env

836e72a3c413366ba9801726f3b249c7791cb9caChristian Maeder -> Result ((RawKind, Set.Set Kind), Type)

836e72a3c413366ba9801726f3b249c7791cb9caChristian MaederinferKinds b ty te@Env{classMap = cm} = case ty of

2a598ff0c1b7b51c33aee7029b43bc5cfcbea6b8Christian Maeder TypeName i _ _ -> getCoVarKind b te i

7dec34aee2b609b9535c48d060e0f7baf3536457Christian Maeder TypeAppl t1 t2 -> do

aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder ((rk, ks), t3) <- inferKinds b t1 te

7dec34aee2b609b9535c48d060e0f7baf3536457Christian Maeder case rk of

5e26bfc8d7b18cf3a3fa7b919b4450fb669f37a5Christian Maeder FunKind v _ rr _ -> do

5e26bfc8d7b18cf3a3fa7b919b4450fb669f37a5Christian Maeder ((_, l), t4) <- inferKinds (case v of

5e26bfc8d7b18cf3a3fa7b919b4450fb669f37a5Christian Maeder ContraVar -> Just $ maybe False not b

5e26bfc8d7b18cf3a3fa7b919b4450fb669f37a5Christian Maeder CoVar -> Just $ maybe True id b

aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder InVar -> Nothing) t2 te

5e26bfc8d7b18cf3a3fa7b919b4450fb669f37a5Christian Maeder kks <- mapM (getFunKinds cm) $ Set.toList ks

bbae6e6ca0de7f2ffbb44d2c8da179f2b717237fChristian Maeder rs <- mapM ( \ fk -> case fk of

2a598ff0c1b7b51c33aee7029b43bc5cfcbea6b8Christian Maeder FunKind _ arg res _ -> subKinds Hint cm t2

aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder (Set.singleton arg) l $ Set.singleton res

5e26bfc8d7b18cf3a3fa7b919b4450fb669f37a5Christian Maeder _ -> error "inferKinds: no function kind"

5e26bfc8d7b18cf3a3fa7b919b4450fb669f37a5Christian Maeder ) $ Set.toList $ keepMinKinds cm kks

5e26bfc8d7b18cf3a3fa7b919b4450fb669f37a5Christian Maeder return ((rr, keepMinKinds cm rs), TypeAppl t3 t4)

797f811e57952d59e73b8cd03b667eef276db972Christian Maeder _ -> mkError "unexpected type argument" t2

2a598ff0c1b7b51c33aee7029b43bc5cfcbea6b8Christian Maeder TypeAbs ta@(TypeArg _ v k r _ _ q) t ps -> do

aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder let newEnv = execState (addTypeVarDecl False ta) te

5e26bfc8d7b18cf3a3fa7b919b4450fb669f37a5Christian Maeder ((rk, ks), nt) <- inferKinds Nothing t newEnv

5e26bfc8d7b18cf3a3fa7b919b4450fb669f37a5Christian Maeder return (( FunKind v r rk q

5e26bfc8d7b18cf3a3fa7b919b4450fb669f37a5Christian Maeder , keepMinKinds cm

5e26bfc8d7b18cf3a3fa7b919b4450fb669f37a5Christian Maeder [Set.map (\ j -> FunKind v (toKind k) j q) ks])

5e26bfc8d7b18cf3a3fa7b919b4450fb669f37a5Christian Maeder , TypeAbs ta nt ps)

5e26bfc8d7b18cf3a3fa7b919b4450fb669f37a5Christian Maeder KindedType kt kind ps -> do

bbae6e6ca0de7f2ffbb44d2c8da179f2b717237fChristian Maeder let Result ds _ = mapM (flip anaKindM cm) $ Set.toList kind

ccf3de3d66b521a260e5c22d335c64a48e3f0195Christian Maeder sk <- if null ds then return kind else Result ds Nothing

2a598ff0c1b7b51c33aee7029b43bc5cfcbea6b8Christian Maeder ((rk, ks), t) <- inferKinds b kt te

d17834302eaa101395b4b806cd73670fd864445fChristian Maeder l <- subKinds Hint cm kt sk ks sk

e1839fb37a3a2ccd457464cb0dcc5efd466dbe22Christian Maeder return ((rk, l), KindedType t sk ps)

2a598ff0c1b7b51c33aee7029b43bc5cfcbea6b8Christian Maeder ExpandedType t1 t2 -> do

e774ab5733a1d673b123b0e63b14dd533e6fd4fcChristian Maeder ((rk, ks), t4) <- inferKinds b t2 te

2a598ff0c1b7b51c33aee7029b43bc5cfcbea6b8Christian Maeder ((_, aks), t3) <- inferKinds b t1 te

2a598ff0c1b7b51c33aee7029b43bc5cfcbea6b8Christian Maeder return ((rk, keepMinKinds cm [aks, ks]), ExpandedType t3 t4)

aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder _ -> error "inferKinds"

7dec34aee2b609b9535c48d060e0f7baf3536457Christian Maeder

7dec34aee2b609b9535c48d060e0f7baf3536457Christian Maeder-- * converting type terms

1738d16957389457347bee85075d3d33d002158fChristian Maeder

1738d16957389457347bee85075d3d33d002158fChristian Maeder-- | throw away alias or kind information

1738d16957389457347bee85075d3d33d002158fChristian MaederstripType :: String -> Type -> Type

33a5d53a412ba0a4e5847f7538d6da2e22bd116cChristian MaederstripType msg ty = case ty of

aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder ExpandedType _ t -> t

2a598ff0c1b7b51c33aee7029b43bc5cfcbea6b8Christian Maeder KindedType t _ _ -> t

2a598ff0c1b7b51c33aee7029b43bc5cfcbea6b8Christian Maeder _ -> error $ "stripType " ++ msg

0f67ca7b0c738a28f6688ba6e96d44d7c14af611Christian Maeder

c70d42540b8f8c3c141cc0779599d25f7eb69bbfChristian Maeder-- * subtyping relation

5e26bfc8d7b18cf3a3fa7b919b4450fb669f37a5Christian Maeder

aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder-- | extract the raw kind from a type term

5e26bfc8d7b18cf3a3fa7b919b4450fb669f37a5Christian MaederrawKindOfType :: Type -> RawKind

1d589334ba6b4a4cbfb35307a7a732261e77b0cdChristian MaederrawKindOfType ty = case ty of

1d589334ba6b4a4cbfb35307a7a732261e77b0cdChristian Maeder TypeName _ k _ -> k

1d589334ba6b4a4cbfb35307a7a732261e77b0cdChristian Maeder TypeAppl t1 _ -> case rawKindOfType t1 of

1d589334ba6b4a4cbfb35307a7a732261e77b0cdChristian Maeder FunKind _ _ rk _ -> rk

1d589334ba6b4a4cbfb35307a7a732261e77b0cdChristian Maeder _ -> error "rawKindOfType"

1d589334ba6b4a4cbfb35307a7a732261e77b0cdChristian Maeder TypeAbs (TypeArg _ v _ r _ _ _) t ps ->

1d589334ba6b4a4cbfb35307a7a732261e77b0cdChristian Maeder FunKind v r (rawKindOfType t) ps

1d589334ba6b4a4cbfb35307a7a732261e77b0cdChristian Maeder _ -> rawKindOfType $ stripType "rawKindOfType" ty

1d589334ba6b4a4cbfb35307a7a732261e77b0cdChristian Maeder

1d589334ba6b4a4cbfb35307a7a732261e77b0cdChristian Maeder-- | subtyping relation

1d589334ba6b4a4cbfb35307a7a732261e77b0cdChristian MaederlesserType :: Env -> Type -> Type -> Bool

1d589334ba6b4a4cbfb35307a7a732261e77b0cdChristian MaederlesserType te t1 t2 = case (t1, t2) of

1d589334ba6b4a4cbfb35307a7a732261e77b0cdChristian Maeder (TypeAppl c1 a1, TypeAppl c2 a2) ->

1d589334ba6b4a4cbfb35307a7a732261e77b0cdChristian Maeder let b1 = lesserType te a1 a2

1d589334ba6b4a4cbfb35307a7a732261e77b0cdChristian Maeder b2 = lesserType te a2 a1

1d589334ba6b4a4cbfb35307a7a732261e77b0cdChristian Maeder b = b1 && b2

1d589334ba6b4a4cbfb35307a7a732261e77b0cdChristian Maeder in (case (rawKindOfType c1, rawKindOfType c2) of

aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder (FunKind v1 _ _ _, FunKind v2 _ _ _) ->

aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder if v1 == v2 then case v1 of

1d589334ba6b4a4cbfb35307a7a732261e77b0cdChristian Maeder CoVar -> b1

1d589334ba6b4a4cbfb35307a7a732261e77b0cdChristian Maeder ContraVar -> b2

1d589334ba6b4a4cbfb35307a7a732261e77b0cdChristian Maeder _ -> b

1d589334ba6b4a4cbfb35307a7a732261e77b0cdChristian Maeder else b

1d589334ba6b4a4cbfb35307a7a732261e77b0cdChristian Maeder _ -> error "lesserType: no FunKind") && lesserType te c1 c2

aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder (TypeName i1 _ _, TypeName i2 _ _) | i1 == i2 -> True

aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder (TypeName i k _, _) -> case Map.lookup i $ localTypeVars te of

1d589334ba6b4a4cbfb35307a7a732261e77b0cdChristian Maeder Nothing -> case Map.lookup i $ typeMap te of

aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder Nothing -> False

1d589334ba6b4a4cbfb35307a7a732261e77b0cdChristian Maeder Just ti -> any ( \ j -> lesserType te (TypeName j k 0) t2) $

1d589334ba6b4a4cbfb35307a7a732261e77b0cdChristian Maeder Set.toList $ superTypes ti

1d589334ba6b4a4cbfb35307a7a732261e77b0cdChristian Maeder Just (TypeVarDefn _ vk _ _) -> case vk of

1d589334ba6b4a4cbfb35307a7a732261e77b0cdChristian Maeder Downset t -> lesserType te t t2

1d589334ba6b4a4cbfb35307a7a732261e77b0cdChristian Maeder _ -> False

aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder (TypeAppl _ _, TypeName _ _ _) -> False

aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder (TypeAppl _ _, TypeAbs _ _ _) -> False

(TypeAbs _ _ _, TypeName _ _ _) -> False

(KindedType t _ _, _) -> lesserType te t t2

(ExpandedType _ t, _) -> lesserType te t t2

(_, KindedType t _ _) -> lesserType te t1 t

(_, ExpandedType _ t) -> lesserType te t1 t

(t3, t4) -> t3 == t4

-- * leaves of types and substitution

-- | the type name components of a type

leaves :: (Int -> Bool) -> Type -> [(Int, (Id, RawKind))]

leaves b t =

case t of

TypeName j k i -> if b(i)

then [(i, (j, k))]

else []

TypeAppl t1 t2 -> leaves b t1 `List.union` leaves b t2

TypeAbs (TypeArg i _ _ r c _ _) ty _ ->

List.delete (c, (i, r)) $ leaves b ty

_ -> leaves b $ stripType "leaves" t

-- | type identifiers of a type

idsOf :: (Int -> Bool) -> Type -> Set.Set Id

idsOf b = Set.fromList . map (fst . snd) . leaves b

-- | replace some type names with types

repl :: Map.Map Id Type -> Type -> Type

repl m = rename ( \ i k n ->

case Map.lookup i m of

Just s -> s

Nothing -> TypeName i k n)

-- * super type ids

-- | compute super type ids of one type id

superIds :: TypeMap -> Id -> Set.Set Id

superIds tm = supIds tm Set.empty . Set.singleton

-- | compute all super type ids for several type ids given as second argument

supIds :: TypeMap -> Set.Set Id -> Set.Set Id -> Set.Set Id

supIds tm known new =

if Set.null new then known else

let more = Set.unions $ map ( \ i -> superTypes

$ Map.findWithDefault starTypeInfo i tm)

$ Set.toList new

newKnown = Set.union known new

in supIds tm newKnown (more Set.\\ newKnown)

-- * expand alias types

-- | expand aliases in a type scheme

expand :: TypeMap -> TypeScheme -> TypeScheme

expand = mapTypeOfScheme . expandAliases

filterAliases :: TypeMap -> TypeMap

filterAliases = Map.filter ( \ ti -> case typeDefn ti of

AliasTypeDefn _ -> True

_ -> False)

-- | expand aliases in a type and reduce type map first

expandAlias :: TypeMap -> Type -> Type

expandAlias = expandAliases . filterAliases

-- | expand aliases in a type if type map non-null

expandAliases :: TypeMap -> Type -> Type

expandAliases tm = if Map.null tm then id else expandAux tm

-- | expand aliases in a type

expandAux :: TypeMap -> Type -> Type

expandAux tm ty = rename ( \ i k n ->

case Map.lookup i tm of

Just TypeInfo {typeDefn = AliasTypeDefn s} ->

ExpandedType (TypeName i k n) s

_ -> TypeName i k n) ty

-- | find unexpanded alias identifier

hasAlias :: TypeMap -> Type -> [Diagnosis]

hasAlias tm t =

map ( \ i -> mkDiag Error ("unexpanded alias '" ++ showId i "' in") t)

$ Set.toList $ Set.intersection (idsOf (const True) t) $

Map.keysSet $ filterAliases tm

-- * resolve and analyse types

-- | resolve type and infer minimal kinds

anaTypeM :: (Maybe Kind, Type) -> Env -> Result ((RawKind, Set.Set Kind), Type)

anaTypeM (mk, parsedType) te =

do resolvedType <- mkTypeConstrAppl te parsedType

let tm = typeMap te

adj = adjustPos $ getRange parsedType

expandedType = expandAlias tm resolvedType

cm = classMap te

((rk, ks), checkedType) <- adj $ inferKinds Nothing expandedType te

l <- adj $ case mk of

Nothing -> subKinds Error cm parsedType

(if Set.null ks then Set.singleton universe else ks) ks ks

Just k -> subKinds Error cm parsedType (Set.singleton k) ks $

Set.filter (flip (lesserKind cm) k) ks

Result (hasAlias tm checkedType) $ Just ()

return ((rk, l), checkedType)

-- | resolve the type and check if it is of the universe class

anaStarTypeM :: Type -> Env -> Result ((RawKind, Set.Set Kind), Type)

anaStarTypeM t = anaTypeM (Just universe, t)

-- * misc functions on types

-- | check if an id occurs in a type

cyclicType :: Id -> Type -> Bool

cyclicType i ty = Set.member i $ idsOf (==0) ty

-- | check for unbound (or if False for too many) type variables

unboundTypevars :: Bool -> [TypeArg] -> Type -> [Diagnosis]

unboundTypevars b args ty =

let fvs = map (fst . snd) (leaves (> 0) ty)

argIds = map getTypeVar args

restVars1 = fvs List.\\ argIds

restVars2 = argIds List.\\ fvs

in (if null restVars1 then []

else [mkDiag Error ("unbound type variable(s)\n "

++ showSepList ("," ++) showId

restVars1 " in") ty])

++ if b || null restVars2 then [] else

[mkDiag Warning ("ignoring unused variable(s)\n "

++ showSepList ("," ++) showId

restVars2 " in") ty]

-- | check for proper generalizability (False: warn also for unused types)

generalizable :: Bool -> TypeScheme -> [Diagnosis]

generalizable b (TypeScheme args ty _) =

unboundTypevars b args ty ++ checkUniqueTypevars args

-- | check uniqueness of type variables

checkUniqueTypevars :: [TypeArg] -> [Diagnosis]

checkUniqueTypevars = checkUniqueness . map getTypeVar