{- |
Module      :  ./HasCASL/TypeAna.hs
Description :  infer the kinds of types
Copyright   :  (c) Christian Maeder and Uni Bremen 2003-2005
License     :  GPLv2 or higher, see LICENSE.txt

Maintainer  :  Christian.Maeder@dfki.de
Stability   :  experimental
Portability :  portable

analyse types
-}

module HasCASL.TypeAna where

import HasCASL.As
import HasCASL.FoldType
import HasCASL.AsUtils
import HasCASL.Le
import HasCASL.ClassAna
import HasCASL.TypeMixAna
import qualified Data.Map as Map
import qualified Data.Set as Set
import Common.DocUtils
import Common.Id
import Common.Result
import Common.Utils
import Common.Lib.State

import Data.Maybe
import Data.List as List

import Control.Monad

-- * infer kind

-- | extract kinds of type identifier
getIdKind :: Env -> Id -> Result ((Variance, RawKind, Set.Set Kind), Type)
getIdKind :: Env -> Id -> Result ((Variance, RawKind, Set Kind), Type)
getIdKind te :: Env
te i :: Id
i =
    case Id -> Map Id TypeVarDefn -> Maybe TypeVarDefn
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Id
i (Map Id TypeVarDefn -> Maybe TypeVarDefn)
-> Map Id TypeVarDefn -> Maybe TypeVarDefn
forall a b. (a -> b) -> a -> b
$ Env -> Map Id TypeVarDefn
localTypeVars Env
te of
       Nothing -> case Id -> Map Id TypeInfo -> Maybe TypeInfo
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Id
i (Map Id TypeInfo -> Maybe TypeInfo)
-> Map Id TypeInfo -> Maybe TypeInfo
forall a b. (a -> b) -> a -> b
$ Env -> Map Id TypeInfo
typeMap Env
te of
           Nothing -> String -> Id -> Result ((Variance, RawKind, Set Kind), Type)
forall a b. (GetRange a, Pretty a) => String -> a -> Result b
mkError "unknown type" Id
i
           Just (TypeInfo rk :: RawKind
rk l :: Set Kind
l _ _) ->
               ((Variance, RawKind, Set Kind), Type)
-> Result ((Variance, RawKind, Set Kind), Type)
forall (m :: * -> *) a. Monad m => a -> m a
return ((Variance
NonVar, RawKind
rk, Set Kind
l), Id -> RawKind -> Int -> Type
TypeName Id
i RawKind
rk 0)
       Just (TypeVarDefn v :: Variance
v vk :: VarKind
vk rk :: RawKind
rk c :: Int
c) ->
           ((Variance, RawKind, Set Kind), Type)
-> Result ((Variance, RawKind, Set Kind), Type)
forall (m :: * -> *) a. Monad m => a -> m a
return ((Variance
v, RawKind
rk, Kind -> Set Kind
forall a. a -> Set a
Set.singleton (Kind -> Set Kind) -> Kind -> Set Kind
forall a b. (a -> b) -> a -> b
$ VarKind -> Kind
toKind VarKind
vk), Id -> RawKind -> Int -> Type
TypeName Id
i RawKind
rk Int
c)

-- | extract kinds of co- or invariant type identifiers
getCoVarKind :: Maybe Bool -> Env -> Id
             -> Result ((RawKind, Set.Set Kind), Type)
getCoVarKind :: Maybe Bool -> Env -> Id -> Result ((RawKind, Set Kind), Type)
getCoVarKind b :: Maybe Bool
b te :: Env
te i :: Id
i = do
    ((v :: Variance
v, rk :: RawKind
rk, l :: Set Kind
l), ty :: Type
ty) <- Env -> Id -> Result ((Variance, RawKind, Set Kind), Type)
getIdKind Env
te Id
i
    case (Variance
v, Maybe Bool
b) of
           (ContraVar, Just True) -> [Diagnosis]
-> Maybe ((RawKind, Set Kind), Type)
-> Result ((RawKind, Set Kind), Type)
forall a. [Diagnosis] -> Maybe a -> Result a
Result
               [DiagKind -> String -> Id -> Diagnosis
forall a.
(GetRange a, Pretty a) =>
DiagKind -> String -> a -> Diagnosis
mkDiag DiagKind
Hint "wrong contravariance of" Id
i]
               (Maybe ((RawKind, Set Kind), Type)
 -> Result ((RawKind, Set Kind), Type))
-> Maybe ((RawKind, Set Kind), Type)
-> Result ((RawKind, Set Kind), Type)
forall a b. (a -> b) -> a -> b
$ ((RawKind, Set Kind), Type) -> Maybe ((RawKind, Set Kind), Type)
forall a. a -> Maybe a
Just ((RawKind
rk, Set Kind
forall a. Set a
Set.empty), Type
ty)
           (CoVar, Just False) -> [Diagnosis]
-> Maybe ((RawKind, Set Kind), Type)
-> Result ((RawKind, Set Kind), Type)
forall a. [Diagnosis] -> Maybe a -> Result a
Result
               [DiagKind -> String -> Id -> Diagnosis
forall a.
(GetRange a, Pretty a) =>
DiagKind -> String -> a -> Diagnosis
mkDiag DiagKind
Hint "wrong covariance of" Id
i]
               (Maybe ((RawKind, Set Kind), Type)
 -> Result ((RawKind, Set Kind), Type))
-> Maybe ((RawKind, Set Kind), Type)
-> Result ((RawKind, Set Kind), Type)
forall a b. (a -> b) -> a -> b
$ ((RawKind, Set Kind), Type) -> Maybe ((RawKind, Set Kind), Type)
forall a. a -> Maybe a
Just ((RawKind
rk, Set Kind
forall a. Set a
Set.empty), Type
ty)
           _ -> ((RawKind, Set Kind), Type) -> Result ((RawKind, Set Kind), Type)
forall (m :: * -> *) a. Monad m => a -> m a
return ((RawKind
rk, Set Kind
l), Type
ty)

-- | check if there is at least one solution
subKinds :: DiagKind -> ClassMap -> Type -> Set.Set Kind -> Set.Set Kind
         -> Set.Set Kind -> Result (Set.Set Kind)
subKinds :: DiagKind
-> ClassMap
-> Type
-> Set Kind
-> Set Kind
-> Set Kind
-> Result (Set Kind)
subKinds dk :: DiagKind
dk cm :: ClassMap
cm ty :: Type
ty sk :: Set Kind
sk ks :: Set Kind
ks res :: Set Kind
res =
   if Set Kind -> Bool
forall a. Set a -> Bool
Set.null (Set Kind -> Bool) -> Set Kind -> Bool
forall a b. (a -> b) -> a -> b
$ (Kind -> Bool) -> Set Kind -> Set Kind
forall a. (a -> Bool) -> Set a -> Set a
Set.filter ((Kind -> Set Kind -> Bool) -> Set Kind -> Kind -> Bool
forall a b c. (a -> b -> c) -> b -> a -> c
flip (ClassMap -> Kind -> Set Kind -> Bool
newKind ClassMap
cm) Set Kind
ks) Set Kind
sk then Set Kind -> Result (Set Kind)
forall (m :: * -> *) a. Monad m => a -> m a
return Set Kind
res
   else [Diagnosis] -> Maybe (Set Kind) -> Result (Set Kind)
forall a. [Diagnosis] -> Maybe a -> Result a
Result [DiagKind -> String -> Range -> Diagnosis
Diag DiagKind
dk
        ("no kind found for '" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Type -> String -> String
forall a. Pretty a => a -> String -> String
showDoc Type
ty "'" String -> String -> String
forall a. [a] -> [a] -> [a]
++
         if Set Kind -> Bool
forall a. Set a -> Bool
Set.null Set Kind
ks then "" else Set Kind -> Set Kind -> String
forall a. Pretty a => a -> a -> String
expected Set Kind
sk Set Kind
ks)
        (Range -> Diagnosis) -> Range -> Diagnosis
forall a b. (a -> b) -> a -> b
$ Type -> Range
forall a. GetRange a => a -> Range
getRange Type
ty] (Maybe (Set Kind) -> Result (Set Kind))
-> Maybe (Set Kind) -> Result (Set Kind)
forall a b. (a -> b) -> a -> b
$ if DiagKind
dk DiagKind -> DiagKind -> Bool
forall a. Eq a => a -> a -> Bool
== DiagKind
Error then Maybe (Set Kind)
forall a. Maybe a
Nothing else Set Kind -> Maybe (Set Kind)
forall a. a -> Maybe a
Just Set Kind
forall a. Set a
Set.empty

-- | add an analysed type argument (warn on redeclared types)
addTypeVarDecl :: Bool -> TypeArg -> State Env ()
addTypeVarDecl :: Bool -> TypeArg -> State Env ()
addTypeVarDecl warn :: Bool
warn (TypeArg i :: Id
i v :: Variance
v vk :: VarKind
vk rk :: RawKind
rk c :: Int
c _ _) =
       Bool -> TypeVarDefn -> Id -> State Env ()
addLocalTypeVar Bool
warn (Variance -> VarKind -> RawKind -> Int -> TypeVarDefn
TypeVarDefn Variance
v VarKind
vk RawKind
rk Int
c) Id
i

addLocalTypeVar :: Bool -> TypeVarDefn -> Id -> State Env ()
addLocalTypeVar :: Bool -> TypeVarDefn -> Id -> State Env ()
addLocalTypeVar warn :: Bool
warn tvd :: TypeVarDefn
tvd i :: Id
i = do
    Env
e <- State Env Env
forall s. State s s
get
    let tvs :: Map Id TypeVarDefn
tvs = Env -> Map Id TypeVarDefn
localTypeVars Env
e
    Bool -> State Env () -> State Env ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when Bool
warn (State Env () -> State Env ()) -> State Env () -> State Env ()
forall a b. (a -> b) -> a -> b
$ do
       Bool -> State Env () -> State Env ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Id -> Map Id TypeInfo -> Bool
forall k a. Ord k => k -> Map k a -> Bool
Map.member Id
i (Map Id TypeInfo -> Bool) -> Map Id TypeInfo -> Bool
forall a b. (a -> b) -> a -> b
$ Env -> Map Id TypeInfo
typeMap Env
e)
         (State Env () -> State Env ()) -> State Env () -> State Env ()
forall a b. (a -> b) -> a -> b
$ [Diagnosis] -> State Env ()
addDiags [DiagKind -> String -> Id -> Diagnosis
forall a.
(GetRange a, Pretty a) =>
DiagKind -> String -> a -> Diagnosis
mkDiag DiagKind
Warning
           "type variable shadows type constructor" Id
i]
       Bool -> State Env () -> State Env ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Id -> Map Id TypeVarDefn -> Bool
forall k a. Ord k => k -> Map k a -> Bool
Map.member Id
i Map Id TypeVarDefn
tvs)
         (State Env () -> State Env ()) -> State Env () -> State Env ()
forall a b. (a -> b) -> a -> b
$ [Diagnosis] -> State Env ()
addDiags [DiagKind -> String -> Id -> Diagnosis
forall a.
(GetRange a, Pretty a) =>
DiagKind -> String -> a -> Diagnosis
mkDiag DiagKind
Hint "rebound type variable" Id
i]
       Bool -> State Env () -> State Env ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Id -> Map Id VarDefn -> Bool
forall k a. Ord k => k -> Map k a -> Bool
Map.member Id
i (Map Id VarDefn -> Bool) -> Map Id VarDefn -> Bool
forall a b. (a -> b) -> a -> b
$ Env -> Map Id VarDefn
localVars Env
e)
         (State Env () -> State Env ()) -> State Env () -> State Env ()
forall a b. (a -> b) -> a -> b
$ [Diagnosis] -> State Env ()
addDiags [DiagKind -> String -> Id -> Diagnosis
forall a.
(GetRange a, Pretty a) =>
DiagKind -> String -> a -> Diagnosis
mkDiag DiagKind
Warning
           "type variable does not shadow normal variable" Id
i]
    Map Id TypeVarDefn -> State Env ()
putLocalTypeVars (Map Id TypeVarDefn -> State Env ())
-> Map Id TypeVarDefn -> State Env ()
forall a b. (a -> b) -> a -> b
$ Id -> TypeVarDefn -> Map Id TypeVarDefn -> Map Id TypeVarDefn
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert Id
i TypeVarDefn
tvd Map Id TypeVarDefn
tvs

-- | infer all minimal kinds
inferKinds :: Maybe Bool -> Type -> Env
           -> Result ((RawKind, Set.Set Kind), Type)
inferKinds :: Maybe Bool -> Type -> Env -> Result ((RawKind, Set Kind), Type)
inferKinds b :: Maybe Bool
b ty :: Type
ty te :: Env
te@Env {classMap :: Env -> ClassMap
classMap = ClassMap
cm} = case Type
ty of
    TypeName i :: Id
i _ _ -> Maybe Bool -> Env -> Id -> Result ((RawKind, Set Kind), Type)
getCoVarKind Maybe Bool
b Env
te Id
i
    TypeAppl t1 :: Type
t1 t2 :: Type
t2 -> do
       ((rk :: RawKind
rk, ks :: Set Kind
ks), t3 :: Type
t3) <- Maybe Bool -> Type -> Env -> Result ((RawKind, Set Kind), Type)
inferKinds Maybe Bool
b Type
t1 Env
te
       case RawKind
rk of
           FunKind v :: Variance
v _ rr :: RawKind
rr _ -> do
               ((_, l :: Set Kind
l), t4 :: Type
t4) <- Maybe Bool -> Type -> Env -> Result ((RawKind, Set Kind), Type)
inferKinds (case Variance
v of
                            ContraVar -> Bool -> Maybe Bool
forall a. a -> Maybe a
Just (Bool -> Maybe Bool) -> Bool -> Maybe Bool
forall a b. (a -> b) -> a -> b
$ Bool -> (Bool -> Bool) -> Maybe Bool -> Bool
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Bool
False Bool -> Bool
not Maybe Bool
b
                            CoVar -> Bool -> Maybe Bool
forall a. a -> Maybe a
Just (Bool -> Maybe Bool) -> Bool -> Maybe Bool
forall a b. (a -> b) -> a -> b
$ Bool -> Maybe Bool -> Bool
forall a. a -> Maybe a -> a
fromMaybe Bool
True Maybe Bool
b
                            _ -> Maybe Bool
forall a. Maybe a
Nothing) Type
t2 Env
te
               [Set Kind]
kks <- (Kind -> Result (Set Kind)) -> [Kind] -> Result [Set Kind]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (ClassMap -> Kind -> Result (Set Kind)
forall (m :: * -> *).
MonadFail m =>
ClassMap -> Kind -> m (Set Kind)
getFunKinds ClassMap
cm) ([Kind] -> Result [Set Kind]) -> [Kind] -> Result [Set Kind]
forall a b. (a -> b) -> a -> b
$ Set Kind -> [Kind]
forall a. Set a -> [a]
Set.toList Set Kind
ks
               [Set Kind]
rs <- (Kind -> Result (Set Kind)) -> [Kind] -> Result [Set Kind]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM ( \ fk :: Kind
fk -> case Kind
fk of
                    FunKind _ arg :: Kind
arg res :: Kind
res _ -> DiagKind
-> ClassMap
-> Type
-> Set Kind
-> Set Kind
-> Set Kind
-> Result (Set Kind)
subKinds DiagKind
Hint ClassMap
cm Type
t2
                        (Kind -> Set Kind
forall a. a -> Set a
Set.singleton Kind
arg) Set Kind
l (Set Kind -> Result (Set Kind)) -> Set Kind -> Result (Set Kind)
forall a b. (a -> b) -> a -> b
$ Kind -> Set Kind
forall a. a -> Set a
Set.singleton Kind
res
                    _ -> String -> Result (Set Kind)
forall a. HasCallStack => String -> a
error "inferKinds: no function kind"
                  ) ([Kind] -> Result [Set Kind]) -> [Kind] -> Result [Set Kind]
forall a b. (a -> b) -> a -> b
$ Set Kind -> [Kind]
forall a. Set a -> [a]
Set.toList (Set Kind -> [Kind]) -> Set Kind -> [Kind]
forall a b. (a -> b) -> a -> b
$ ClassMap -> [Set Kind] -> Set Kind
keepMinKinds ClassMap
cm [Set Kind]
kks
               ((RawKind, Set Kind), Type) -> Result ((RawKind, Set Kind), Type)
forall (m :: * -> *) a. Monad m => a -> m a
return ((RawKind
rr, ClassMap -> [Set Kind] -> Set Kind
keepMinKinds ClassMap
cm [Set Kind]
rs), Type -> Type -> Type
TypeAppl Type
t3 Type
t4)
           _ -> String -> Type -> Result ((RawKind, Set Kind), Type)
forall a b. (GetRange a, Pretty a) => String -> a -> Result b
mkError "unexpected type argument" Type
t2
    TypeAbs ta :: TypeArg
ta@(TypeArg _ v :: Variance
v k :: VarKind
k r :: RawKind
r _ _ q :: Range
q) t :: Type
t ps :: Range
ps -> do
        let newEnv :: Env
newEnv = State Env () -> Env -> Env
forall s a. State s a -> s -> s
execState (Bool -> TypeArg -> State Env ()
addTypeVarDecl Bool
False TypeArg
ta) Env
te
        ((rk :: RawKind
rk, ks :: Set Kind
ks), nt :: Type
nt) <- Maybe Bool -> Type -> Env -> Result ((RawKind, Set Kind), Type)
inferKinds Maybe Bool
forall a. Maybe a
Nothing Type
t Env
newEnv
        ((RawKind, Set Kind), Type) -> Result ((RawKind, Set Kind), Type)
forall (m :: * -> *) a. Monad m => a -> m a
return (( Variance -> RawKind -> RawKind -> Range -> RawKind
forall a. Variance -> AnyKind a -> AnyKind a -> Range -> AnyKind a
FunKind Variance
v RawKind
r RawKind
rk Range
q
                , ClassMap -> [Set Kind] -> Set Kind
keepMinKinds ClassMap
cm
                  [(Kind -> Kind) -> Set Kind -> Set Kind
forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map (\ j :: Kind
j -> Variance -> Kind -> Kind -> Range -> Kind
forall a. Variance -> AnyKind a -> AnyKind a -> Range -> AnyKind a
FunKind Variance
v (VarKind -> Kind
toKind VarKind
k) Kind
j Range
q) Set Kind
ks])
               , TypeArg -> Type -> Range -> Type
TypeAbs TypeArg
ta Type
nt Range
ps)
    KindedType kt :: Type
kt kind :: Set Kind
kind ps :: Range
ps -> do
        let Result ds :: [Diagnosis]
ds _ = (Kind -> Result RawKind) -> [Kind] -> Result [RawKind]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (Kind -> ClassMap -> Result RawKind
`anaKindM` ClassMap
cm) ([Kind] -> Result [RawKind]) -> [Kind] -> Result [RawKind]
forall a b. (a -> b) -> a -> b
$ Set Kind -> [Kind]
forall a. Set a -> [a]
Set.toList Set Kind
kind
        Set Kind
sk <- if [Diagnosis] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Diagnosis]
ds then Set Kind -> Result (Set Kind)
forall (m :: * -> *) a. Monad m => a -> m a
return Set Kind
kind else [Diagnosis] -> Maybe (Set Kind) -> Result (Set Kind)
forall a. [Diagnosis] -> Maybe a -> Result a
Result [Diagnosis]
ds Maybe (Set Kind)
forall a. Maybe a
Nothing
        ((rk :: RawKind
rk, ks :: Set Kind
ks), t :: Type
t) <- Maybe Bool -> Type -> Env -> Result ((RawKind, Set Kind), Type)
inferKinds Maybe Bool
b Type
kt Env
te
        Set Kind
l <- DiagKind
-> ClassMap
-> Type
-> Set Kind
-> Set Kind
-> Set Kind
-> Result (Set Kind)
subKinds DiagKind
Hint ClassMap
cm Type
kt Set Kind
sk Set Kind
ks Set Kind
sk
        ((RawKind, Set Kind), Type) -> Result ((RawKind, Set Kind), Type)
forall (m :: * -> *) a. Monad m => a -> m a
return ((RawKind
rk, Set Kind
l), Type -> Set Kind -> Range -> Type
KindedType Type
t Set Kind
sk Range
ps)
    ExpandedType t1 :: Type
t1 t2 :: Type
t2 -> do
        ((rk1 :: RawKind
rk1, ks :: Set Kind
ks), t4 :: Type
t4) <- Maybe Bool -> Type -> Env -> Result ((RawKind, Set Kind), Type)
inferKinds Maybe Bool
b Type
t2 Env
te
        ((rk2 :: RawKind
rk2, aks :: Set Kind
aks), t3 :: Type
t3) <- Maybe Bool -> Type -> Env -> Result ((RawKind, Set Kind), Type)
inferKinds Maybe Bool
b Type
t1 Env
te
        RawKind
rk <- Result RawKind
-> (RawKind -> Result RawKind) -> Maybe RawKind -> Result RawKind
forall b a. b -> (a -> b) -> Maybe a -> b
maybe ([Diagnosis] -> Maybe RawKind -> Result RawKind
forall a. [Diagnosis] -> Maybe a -> Result a
Result (Type -> RawKind -> RawKind -> [Diagnosis]
forall a.
(GetRange a, Pretty a) =>
a -> RawKind -> RawKind -> [Diagnosis]
diffKindDiag Type
ty RawKind
rk1 RawKind
rk2) Maybe RawKind
forall a. Maybe a
Nothing) RawKind -> Result RawKind
forall (m :: * -> *) a. Monad m => a -> m a
return
              (Maybe RawKind -> Result RawKind)
-> Maybe RawKind -> Result RawKind
forall a b. (a -> b) -> a -> b
$ String -> RawKind -> RawKind -> Maybe RawKind
forall (m :: * -> *).
MonadFail m =>
String -> RawKind -> RawKind -> m RawKind
minRawKind "" RawKind
rk1 RawKind
rk2
        ((RawKind, Set Kind), Type) -> Result ((RawKind, Set Kind), Type)
forall (m :: * -> *) a. Monad m => a -> m a
return ((RawKind
rk, ClassMap -> [Set Kind] -> Set Kind
keepMinKinds ClassMap
cm [Set Kind
aks, Set Kind
ks]), Type -> Type -> Type
ExpandedType Type
t3 Type
t4)
    _ -> String -> Result ((RawKind, Set Kind), Type)
forall a. HasCallStack => String -> a
error "inferKinds"

-- | extract the raw kind from a type term
rawKindOfType :: Type -> RawKind
rawKindOfType :: Type -> RawKind
rawKindOfType = FoldTypeRec RawKind -> Type -> RawKind
forall a. FoldTypeRec a -> Type -> a
foldType FoldTypeRec :: forall a.
(Type -> Id -> RawKind -> Int -> a)
-> (Type -> a -> a -> a)
-> (Type -> a -> a -> a)
-> (Type -> TypeArg -> a -> Range -> a)
-> (Type -> a -> Set Kind -> Range -> a)
-> (Type -> Token -> a)
-> (Type -> BracketKind -> [a] -> Range -> a)
-> (Type -> [a] -> a)
-> FoldTypeRec a
FoldTypeRec
  { foldTypeName :: Type -> Id -> RawKind -> Int -> RawKind
foldTypeName = \ _ _ k :: RawKind
k _ -> RawKind
k
  , foldTypeAppl :: Type -> RawKind -> RawKind -> RawKind
foldTypeAppl = \ _ ka :: RawKind
ka _ -> case RawKind
ka of
        FunKind _ _ k :: RawKind
k _ -> RawKind
k
        _ -> String -> RawKind
forall a. HasCallStack => String -> a
error "rawKindOfType"
  , foldExpandedType :: Type -> RawKind -> RawKind -> RawKind
foldExpandedType = \ _ k1 :: RawKind
k1 ->
        RawKind -> Maybe RawKind -> RawKind
forall a. a -> Maybe a -> a
fromMaybe (String -> RawKind
forall a. HasCallStack => String -> a
error "rawKindOfType.foldExpandedType") (Maybe RawKind -> RawKind)
-> (RawKind -> Maybe RawKind) -> RawKind -> RawKind
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> RawKind -> RawKind -> Maybe RawKind
forall (m :: * -> *).
MonadFail m =>
String -> RawKind -> RawKind -> m RawKind
minRawKind "" RawKind
k1
  , foldTypeAbs :: Type -> TypeArg -> RawKind -> Range -> RawKind
foldTypeAbs = \ _ (TypeArg _ v :: Variance
v _ r :: RawKind
r _ _ _) -> Variance -> RawKind -> RawKind -> Range -> RawKind
forall a. Variance -> AnyKind a -> AnyKind a -> Range -> AnyKind a
FunKind Variance
v RawKind
r
  , foldKindedType :: Type -> RawKind -> Set Kind -> Range -> RawKind
foldKindedType = \ _ k :: RawKind
k _ _ -> RawKind
k
  , foldTypeToken :: Type -> Token -> RawKind
foldTypeToken = \ _ _ -> RawKind
rStar
  , foldBracketType :: Type -> BracketKind -> [RawKind] -> Range -> RawKind
foldBracketType = \ _ _ _ _ -> RawKind
rStar
  , foldMixfixType :: Type -> [RawKind] -> RawKind
foldMixfixType = \ _ _ -> RawKind
rStar }

-- | subtyping relation
lesserType :: Env -> Type -> Type -> Bool
lesserType :: Env -> Type -> Type -> Bool
lesserType te :: Env
te t1 :: Type
t1 t2 :: Type
t2 = case (Type
t1, Type
t2) of
    (KindedType t :: Type
t _ _, _) -> Env -> Type -> Type -> Bool
lesserType Env
te Type
t Type
t2
    (ExpandedType _ t :: Type
t, _) -> Env -> Type -> Type -> Bool
lesserType Env
te Type
t Type
t2
    (_, KindedType t :: Type
t _ _) -> Env -> Type -> Type -> Bool
lesserType Env
te Type
t1 Type
t
    (_, ExpandedType _ t :: Type
t) -> Env -> Type -> Type -> Bool
lesserType Env
te Type
t1 Type
t
    (TypeName {}, TypeAppl (TypeName l :: Id
l _ _) t :: Type
t) | Id
l Id -> Id -> Bool
forall a. Eq a => a -> a -> Bool
== Id
lazyTypeId ->
       Env -> Type -> Type -> Bool
lesserType Env
te Type
t1 Type
t
    (TypeAppl c1 :: Type
c1 a1 :: Type
a1, TypeAppl c2 :: Type
c2 a2 :: Type
a2) ->
        let b1 :: Bool
b1 = Env -> Type -> Type -> Bool
lesserType Env
te Type
a1 Type
a2
            b2 :: Bool
b2 = Env -> Type -> Type -> Bool
lesserType Env
te Type
a2 Type
a1
            b :: Bool
b = Bool
b1 Bool -> Bool -> Bool
&& Bool
b2
        in (case (Type -> RawKind
rawKindOfType Type
c1, Type -> RawKind
rawKindOfType Type
c2) of
            (FunKind v1 :: Variance
v1 _ _ _, FunKind v2 :: Variance
v2 _ _ _) ->
                if Variance
v1 Variance -> Variance -> Bool
forall a. Eq a => a -> a -> Bool
== Variance
v2 then case Variance
v1 of
                            CoVar -> Bool
b1
                            ContraVar -> Bool
b2
                            _ -> Bool
b
                        else Bool
b
            _ -> String -> Bool
forall a. HasCallStack => String -> a
error "lesserType: no FunKind") Bool -> Bool -> Bool
&& Env -> Type -> Type -> Bool
lesserType Env
te Type
c1 Type
c2
        Bool -> Bool -> Bool
|| case Type
c2 of
             (TypeName l :: Id
l _ _) | Id
l Id -> Id -> Bool
forall a. Eq a => a -> a -> Bool
== Id
lazyTypeId -> Env -> Type -> Type -> Bool
lesserType Env
te Type
t1 Type
a2
             _ -> Bool
False
    (TypeName i1 :: Id
i1 _ _, TypeName i2 :: Id
i2 _ _) | Id
i1 Id -> Id -> Bool
forall a. Eq a => a -> a -> Bool
== Id
i2 -> Bool
True
    (TypeName i :: Id
i k :: RawKind
k _, _) -> case Id -> Map Id TypeVarDefn -> Maybe TypeVarDefn
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Id
i (Map Id TypeVarDefn -> Maybe TypeVarDefn)
-> Map Id TypeVarDefn -> Maybe TypeVarDefn
forall a b. (a -> b) -> a -> b
$ Env -> Map Id TypeVarDefn
localTypeVars Env
te of
        Nothing -> case Id -> Map Id TypeInfo -> Maybe TypeInfo
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Id
i (Map Id TypeInfo -> Maybe TypeInfo)
-> Map Id TypeInfo -> Maybe TypeInfo
forall a b. (a -> b) -> a -> b
$ Env -> Map Id TypeInfo
typeMap Env
te of
            Nothing -> Bool
False
            Just ti :: TypeInfo
ti -> (Id -> Bool) -> [Id] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any ( \ j :: Id
j -> Env -> Type -> Type -> Bool
lesserType Env
te (Id -> RawKind -> Int -> Type
TypeName Id
j RawKind
k 0) Type
t2) ([Id] -> Bool) -> [Id] -> Bool
forall a b. (a -> b) -> a -> b
$
                       Set Id -> [Id]
forall a. Set a -> [a]
Set.toList (Set Id -> [Id]) -> Set Id -> [Id]
forall a b. (a -> b) -> a -> b
$ TypeInfo -> Set Id
superTypes TypeInfo
ti
        Just (TypeVarDefn _ vk :: VarKind
vk _ _) -> case VarKind
vk of
            Downset t :: Type
t -> Env -> Type -> Type -> Bool
lesserType Env
te Type
t Type
t2
            _ -> Bool
False
    (TypeAppl _ _, TypeName {}) -> Bool
False
    (TypeAppl _ _, TypeAbs {}) -> Bool
False
    (TypeAbs {}, TypeName {}) -> Bool
False
    (t3 :: Type
t3, t4 :: Type
t4) -> Type
t3 Type -> Type -> Bool
forall a. Eq a => a -> a -> Bool
== Type
t4

lesserTypeScheme :: Env -> TypeScheme -> TypeScheme -> Bool
lesserTypeScheme :: Env -> TypeScheme -> TypeScheme -> Bool
lesserTypeScheme e :: Env
e (TypeScheme args1 :: [TypeArg]
args1 t1 :: Type
t1 _) (TypeScheme args2 :: [TypeArg]
args2 t2 :: Type
t2 _) =
   [TypeArg] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [TypeArg]
args1 Bool -> Bool -> Bool
&& [TypeArg] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [TypeArg]
args2 Bool -> Bool -> Bool
&& Env -> Type -> Type -> Bool
lesserType Env
e Type
t1 Type
t2

lesserOpInfo :: Env -> OpInfo -> OpInfo -> Bool
lesserOpInfo :: Env -> OpInfo -> OpInfo -> Bool
lesserOpInfo e :: Env
e o1 :: OpInfo
o1 = Env -> TypeScheme -> TypeScheme -> Bool
lesserTypeScheme Env
e (OpInfo -> TypeScheme
opType OpInfo
o1) (TypeScheme -> Bool) -> (OpInfo -> TypeScheme) -> OpInfo -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. OpInfo -> TypeScheme
opType

-- | get operations by name removing super profiles
getMinAssumps :: Env -> Id -> [OpInfo]
getMinAssumps :: Env -> Id -> [OpInfo]
getMinAssumps e :: Env
e i :: Id
i = (OpInfo -> OpInfo -> Bool) -> [OpInfo] -> [OpInfo]
forall a. (a -> a -> Bool) -> [a] -> [a]
keepMins (Env -> OpInfo -> OpInfo -> Bool
lesserOpInfo Env
e) ([OpInfo] -> [OpInfo]) -> [OpInfo] -> [OpInfo]
forall a b. (a -> b) -> a -> b
$ Set OpInfo -> [OpInfo]
forall a. Set a -> [a]
Set.toList
  (Set OpInfo -> [OpInfo]) -> Set OpInfo -> [OpInfo]
forall a b. (a -> b) -> a -> b
$ Set OpInfo -> Id -> Map Id (Set OpInfo) -> Set OpInfo
forall k a. Ord k => a -> k -> Map k a -> a
Map.findWithDefault Set OpInfo
forall a. Set a
Set.empty Id
i (Map Id (Set OpInfo) -> Set OpInfo)
-> Map Id (Set OpInfo) -> Set OpInfo
forall a b. (a -> b) -> a -> b
$ Env -> Map Id (Set OpInfo)
assumps Env
e

-- | type identifiers of a type
idsOf :: (Int -> Bool) -> Type -> Set.Set Id
idsOf :: (Int -> Bool) -> Type -> Set Id
idsOf b :: Int -> Bool
b = [Id] -> Set Id
forall a. Ord a => [a] -> Set a
Set.fromList ([Id] -> Set Id) -> (Type -> [Id]) -> Type -> Set Id
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((Int, (Id, RawKind)) -> Id) -> [(Int, (Id, RawKind))] -> [Id]
forall a b. (a -> b) -> [a] -> [b]
map ((Id, RawKind) -> Id
forall a b. (a, b) -> a
fst ((Id, RawKind) -> Id)
-> ((Int, (Id, RawKind)) -> (Id, RawKind))
-> (Int, (Id, RawKind))
-> Id
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Int, (Id, RawKind)) -> (Id, RawKind)
forall a b. (a, b) -> b
snd) ([(Int, (Id, RawKind))] -> [Id])
-> (Type -> [(Int, (Id, RawKind))]) -> Type -> [Id]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Int -> Bool) -> Type -> [(Int, (Id, RawKind))]
leaves Int -> Bool
b

-- * super type ids

-- | compute super type ids of one type id
superIds :: TypeMap -> Id -> Set.Set Id
superIds :: Map Id TypeInfo -> Id -> Set Id
superIds tm :: Map Id TypeInfo
tm = Map Id TypeInfo -> Set Id -> Set Id -> Set Id
supIds Map Id TypeInfo
tm Set Id
forall a. Set a
Set.empty (Set Id -> Set Id) -> (Id -> Set Id) -> Id -> Set Id
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Id -> Set Id
forall a. a -> Set a
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 :: Map Id TypeInfo -> Set Id -> Set Id -> Set Id
supIds tm :: Map Id TypeInfo
tm known :: Set Id
known new :: Set Id
new =
    if Set Id -> Bool
forall a. Set a -> Bool
Set.null Set Id
new then Set Id
known else
       let more :: Set Id
more = [Set Id] -> Set Id
forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
Set.unions ([Set Id] -> Set Id) -> [Set Id] -> Set Id
forall a b. (a -> b) -> a -> b
$ (Id -> Set Id) -> [Id] -> [Set Id]
forall a b. (a -> b) -> [a] -> [b]
map ( \ i :: Id
i -> TypeInfo -> Set Id
superTypes
                            (TypeInfo -> Set Id) -> TypeInfo -> Set Id
forall a b. (a -> b) -> a -> b
$ TypeInfo -> Id -> Map Id TypeInfo -> TypeInfo
forall k a. Ord k => a -> k -> Map k a -> a
Map.findWithDefault TypeInfo
starTypeInfo Id
i Map Id TypeInfo
tm)
                  ([Id] -> [Set Id]) -> [Id] -> [Set Id]
forall a b. (a -> b) -> a -> b
$ Set Id -> [Id]
forall a. Set a -> [a]
Set.toList Set Id
new
           newKnown :: Set Id
newKnown = Set Id -> Set Id -> Set Id
forall a. Ord a => Set a -> Set a -> Set a
Set.union Set Id
known Set Id
new
    in Map Id TypeInfo -> Set Id -> Set Id -> Set Id
supIds Map Id TypeInfo
tm Set Id
newKnown (Set Id
more Set Id -> Set Id -> Set Id
forall a. Ord a => Set a -> Set a -> Set a
Set.\\ Set Id
newKnown)

-- * expand alias types

-- | expand aliases in a type scheme
expand :: TypeMap -> TypeScheme -> TypeScheme
expand :: Map Id TypeInfo -> TypeScheme -> TypeScheme
expand = (Type -> Type) -> TypeScheme -> TypeScheme
mapTypeOfScheme ((Type -> Type) -> TypeScheme -> TypeScheme)
-> (Map Id TypeInfo -> Type -> Type)
-> Map Id TypeInfo
-> TypeScheme
-> TypeScheme
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Map Id TypeInfo -> Type -> Type
expandAliases

filterAliases :: TypeMap -> TypeMap
filterAliases :: Map Id TypeInfo -> Map Id TypeInfo
filterAliases = (TypeInfo -> Bool) -> Map Id TypeInfo -> Map Id TypeInfo
forall a k. (a -> Bool) -> Map k a -> Map k a
Map.filter ( \ ti :: TypeInfo
ti -> case TypeInfo -> TypeDefn
typeDefn TypeInfo
ti of
         AliasTypeDefn _ -> Bool
True
         _ -> Bool
False)

-- | expand aliases in a type and reduce type map first
expandAlias :: TypeMap -> Type -> Type
expandAlias :: Map Id TypeInfo -> Type -> Type
expandAlias = Map Id TypeInfo -> Type -> Type
expandAliases (Map Id TypeInfo -> Type -> Type)
-> (Map Id TypeInfo -> Map Id TypeInfo)
-> Map Id TypeInfo
-> Type
-> Type
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Map Id TypeInfo -> Map Id TypeInfo
filterAliases

-- | expand aliases in a type if type map non-null
expandAliases :: TypeMap -> Type -> Type
expandAliases :: Map Id TypeInfo -> Type -> Type
expandAliases tm :: Map Id TypeInfo
tm = if Map Id TypeInfo -> Bool
forall k a. Map k a -> Bool
Map.null Map Id TypeInfo
tm then Type -> Type
forall a. a -> a
id else Map Id TypeInfo -> Type -> Type
expandAux Map Id TypeInfo
tm

-- | expand aliases in a type
expandAux :: TypeMap -> Type -> Type
expandAux :: Map Id TypeInfo -> Type -> Type
expandAux tm :: Map Id TypeInfo
tm = (Id -> RawKind -> Int -> Type) -> Type -> Type
replAlias ((Id -> RawKind -> Int -> Type) -> Type -> Type)
-> (Id -> RawKind -> Int -> Type) -> Type -> Type
forall a b. (a -> b) -> a -> b
$ \ i :: Id
i k :: RawKind
k n :: Int
n -> case Id -> Map Id TypeInfo -> Maybe TypeInfo
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Id
i Map Id TypeInfo
tm of
    Just TypeInfo {typeDefn :: TypeInfo -> TypeDefn
typeDefn = AliasTypeDefn s :: Type
s} ->
        Type -> Type -> Type
ExpandedType (Id -> RawKind -> Int -> Type
TypeName Id
i RawKind
k Int
n) Type
s
    _ -> Id -> RawKind -> Int -> Type
TypeName Id
i RawKind
k Int
n

-- | find unexpanded alias identifier
hasAlias :: TypeMap -> Type -> [Diagnosis]
hasAlias :: Map Id TypeInfo -> Type -> [Diagnosis]
hasAlias tm :: Map Id TypeInfo
tm t :: Type
t =
     (Id -> Diagnosis) -> [Id] -> [Diagnosis]
forall a b. (a -> b) -> [a] -> [b]
map ( \ i :: Id
i -> DiagKind -> String -> Type -> Diagnosis
forall a.
(GetRange a, Pretty a) =>
DiagKind -> String -> a -> Diagnosis
mkDiag DiagKind
Error ("unexpanded alias '" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Id -> String -> String
showId Id
i "' in") Type
t)
     ([Id] -> [Diagnosis]) -> [Id] -> [Diagnosis]
forall a b. (a -> b) -> a -> b
$ Set Id -> [Id]
forall a. Set a -> [a]
Set.toList (Set Id -> [Id]) -> Set Id -> [Id]
forall a b. (a -> b) -> a -> b
$ Set Id -> Set Id -> Set Id
forall a. Ord a => Set a -> Set a -> Set a
Set.intersection ((Int -> Bool) -> Type -> Set Id
idsOf (Bool -> Int -> Bool
forall a b. a -> b -> a
const Bool
True) Type
t) (Set Id -> Set Id) -> Set Id -> Set Id
forall a b. (a -> b) -> a -> b
$
       Map Id TypeInfo -> Set Id
forall k a. Map k a -> Set k
Map.keysSet (Map Id TypeInfo -> Set Id) -> Map Id TypeInfo -> Set Id
forall a b. (a -> b) -> a -> b
$ Map Id TypeInfo -> Map Id TypeInfo
filterAliases Map Id TypeInfo
tm

-- * resolve and analyse types

-- | resolve type and infer minimal kinds
anaTypeM :: (Maybe Kind, Type) -> Env -> Result ((RawKind, Set.Set Kind), Type)
anaTypeM :: (Maybe Kind, Type) -> Env -> Result ((RawKind, Set Kind), Type)
anaTypeM (mk :: Maybe Kind
mk, parsedType :: Type
parsedType) te :: Env
te =
    do Type
resolvedType <- Env -> Type -> Result Type
mkTypeConstrAppl Env
te Type
parsedType
       let tm :: Map Id TypeInfo
tm = Env -> Map Id TypeInfo
typeMap Env
te
           adj :: Result a -> Result a
adj = Range -> Result a -> Result a
forall a. Range -> Result a -> Result a
adjustPos (Range -> Result a -> Result a) -> Range -> Result a -> Result a
forall a b. (a -> b) -> a -> b
$ Type -> Range
forall a. GetRange a => a -> Range
getRange Type
parsedType
           cm :: ClassMap
cm = Env -> ClassMap
classMap Env
te
       ((rk :: RawKind
rk, ks :: Set Kind
ks), checkedType :: Type
checkedType) <- Result ((RawKind, Set Kind), Type)
-> Result ((RawKind, Set Kind), Type)
forall a. Result a -> Result a
adj (Result ((RawKind, Set Kind), Type)
 -> Result ((RawKind, Set Kind), Type))
-> Result ((RawKind, Set Kind), Type)
-> Result ((RawKind, Set Kind), Type)
forall a b. (a -> b) -> a -> b
$ Maybe Bool -> Type -> Env -> Result ((RawKind, Set Kind), Type)
inferKinds Maybe Bool
forall a. Maybe a
Nothing Type
resolvedType Env
te
       Set Kind
l <- Result (Set Kind) -> Result (Set Kind)
forall a. Result a -> Result a
adj (Result (Set Kind) -> Result (Set Kind))
-> Result (Set Kind) -> Result (Set Kind)
forall a b. (a -> b) -> a -> b
$ case Maybe Kind
mk of
               Nothing -> DiagKind
-> ClassMap
-> Type
-> Set Kind
-> Set Kind
-> Set Kind
-> Result (Set Kind)
subKinds DiagKind
Error ClassMap
cm Type
parsedType
                 (if Set Kind -> Bool
forall a. Set a -> Bool
Set.null Set Kind
ks then Kind -> Set Kind
forall a. a -> Set a
Set.singleton Kind
universe else Set Kind
ks) Set Kind
ks Set Kind
ks
               Just k :: Kind
k -> DiagKind
-> ClassMap
-> Type
-> Set Kind
-> Set Kind
-> Set Kind
-> Result (Set Kind)
subKinds DiagKind
Error ClassMap
cm Type
parsedType (Kind -> Set Kind
forall a. a -> Set a
Set.singleton Kind
k) Set Kind
ks (Set Kind -> Result (Set Kind)) -> Set Kind -> Result (Set Kind)
forall a b. (a -> b) -> a -> b
$
                         (Kind -> Bool) -> Set Kind -> Set Kind
forall a. (a -> Bool) -> Set a -> Set a
Set.filter ((Kind -> Kind -> Bool) -> Kind -> Kind -> Bool
forall a b c. (a -> b -> c) -> b -> a -> c
flip (ClassMap -> Kind -> Kind -> Bool
lesserKind ClassMap
cm) Kind
k) Set Kind
ks
       let expandedType :: Type
expandedType = Map Id TypeInfo -> Type -> Type
expandAlias Map Id TypeInfo
tm Type
checkedType
       [Diagnosis] -> Maybe () -> Result ()
forall a. [Diagnosis] -> Maybe a -> Result a
Result (Map Id TypeInfo -> Type -> [Diagnosis]
hasAlias Map Id TypeInfo
tm Type
expandedType) (Maybe () -> Result ()) -> Maybe () -> Result ()
forall a b. (a -> b) -> a -> b
$ () -> Maybe ()
forall a. a -> Maybe a
Just ()
       ((RawKind, Set Kind), Type) -> Result ((RawKind, Set Kind), Type)
forall (m :: * -> *) a. Monad m => a -> m a
return ((RawKind
rk, Set Kind
l), Type
expandedType)

-- | resolve the type and check if it is of the universe class
anaStarTypeM :: Type -> Env -> Result ((RawKind, Set.Set Kind), Type)
anaStarTypeM :: Type -> Env -> Result ((RawKind, Set Kind), Type)
anaStarTypeM t :: Type
t = (Maybe Kind, Type) -> Env -> Result ((RawKind, Set Kind), Type)
anaTypeM (Kind -> Maybe Kind
forall a. a -> Maybe a
Just Kind
universe, Type
t)

-- * misc functions on types

-- | check if an id occurs in a type
cyclicType :: Id -> Type -> Bool
cyclicType :: Id -> Type -> Bool
cyclicType i :: Id
i = Id -> Set Id -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.member Id
i (Set Id -> Bool) -> (Type -> Set Id) -> Type -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Int -> Bool) -> Type -> Set Id
idsOf (Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== 0)

-- | check for unbound (or if False for too many) type variables
unboundTypevars :: Bool -> [TypeArg] -> Type -> [Diagnosis]
unboundTypevars :: Bool -> [TypeArg] -> Type -> [Diagnosis]
unboundTypevars b :: Bool
b args :: [TypeArg]
args ty :: Type
ty =
    let fvs :: [Id]
fvs = Type -> [Id]
freeTVarIds Type
ty
        argIds :: [Id]
argIds = (TypeArg -> Id) -> [TypeArg] -> [Id]
forall a b. (a -> b) -> [a] -> [b]
map TypeArg -> Id
getTypeVar [TypeArg]
args
        restVars1 :: [Id]
restVars1 = [Id]
fvs [Id] -> [Id] -> [Id]
forall a. Eq a => [a] -> [a] -> [a]
List.\\ [Id]
argIds
        restVars2 :: [Id]
restVars2 = [Id]
argIds [Id] -> [Id] -> [Id]
forall a. Eq a => [a] -> [a] -> [a]
List.\\ [Id]
fvs
    in (if [Id] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Id]
restVars1 then []
       else [DiagKind -> String -> Type -> Diagnosis
forall a.
(GetRange a, Pretty a) =>
DiagKind -> String -> a -> Diagnosis
mkDiag DiagKind
Error ("unbound type variable(s)\n  "
                                  String -> String -> String
forall a. [a] -> [a] -> [a]
++ (String -> String)
-> (Id -> String -> String) -> [Id] -> String -> String
forall a.
(String -> String)
-> (a -> String -> String) -> [a] -> String -> String
showSepList ("," String -> String -> String
forall a. [a] -> [a] -> [a]
++) Id -> String -> String
showId
                                  [Id]
restVars1 " in") Type
ty])
       [Diagnosis] -> [Diagnosis] -> [Diagnosis]
forall a. [a] -> [a] -> [a]
++ if Bool
b Bool -> Bool -> Bool
|| [Id] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Id]
restVars2 then [] else
            [DiagKind -> String -> Type -> Diagnosis
forall a.
(GetRange a, Pretty a) =>
DiagKind -> String -> a -> Diagnosis
mkDiag DiagKind
Warning ("ignoring unused variable(s)\n  "
                                  String -> String -> String
forall a. [a] -> [a] -> [a]
++ (String -> String)
-> (Id -> String -> String) -> [Id] -> String -> String
forall a.
(String -> String)
-> (a -> String -> String) -> [a] -> String -> String
showSepList ("," String -> String -> String
forall a. [a] -> [a] -> [a]
++) Id -> String -> String
showId
                                  [Id]
restVars2 " in") Type
ty]

-- | check for proper generalizability (False: warn also for unused types)
generalizable :: Bool -> TypeScheme -> [Diagnosis]
generalizable :: Bool -> TypeScheme -> [Diagnosis]
generalizable b :: Bool
b (TypeScheme args :: [TypeArg]
args ty :: Type
ty _) =
    Bool -> [TypeArg] -> Type -> [Diagnosis]
unboundTypevars Bool
b [TypeArg]
args Type
ty [Diagnosis] -> [Diagnosis] -> [Diagnosis]
forall a. [a] -> [a] -> [a]
++ [TypeArg] -> [Diagnosis]
checkUniqueTypevars [TypeArg]
args

-- | check uniqueness of type variables
checkUniqueTypevars :: [TypeArg] -> [Diagnosis]
checkUniqueTypevars :: [TypeArg] -> [Diagnosis]
checkUniqueTypevars = [Id] -> [Diagnosis]
forall a. (Pretty a, GetRange a, Ord a) => [a] -> [Diagnosis]
checkUniqueness ([Id] -> [Diagnosis])
-> ([TypeArg] -> [Id]) -> [TypeArg] -> [Diagnosis]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (TypeArg -> Id) -> [TypeArg] -> [Id]
forall a b. (a -> b) -> [a] -> [b]
map TypeArg -> Id
getTypeVar