{- |
Module      :  ./HasCASL/Constrain.hs
Description :  resolve type constraints
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

constraint resolution
-}

module HasCASL.Constrain
    ( Constraints
    , Constrain (..)
    , noC
    , substC
    , joinC
    , insertC
    , partitionC
    , toListC
    , shapeRelAndSimplify
    , fromTypeMap
    ) where

import HasCASL.Unify
import HasCASL.As
import HasCASL.FoldType
import HasCASL.AsUtils
import HasCASL.Le
import HasCASL.PrintLe ()
import HasCASL.TypeAna
import HasCASL.ClassAna
import HasCASL.VarDecl

import qualified Data.Set as Set
import qualified Data.Map as Map
import qualified Common.Lib.Rel as Rel
import Common.Lib.State
import Common.Doc
import Common.DocUtils
import Common.Id
import Common.Result
import Common.Utils

import Control.Exception (assert)
import Control.Monad
import qualified Control.Monad.Fail as Fail

import Data.List
import Data.Maybe

instance Pretty Constrain where
    pretty :: Constrain -> Doc
pretty c :: Constrain
c = case Constrain
c of
       Kinding ty :: Type
ty k :: Kind
k -> Type -> Doc
forall a. Pretty a => a -> Doc
pretty (Type -> Doc) -> Type -> Doc
forall a b. (a -> b) -> a -> b
$ Type -> Set Kind -> Range -> Type
KindedType Type
ty (Kind -> Set Kind
forall a. a -> Set a
Set.singleton Kind
k) Range
nullRange
       Subtyping t1 :: Type
t1 t2 :: Type
t2 -> [Doc] -> Doc
fsep [Type -> Doc
forall a. Pretty a => a -> Doc
pretty Type
t1, Doc
less Doc -> Doc -> Doc
<+> Type -> Doc
forall a. Pretty a => a -> Doc
pretty Type
t2]

instance GetRange Constrain where
  getRange :: Constrain -> Range
getRange c :: Constrain
c = case Constrain
c of
    Kinding ty :: Type
ty _ -> Type -> Range
forall a. GetRange a => a -> Range
getRange Type
ty
    Subtyping t1 :: Type
t1 t2 :: Type
t2 -> Type -> Range
forall a. GetRange a => a -> Range
getRange Type
t1 Range -> Range -> Range
`appRange` Type -> Range
forall a. GetRange a => a -> Range
getRange Type
t2

type Constraints = Set.Set Constrain

noC :: Constraints
noC :: Constraints
noC = Constraints
forall a. Set a
Set.empty

joinC :: Constraints -> Constraints -> Constraints
joinC :: Constraints -> Constraints -> Constraints
joinC = Constraints -> Constraints -> Constraints
forall a. Ord a => Set a -> Set a -> Set a
Set.union

noVars :: Constrain -> Bool
noVars :: Constrain -> Bool
noVars c :: Constrain
c = case Constrain
c of
  Kinding ty :: Type
ty _ -> [(Int, (Id, RawKind))] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null ([(Int, (Id, RawKind))] -> Bool) -> [(Int, (Id, RawKind))] -> Bool
forall a b. (a -> b) -> a -> b
$ Type -> [(Int, (Id, RawKind))]
freeTVars Type
ty
  Subtyping t1 :: Type
t1 t2 :: Type
t2 -> [(Int, (Id, RawKind))] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null (Type -> [(Int, (Id, RawKind))]
freeTVars Type
t1) Bool -> Bool -> Bool
&& [(Int, (Id, RawKind))] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null (Type -> [(Int, (Id, RawKind))]
freeTVars Type
t2)

partitionVarC :: Constraints -> (Constraints, Constraints)
partitionVarC :: Constraints -> (Constraints, Constraints)
partitionVarC = (Constrain -> Bool) -> Constraints -> (Constraints, Constraints)
forall a. (a -> Bool) -> Set a -> (Set a, Set a)
Set.partition Constrain -> Bool
noVars

insertC :: Constrain -> Constraints -> Constraints
insertC :: Constrain -> Constraints -> Constraints
insertC c :: Constrain
c = case Constrain
c of
            Subtyping t1 :: Type
t1 t2 :: Type
t2 -> if Type
t1 Type -> Type -> Bool
forall a. Eq a => a -> a -> Bool
== Type
t2 then Constraints -> Constraints
forall a. a -> a
id else Constrain -> Constraints -> Constraints
forall a. Ord a => a -> Set a -> Set a
Set.insert Constrain
c
            Kinding _ k :: Kind
k -> if Kind
k Kind -> Kind -> Bool
forall a. Eq a => a -> a -> Bool
== Kind
universe then Constraints -> Constraints
forall a. a -> a
id else Constrain -> Constraints -> Constraints
forall a. Ord a => a -> Set a -> Set a
Set.insert Constrain
c

substC :: Subst -> Constraints -> Constraints
substC :: Subst -> Constraints -> Constraints
substC s :: Subst
s = (Constrain -> Constraints -> Constraints)
-> Constraints -> Constraints -> Constraints
forall a b. (a -> b -> b) -> b -> Set a -> b
Set.fold (Constrain -> Constraints -> Constraints
insertC (Constrain -> Constraints -> Constraints)
-> (Constrain -> Constrain)
-> Constrain
-> Constraints
-> Constraints
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ( \ c :: Constrain
c -> case Constrain
c of
    Kinding ty :: Type
ty k :: Kind
k -> Type -> Kind -> Constrain
Kinding (Subst -> Type -> Type
subst Subst
s Type
ty) Kind
k
    Subtyping t1 :: Type
t1 t2 :: Type
t2 -> Type -> Type -> Constrain
Subtyping (Subst -> Type -> Type
subst Subst
s Type
t1) (Type -> Constrain) -> Type -> Constrain
forall a b. (a -> b) -> a -> b
$ Subst -> Type -> Type
subst Subst
s Type
t2)) Constraints
noC

simplify :: Env -> Constraints -> ([Diagnosis], Constraints)
simplify :: Env -> Constraints -> ([Diagnosis], Constraints)
simplify te :: Env
te rs :: Constraints
rs =
    if Constraints -> Bool
forall a. Set a -> Bool
Set.null Constraints
rs then ([], Constraints
noC)
    else let (r :: Constrain
r, rt :: Constraints
rt) = Constraints -> (Constrain, Constraints)
forall a. Set a -> (a, Set a)
Set.deleteFindMin Constraints
rs
             Result ds :: [Diagnosis]
ds m :: Maybe ()
m = Env -> Constrain -> Result ()
forall (m :: * -> *). MonadFail m => Env -> Constrain -> m ()
entail Env
te Constrain
r
             (es :: [Diagnosis]
es, cs :: Constraints
cs) = Env -> Constraints -> ([Diagnosis], Constraints)
simplify Env
te Constraints
rt
             in ([Diagnosis]
ds [Diagnosis] -> [Diagnosis] -> [Diagnosis]
forall a. [a] -> [a] -> [a]
++ [Diagnosis]
es, case Maybe ()
m of
                                 Just _ -> Constraints
cs
                                 Nothing -> Constrain -> Constraints -> Constraints
insertC Constrain
r Constraints
cs)

entail :: Fail.MonadFail m => Env -> Constrain -> m ()
entail :: Env -> Constrain -> m ()
entail te :: Env
te c :: Constrain
c = let cm :: ClassMap
cm = Env -> ClassMap
classMap Env
te in case Constrain
c of
    Kinding ty :: Type
ty k :: Kind
k -> if Kind
k Kind -> Kind -> Bool
forall a. Eq a => a -> a -> Bool
== Kind
universe then
                        Bool -> m () -> m ()
forall a. (?callStack::CallStack) => Bool -> a -> a
assert (Type -> RawKind
rawKindOfType Type
ty RawKind -> RawKind -> Bool
forall a. Eq a => a -> a -> Bool
== () -> RawKind
forall a. a -> AnyKind a
ClassKind ())
                    (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$ () -> m ()
forall (m :: * -> *) a. Monad m => a -> m a
return () else
      let Result _ds :: [Diagnosis]
_ds mk :: Maybe ((RawKind, Set Kind), Type)
mk = Maybe Bool -> Type -> Env -> Result ((RawKind, Set Kind), Type)
inferKinds Maybe Bool
forall a. Maybe a
Nothing Type
ty Env
te in
                   case Maybe ((RawKind, Set Kind), Type)
mk of
                   Nothing -> String -> m ()
forall (m :: * -> *) a. MonadFail m => String -> m a
Fail.fail (String -> m ()) -> String -> m ()
forall a b. (a -> b) -> a -> b
$ "constrain '" String -> String -> String
forall a. [a] -> [a] -> [a]
++
                                  Constrain -> String -> String
forall a. Pretty a => a -> String -> String
showDoc Constrain
c "' is unprovable"
                   Just ((_, ks :: Set Kind
ks), _) -> Bool -> m () -> m ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (ClassMap -> Kind -> Set Kind -> Bool
newKind ClassMap
cm Kind
k Set Kind
ks)
                       (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$ String -> m ()
forall (m :: * -> *) a. MonadFail m => String -> m a
Fail.fail (String -> m ()) -> String -> m ()
forall a b. (a -> b) -> a -> b
$ "constrain '" String -> String -> String
forall a. [a] -> [a] -> [a]
++
                           Constrain -> String -> String
forall a. Pretty a => a -> String -> String
showDoc Constrain
c "' is unprovable" String -> String -> String
forall a. [a] -> [a] -> [a]
++
                              if Set Kind -> Bool
forall a. Set a -> Bool
Set.null Set Kind
ks then "" else
                                  "\n  known kinds are: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Set Kind -> String -> String
forall a. Pretty a => a -> String -> String
showDoc Set Kind
ks ""
    Subtyping t1 :: Type
t1 t2 :: Type
t2 -> Bool -> m () -> m ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Env -> Type -> Type -> Bool
lesserType Env
te Type
t1 Type
t2)
                       (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$ String -> m ()
forall (m :: * -> *) a. MonadFail m => String -> m a
Fail.fail ("unable to prove: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Type -> String -> String
forall a. Pretty a => a -> String -> String
showDoc Type
t1 " < "
                                  String -> String -> String
forall a. [a] -> [a] -> [a]
++ Type -> String -> String
forall a. Pretty a => a -> String -> String
showDoc Type
t2 "")

freshLeaves :: Type -> State Int Type
freshLeaves :: Type -> State Int Type
freshLeaves ty :: Type
ty = case Type
ty of
    TypeName i :: Id
i k :: RawKind
k _ -> do
      (var :: Id
var, c :: Int
c) <- Id -> State Int (Id, Int)
freshVar Id
i
      Type -> State Int Type
forall (m :: * -> *) a. Monad m => a -> m a
return (Type -> State Int Type) -> Type -> State Int Type
forall a b. (a -> b) -> a -> b
$ Id -> RawKind -> Int -> Type
TypeName Id
var RawKind
k Int
c
    TypeAppl tl :: Type
tl@(TypeName l :: Id
l _ _) t :: Type
t | Id
l Id -> Id -> Bool
forall a. Eq a => a -> a -> Bool
== Id
lazyTypeId -> do
      Type
nt <- Type -> State Int Type
freshLeaves Type
t
      Type -> State Int Type
forall (m :: * -> *) a. Monad m => a -> m a
return (Type -> State Int Type) -> Type -> State Int Type
forall a b. (a -> b) -> a -> b
$ Type -> Type -> Type
TypeAppl Type
tl Type
nt
    TypeAppl f :: Type
f a :: Type
a -> case Type -> Maybe Type
redStep Type
ty of
        Just r :: Type
r -> Type -> State Int Type
freshLeaves Type
r
        Nothing -> do
          Type
nf <- Type -> State Int Type
freshLeaves Type
f
          Type
na <- Type -> State Int Type
freshLeaves Type
a
          Type -> State Int Type
forall (m :: * -> *) a. Monad m => a -> m a
return (Type -> State Int Type) -> Type -> State Int Type
forall a b. (a -> b) -> a -> b
$ Type -> Type -> Type
TypeAppl Type
nf Type
na
    KindedType t :: Type
t k :: Set Kind
k p :: Range
p -> do
      Type
nt <- Type -> State Int Type
freshLeaves Type
t
      Type -> State Int Type
forall (m :: * -> *) a. Monad m => a -> m a
return (Type -> State Int Type) -> Type -> State Int Type
forall a b. (a -> b) -> a -> b
$ Type -> Set Kind -> Range -> Type
KindedType Type
nt Set Kind
k Range
p
    ExpandedType _ t :: Type
t | Type -> Bool
noAbs Type
t -> Type -> State Int Type
freshLeaves Type
t
    ExpandedType e :: Type
e t :: Type
t -> do
      Type
ne <- Type -> State Int Type
freshLeaves Type
e
      Type
nt <- Type -> State Int Type
freshLeaves Type
t
      Type -> State Int Type
forall (m :: * -> *) a. Monad m => a -> m a
return (Type -> State Int Type) -> Type -> State Int Type
forall a b. (a -> b) -> a -> b
$ Type -> Type -> Type
ExpandedType Type
ne Type
nt
    TypeAbs {} -> Type -> State Int Type
forall (m :: * -> *) a. Monad m => a -> m a
return Type
ty
    _ -> String -> State Int Type
forall a. (?callStack::CallStack) => String -> a
error "freshLeaves"

substPairList :: Subst -> [(Type, Type)] -> [(Type, Type)]
substPairList :: Subst -> [(Type, Type)] -> [(Type, Type)]
substPairList s :: Subst
s = ((Type, Type) -> (Type, Type)) -> [(Type, Type)] -> [(Type, Type)]
forall a b. (a -> b) -> [a] -> [b]
map ( \ (a :: Type
a, b :: Type
b) -> (Subst -> Type -> Type
subst Subst
s Type
a, Subst -> Type -> Type
subst Subst
s Type
b))

isAtomic :: (Type, Type) -> Bool
isAtomic :: (Type, Type) -> Bool
isAtomic p :: (Type, Type)
p = case (Type, Type)
p of
    (TypeName {}, TypeName {}) -> Bool
True
    _ -> Bool
False

partEqShapes :: [(Type, Type)] -> [(Type, Type)]
partEqShapes :: [(Type, Type)] -> [(Type, Type)]
partEqShapes = ((Type, Type) -> Bool) -> [(Type, Type)] -> [(Type, Type)]
forall a. (a -> Bool) -> [a] -> [a]
filter ( \ p :: (Type, Type)
p -> case (Type, Type)
p of
    (TypeName _ _ n1 :: Int
n1, TypeName _ _ n2 :: Int
n2) -> Int
n1 Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
/= Int
n2
    _ -> Bool
True)

-- pre: shapeMatchPairList succeeds
shapeMgu :: [(Type, Type)] -> [(Type, Type)] -> State Int (Result Subst)
shapeMgu :: [(Type, Type)] -> [(Type, Type)] -> State Int (Result Subst)
shapeMgu knownAtoms :: [(Type, Type)]
knownAtoms cs :: [(Type, Type)]
cs = let (atoms :: [(Type, Type)]
atoms, sts :: [(Type, Type)]
sts) = ((Type, Type) -> Bool)
-> [(Type, Type)] -> ([(Type, Type)], [(Type, Type)])
forall a. (a -> Bool) -> [a] -> ([a], [a])
span (Type, Type) -> Bool
isAtomic [(Type, Type)]
cs in
  case [(Type, Type)]
sts of
  [] -> Result Subst -> State Int (Result Subst)
forall (m :: * -> *) a. Monad m => a -> m a
return (Result Subst -> State Int (Result Subst))
-> Result Subst -> State Int (Result Subst)
forall a b. (a -> b) -> a -> b
$ Subst -> Result Subst
forall (m :: * -> *) a. Monad m => a -> m a
return Subst
eps
  p :: (Type, Type)
p@(t1 :: Type
t1, t2 :: Type
t2) : tl :: [(Type, Type)]
tl -> let
   newKnowns :: [(Type, Type)]
newKnowns = [(Type, Type)]
knownAtoms [(Type, Type)] -> [(Type, Type)] -> [(Type, Type)]
forall a. [a] -> [a] -> [a]
++ [(Type, Type)] -> [(Type, Type)]
partEqShapes [(Type, Type)]
atoms
   rest :: [(Type, Type)]
rest = [(Type, Type)]
newKnowns [(Type, Type)] -> [(Type, Type)] -> [(Type, Type)]
forall a. [a] -> [a] -> [a]
++ [(Type, Type)]
tl
   in case (Type, Type)
p of
    (ExpandedType _ t :: Type
t, _) | Type -> Bool
noAbs Type
t -> [(Type, Type)] -> [(Type, Type)] -> State Int (Result Subst)
shapeMgu [(Type, Type)]
newKnowns ([(Type, Type)] -> State Int (Result Subst))
-> [(Type, Type)] -> State Int (Result Subst)
forall a b. (a -> b) -> a -> b
$ (Type
t, Type
t2) (Type, Type) -> [(Type, Type)] -> [(Type, Type)]
forall a. a -> [a] -> [a]
: [(Type, Type)]
tl
    (_, ExpandedType _ t :: Type
t) | Type -> Bool
noAbs Type
t -> [(Type, Type)] -> [(Type, Type)] -> State Int (Result Subst)
shapeMgu [(Type, Type)]
newKnowns ([(Type, Type)] -> State Int (Result Subst))
-> [(Type, Type)] -> State Int (Result Subst)
forall a b. (a -> b) -> a -> b
$ (Type
t1, Type
t) (Type, Type) -> [(Type, Type)] -> [(Type, Type)]
forall a. a -> [a] -> [a]
: [(Type, Type)]
tl
    (KindedType t :: Type
t _ _, _) -> [(Type, Type)] -> [(Type, Type)] -> State Int (Result Subst)
shapeMgu [(Type, Type)]
newKnowns ([(Type, Type)] -> State Int (Result Subst))
-> [(Type, Type)] -> State Int (Result Subst)
forall a b. (a -> b) -> a -> b
$ (Type
t, Type
t2) (Type, Type) -> [(Type, Type)] -> [(Type, Type)]
forall a. a -> [a] -> [a]
: [(Type, Type)]
tl
    (_, KindedType t :: Type
t _ _) -> [(Type, Type)] -> [(Type, Type)] -> State Int (Result Subst)
shapeMgu [(Type, Type)]
newKnowns ([(Type, Type)] -> State Int (Result Subst))
-> [(Type, Type)] -> State Int (Result Subst)
forall a b. (a -> b) -> a -> b
$ (Type
t1, Type
t) (Type, Type) -> [(Type, Type)] -> [(Type, Type)]
forall a. a -> [a] -> [a]
: [(Type, Type)]
tl
    (TypeAppl (TypeName l1 :: Id
l1 _ _) a1 :: Type
a1, TypeAppl (TypeName l2 :: Id
l2 _ _) a2 :: Type
a2)
        | Id
l1 Id -> Id -> Bool
forall a. Eq a => a -> a -> Bool
== Id
lazyTypeId Bool -> Bool -> Bool
&& Id
l2 Id -> Id -> Bool
forall a. Eq a => a -> a -> Bool
== Id
lazyTypeId ->
            [(Type, Type)] -> [(Type, Type)] -> State Int (Result Subst)
shapeMgu [(Type, Type)]
newKnowns ([(Type, Type)] -> State Int (Result Subst))
-> [(Type, Type)] -> State Int (Result Subst)
forall a b. (a -> b) -> a -> b
$ (Type
a1, Type
a2) (Type, Type) -> [(Type, Type)] -> [(Type, Type)]
forall a. a -> [a] -> [a]
: [(Type, Type)]
tl
    (TypeAppl (TypeName l :: Id
l _ _) t :: Type
t, TypeName {}) | Id
l Id -> Id -> Bool
forall a. Eq a => a -> a -> Bool
== Id
lazyTypeId ->
        [(Type, Type)] -> [(Type, Type)] -> State Int (Result Subst)
shapeMgu [(Type, Type)]
newKnowns ([(Type, Type)] -> State Int (Result Subst))
-> [(Type, Type)] -> State Int (Result Subst)
forall a b. (a -> b) -> a -> b
$ (Type
t, Type
t2) (Type, Type) -> [(Type, Type)] -> [(Type, Type)]
forall a. a -> [a] -> [a]
: [(Type, Type)]
tl
    (TypeName {}, TypeAppl (TypeName l :: Id
l _ _) t :: Type
t) | Id
l Id -> Id -> Bool
forall a. Eq a => a -> a -> Bool
== Id
lazyTypeId ->
        [(Type, Type)] -> [(Type, Type)] -> State Int (Result Subst)
shapeMgu [(Type, Type)]
newKnowns ([(Type, Type)] -> State Int (Result Subst))
-> [(Type, Type)] -> State Int (Result Subst)
forall a b. (a -> b) -> a -> b
$ (Type
t1, Type
t) (Type, Type) -> [(Type, Type)] -> [(Type, Type)]
forall a. a -> [a] -> [a]
: [(Type, Type)]
tl
    (TypeName _ _ v1 :: Int
v1, _) | Int
v1 Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> 0 -> do
             Type
vt <- Type -> State Int Type
freshLeaves Type
t2
             let s :: Subst
s = Int -> Type -> Subst
forall k a. k -> a -> Map k a
Map.singleton Int
v1 Type
vt
             Result ds :: [Diagnosis]
ds mr :: Maybe Subst
mr <- [(Type, Type)] -> [(Type, Type)] -> State Int (Result Subst)
shapeMgu [] ([(Type, Type)] -> State Int (Result Subst))
-> [(Type, Type)] -> State Int (Result Subst)
forall a b. (a -> b) -> a -> b
$ (Type
vt, Type
t2) (Type, Type) -> [(Type, Type)] -> [(Type, Type)]
forall a. a -> [a] -> [a]
: Subst -> [(Type, Type)] -> [(Type, Type)]
substPairList Subst
s [(Type, Type)]
rest
             case Maybe Subst
mr of
               Just r :: Subst
r -> Result Subst -> State Int (Result Subst)
forall (m :: * -> *) a. Monad m => a -> m a
return (Result Subst -> State Int (Result Subst))
-> Result Subst -> State Int (Result Subst)
forall a b. (a -> b) -> a -> b
$ Subst -> Result Subst
forall (m :: * -> *) a. Monad m => a -> m a
return (Subst -> Result Subst) -> Subst -> Result Subst
forall a b. (a -> b) -> a -> b
$ Subst -> Subst -> Subst
compSubst Subst
s Subst
r
               Nothing -> Result Subst -> State Int (Result Subst)
forall (m :: * -> *) a. Monad m => a -> m a
return (Result Subst -> State Int (Result Subst))
-> Result Subst -> State Int (Result Subst)
forall a b. (a -> b) -> a -> b
$ [Diagnosis] -> Maybe Subst -> Result Subst
forall a. [Diagnosis] -> Maybe a -> Result a
Result [Diagnosis]
ds Maybe Subst
forall a. Maybe a
Nothing
    (_, TypeName _ _ v2 :: Int
v2) | Int
v2 Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> 0 -> do
             Type
vt <- Type -> State Int Type
freshLeaves Type
t1
             let s :: Subst
s = Int -> Type -> Subst
forall k a. k -> a -> Map k a
Map.singleton Int
v2 Type
vt
             Result ds :: [Diagnosis]
ds mr :: Maybe Subst
mr <- [(Type, Type)] -> [(Type, Type)] -> State Int (Result Subst)
shapeMgu [] ([(Type, Type)] -> State Int (Result Subst))
-> [(Type, Type)] -> State Int (Result Subst)
forall a b. (a -> b) -> a -> b
$ (Type
t1, Type
vt) (Type, Type) -> [(Type, Type)] -> [(Type, Type)]
forall a. a -> [a] -> [a]
: Subst -> [(Type, Type)] -> [(Type, Type)]
substPairList Subst
s [(Type, Type)]
rest
             case Maybe Subst
mr of
               Just r :: Subst
r -> Result Subst -> State Int (Result Subst)
forall (m :: * -> *) a. Monad m => a -> m a
return (Result Subst -> State Int (Result Subst))
-> Result Subst -> State Int (Result Subst)
forall a b. (a -> b) -> a -> b
$ Subst -> Result Subst
forall (m :: * -> *) a. Monad m => a -> m a
return (Subst -> Result Subst) -> Subst -> Result Subst
forall a b. (a -> b) -> a -> b
$ Subst -> Subst -> Subst
compSubst Subst
s Subst
r
               Nothing -> Result Subst -> State Int (Result Subst)
forall (m :: * -> *) a. Monad m => a -> m a
return (Result Subst -> State Int (Result Subst))
-> Result Subst -> State Int (Result Subst)
forall a b. (a -> b) -> a -> b
$ [Diagnosis] -> Maybe Subst -> Result Subst
forall a. [Diagnosis] -> Maybe a -> Result a
Result [Diagnosis]
ds Maybe Subst
forall a. Maybe a
Nothing
    (TypeAppl f1 :: Type
f1 a1 :: Type
a1, TypeAppl f2 :: Type
f2 a2 :: Type
a2) -> case (Type
f1, Type
f2) of
      (_, TypeName l :: Id
l _ _) | Id
l Id -> Id -> Bool
forall a. Eq a => a -> a -> Bool
== Id
lazyTypeId ->
        [(Type, Type)] -> [(Type, Type)] -> State Int (Result Subst)
shapeMgu [(Type, Type)]
newKnowns ([(Type, Type)] -> State Int (Result Subst))
-> [(Type, Type)] -> State Int (Result Subst)
forall a b. (a -> b) -> a -> b
$ (Type
t1, Type
a2) (Type, Type) -> [(Type, Type)] -> [(Type, Type)]
forall a. a -> [a] -> [a]
: [(Type, Type)]
tl
      (TypeName l :: Id
l _ _, _) | Id
l Id -> Id -> Bool
forall a. Eq a => a -> a -> Bool
== Id
lazyTypeId ->
        [(Type, Type)] -> [(Type, Type)] -> State Int (Result Subst)
shapeMgu [(Type, Type)]
newKnowns ([(Type, Type)] -> State Int (Result Subst))
-> [(Type, Type)] -> State Int (Result Subst)
forall a b. (a -> b) -> a -> b
$ (Type
a1, Type
t2) (Type, Type) -> [(Type, Type)] -> [(Type, Type)]
forall a. a -> [a] -> [a]
: [(Type, Type)]
tl
      _ -> case Type -> Maybe Type
redStep Type
t1 of
        Just r1 :: Type
r1 -> [(Type, Type)] -> [(Type, Type)] -> State Int (Result Subst)
shapeMgu [(Type, Type)]
newKnowns ([(Type, Type)] -> State Int (Result Subst))
-> [(Type, Type)] -> State Int (Result Subst)
forall a b. (a -> b) -> a -> b
$ (Type
r1, Type
t2) (Type, Type) -> [(Type, Type)] -> [(Type, Type)]
forall a. a -> [a] -> [a]
: [(Type, Type)]
tl
        Nothing -> case Type -> Maybe Type
redStep Type
t2 of
          Just r2 :: Type
r2 -> [(Type, Type)] -> [(Type, Type)] -> State Int (Result Subst)
shapeMgu [(Type, Type)]
newKnowns ([(Type, Type)] -> State Int (Result Subst))
-> [(Type, Type)] -> State Int (Result Subst)
forall a b. (a -> b) -> a -> b
$ (Type
t1, Type
r2) (Type, Type) -> [(Type, Type)] -> [(Type, Type)]
forall a. a -> [a] -> [a]
: [(Type, Type)]
tl
          Nothing -> [(Type, Type)] -> [(Type, Type)] -> State Int (Result Subst)
shapeMgu [(Type, Type)]
newKnowns ([(Type, Type)] -> State Int (Result Subst))
-> [(Type, Type)] -> State Int (Result Subst)
forall a b. (a -> b) -> a -> b
$ (Type
f1, Type
f2) (Type, Type) -> [(Type, Type)] -> [(Type, Type)]
forall a. a -> [a] -> [a]
:
            case (Type -> RawKind
rawKindOfType Type
f1, Type -> RawKind
rawKindOfType Type
f2) of
                     (FunKind CoVar _ _ _,
                       FunKind CoVar _ _ _) -> (Type
a1, Type
a2) (Type, Type) -> [(Type, Type)] -> [(Type, Type)]
forall a. a -> [a] -> [a]
: [(Type, Type)]
tl
                     (FunKind ContraVar _ _ _,
                       FunKind ContraVar _ _ _) -> (Type
a2, Type
a1) (Type, Type) -> [(Type, Type)] -> [(Type, Type)]
forall a. a -> [a] -> [a]
: [(Type, Type)]
tl
                     _ -> (Type
a1, Type
a2) (Type, Type) -> [(Type, Type)] -> [(Type, Type)]
forall a. a -> [a] -> [a]
: (Type
a2, Type
a1) (Type, Type) -> [(Type, Type)] -> [(Type, Type)]
forall a. a -> [a] -> [a]
: [(Type, Type)]
tl
    _ -> [(Type, Type)] -> [(Type, Type)] -> State Int (Result Subst)
shapeMgu [(Type, Type)]
newKnowns [(Type, Type)]
tl -- ignore non-matching pairs

inclusions :: [(Type, Type)] -> [(Type, Type)]
inclusions :: [(Type, Type)] -> [(Type, Type)]
inclusions cs :: [(Type, Type)]
cs = let (atoms :: [(Type, Type)]
atoms, sts :: [(Type, Type)]
sts) = ((Type, Type) -> Bool)
-> [(Type, Type)] -> ([(Type, Type)], [(Type, Type)])
forall a. (a -> Bool) -> [a] -> ([a], [a])
partition (Type, Type) -> Bool
isAtomic [(Type, Type)]
cs in
    case [(Type, Type)]
sts of
      [] -> [(Type, Type)]
atoms
      p :: (Type, Type)
p@(t1 :: Type
t1, t2 :: Type
t2) : tl :: [(Type, Type)]
tl -> [(Type, Type)]
atoms [(Type, Type)] -> [(Type, Type)] -> [(Type, Type)]
forall a. [a] -> [a] -> [a]
++ case (Type, Type)
p of
        (ExpandedType _ t :: Type
t, _) | Type -> Bool
noAbs Type
t -> [(Type, Type)] -> [(Type, Type)]
inclusions ([(Type, Type)] -> [(Type, Type)])
-> [(Type, Type)] -> [(Type, Type)]
forall a b. (a -> b) -> a -> b
$ (Type
t, Type
t2) (Type, Type) -> [(Type, Type)] -> [(Type, Type)]
forall a. a -> [a] -> [a]
: [(Type, Type)]
tl
        (_, ExpandedType _ t :: Type
t) | Type -> Bool
noAbs Type
t -> [(Type, Type)] -> [(Type, Type)]
inclusions ([(Type, Type)] -> [(Type, Type)])
-> [(Type, Type)] -> [(Type, Type)]
forall a b. (a -> b) -> a -> b
$ (Type
t1, Type
t) (Type, Type) -> [(Type, Type)] -> [(Type, Type)]
forall a. a -> [a] -> [a]
: [(Type, Type)]
tl
        (KindedType t :: Type
t _ _, _) -> [(Type, Type)] -> [(Type, Type)]
inclusions ([(Type, Type)] -> [(Type, Type)])
-> [(Type, Type)] -> [(Type, Type)]
forall a b. (a -> b) -> a -> b
$ (Type
t, Type
t2) (Type, Type) -> [(Type, Type)] -> [(Type, Type)]
forall a. a -> [a] -> [a]
: [(Type, Type)]
tl
        (_, KindedType t :: Type
t _ _) -> [(Type, Type)] -> [(Type, Type)]
inclusions ([(Type, Type)] -> [(Type, Type)])
-> [(Type, Type)] -> [(Type, Type)]
forall a b. (a -> b) -> a -> b
$ (Type
t1, Type
t) (Type, Type) -> [(Type, Type)] -> [(Type, Type)]
forall a. a -> [a] -> [a]
: [(Type, Type)]
tl
        (TypeAppl (TypeName l1 :: Id
l1 _ _) a1 :: Type
a1, TypeAppl (TypeName l2 :: Id
l2 _ _) a2 :: Type
a2)
          | Id
l1 Id -> Id -> Bool
forall a. Eq a => a -> a -> Bool
== Id
lazyTypeId Bool -> Bool -> Bool
&& Id
l2 Id -> Id -> Bool
forall a. Eq a => a -> a -> Bool
== Id
lazyTypeId ->
            [(Type, Type)] -> [(Type, Type)]
inclusions ([(Type, Type)] -> [(Type, Type)])
-> [(Type, Type)] -> [(Type, Type)]
forall a b. (a -> b) -> a -> b
$ (Type
a1, Type
a2) (Type, Type) -> [(Type, Type)] -> [(Type, Type)]
forall a. a -> [a] -> [a]
: [(Type, Type)]
tl
        (TypeAppl (TypeName l :: Id
l _ _) t :: Type
t, TypeName {}) | Id
l Id -> Id -> Bool
forall a. Eq a => a -> a -> Bool
== Id
lazyTypeId ->
            [(Type, Type)] -> [(Type, Type)]
inclusions ([(Type, Type)] -> [(Type, Type)])
-> [(Type, Type)] -> [(Type, Type)]
forall a b. (a -> b) -> a -> b
$ (Type
t, Type
t2) (Type, Type) -> [(Type, Type)] -> [(Type, Type)]
forall a. a -> [a] -> [a]
: [(Type, Type)]
tl
        (TypeName {}, TypeAppl (TypeName l :: Id
l _ _) t :: Type
t) | Id
l Id -> Id -> Bool
forall a. Eq a => a -> a -> Bool
== Id
lazyTypeId ->
            [(Type, Type)] -> [(Type, Type)]
inclusions ([(Type, Type)] -> [(Type, Type)])
-> [(Type, Type)] -> [(Type, Type)]
forall a b. (a -> b) -> a -> b
$ (Type
t1, Type
t) (Type, Type) -> [(Type, Type)] -> [(Type, Type)]
forall a. a -> [a] -> [a]
: [(Type, Type)]
tl
        _ -> case Type -> Maybe Type
redStep Type
t1 of
             Nothing -> case Type -> Maybe Type
redStep Type
t2 of
               Nothing -> case (Type, Type)
p of
                 (TypeAppl f1 :: Type
f1 a1 :: Type
a1, TypeAppl f2 :: Type
f2 a2 :: Type
a2) -> case (Type
f1, Type
f2) of
                   (_, TypeName l :: Id
l _ _)
                     | Id
l Id -> Id -> Bool
forall a. Eq a => a -> a -> Bool
== Id
lazyTypeId ->
                       [(Type, Type)] -> [(Type, Type)]
inclusions ([(Type, Type)] -> [(Type, Type)])
-> [(Type, Type)] -> [(Type, Type)]
forall a b. (a -> b) -> a -> b
$ (Type
t1, Type
a2) (Type, Type) -> [(Type, Type)] -> [(Type, Type)]
forall a. a -> [a] -> [a]
: [(Type, Type)]
tl
                   (TypeName l :: Id
l _ _, _)
                     | Id
l Id -> Id -> Bool
forall a. Eq a => a -> a -> Bool
== Id
lazyTypeId ->
                       [(Type, Type)] -> [(Type, Type)]
inclusions ([(Type, Type)] -> [(Type, Type)])
-> [(Type, Type)] -> [(Type, Type)]
forall a b. (a -> b) -> a -> b
$ (Type
a1, Type
t2) (Type, Type) -> [(Type, Type)] -> [(Type, Type)]
forall a. a -> [a] -> [a]
: [(Type, Type)]
tl
                   _ -> [(Type, Type)] -> [(Type, Type)]
inclusions ([(Type, Type)] -> [(Type, Type)])
-> [(Type, Type)] -> [(Type, Type)]
forall a b. (a -> b) -> a -> b
$
                    (Type
f1, Type
f2) (Type, Type) -> [(Type, Type)] -> [(Type, Type)]
forall a. a -> [a] -> [a]
: case (Type -> RawKind
rawKindOfType Type
f1, Type -> RawKind
rawKindOfType Type
f2) of
                     (FunKind CoVar _ _ _,
                       FunKind CoVar _ _ _) -> (Type
a1, Type
a2) (Type, Type) -> [(Type, Type)] -> [(Type, Type)]
forall a. a -> [a] -> [a]
: [(Type, Type)]
tl
                     (FunKind ContraVar _ _ _,
                       FunKind ContraVar _ _ _) -> (Type
a2, Type
a1) (Type, Type) -> [(Type, Type)] -> [(Type, Type)]
forall a. a -> [a] -> [a]
: [(Type, Type)]
tl
                     _ -> (Type
a1, Type
a2) (Type, Type) -> [(Type, Type)] -> [(Type, Type)]
forall a. a -> [a] -> [a]
: (Type
a2, Type
a1) (Type, Type) -> [(Type, Type)] -> [(Type, Type)]
forall a. a -> [a] -> [a]
: [(Type, Type)]
tl
                 _ -> (Type, Type)
p (Type, Type) -> [(Type, Type)] -> [(Type, Type)]
forall a. a -> [a] -> [a]
: [(Type, Type)] -> [(Type, Type)]
inclusions [(Type, Type)]
tl
               Just r2 :: Type
r2 -> [(Type, Type)] -> [(Type, Type)]
inclusions ([(Type, Type)] -> [(Type, Type)])
-> [(Type, Type)] -> [(Type, Type)]
forall a b. (a -> b) -> a -> b
$ (Type
t1, Type
r2) (Type, Type) -> [(Type, Type)] -> [(Type, Type)]
forall a. a -> [a] -> [a]
: [(Type, Type)]
tl
             Just r1 :: Type
r1 -> [(Type, Type)] -> [(Type, Type)]
inclusions ([(Type, Type)] -> [(Type, Type)])
-> [(Type, Type)] -> [(Type, Type)]
forall a b. (a -> b) -> a -> b
$ (Type
r1, Type
t2) (Type, Type) -> [(Type, Type)] -> [(Type, Type)]
forall a. a -> [a] -> [a]
: [(Type, Type)]
tl

shapeUnify :: [(Type, Type)] -> State Int (Result (Subst, [(Type, Type)]))
shapeUnify :: [(Type, Type)] -> State Int (Result (Subst, [(Type, Type)]))
shapeUnify l :: [(Type, Type)]
l = do
    Result ds :: [Diagnosis]
ds ms :: Maybe Subst
ms <- [(Type, Type)] -> [(Type, Type)] -> State Int (Result Subst)
shapeMgu [] [(Type, Type)]
l
    case Maybe Subst
ms of
      Just s :: Subst
s -> Result (Subst, [(Type, Type)])
-> State Int (Result (Subst, [(Type, Type)]))
forall (m :: * -> *) a. Monad m => a -> m a
return (Result (Subst, [(Type, Type)])
 -> State Int (Result (Subst, [(Type, Type)])))
-> Result (Subst, [(Type, Type)])
-> State Int (Result (Subst, [(Type, Type)]))
forall a b. (a -> b) -> a -> b
$ [Diagnosis]
-> Maybe (Subst, [(Type, Type)]) -> Result (Subst, [(Type, Type)])
forall a. [Diagnosis] -> Maybe a -> Result a
Result [Diagnosis]
ds (Maybe (Subst, [(Type, Type)]) -> Result (Subst, [(Type, Type)]))
-> Maybe (Subst, [(Type, Type)]) -> Result (Subst, [(Type, Type)])
forall a b. (a -> b) -> a -> b
$ (Subst, [(Type, Type)]) -> Maybe (Subst, [(Type, Type)])
forall a. a -> Maybe a
Just (Subst
s, [(Type, Type)] -> [(Type, Type)]
inclusions ([(Type, Type)] -> [(Type, Type)])
-> [(Type, Type)] -> [(Type, Type)]
forall a b. (a -> b) -> a -> b
$ Subst -> [(Type, Type)] -> [(Type, Type)]
substPairList Subst
s [(Type, Type)]
l)
      Nothing -> Result (Subst, [(Type, Type)])
-> State Int (Result (Subst, [(Type, Type)]))
forall (m :: * -> *) a. Monad m => a -> m a
return (Result (Subst, [(Type, Type)])
 -> State Int (Result (Subst, [(Type, Type)])))
-> Result (Subst, [(Type, Type)])
-> State Int (Result (Subst, [(Type, Type)]))
forall a b. (a -> b) -> a -> b
$ [Diagnosis]
-> Maybe (Subst, [(Type, Type)]) -> Result (Subst, [(Type, Type)])
forall a. [Diagnosis] -> Maybe a -> Result a
Result [Diagnosis]
ds Maybe (Subst, [(Type, Type)])
forall a. Maybe a
Nothing

-- input an atomized constraint list
collapser :: Rel.Rel Type -> Result Subst
collapser :: Rel Type -> Result Subst
collapser r :: Rel Type
r =
    let t :: [Set Type]
t = Rel Type -> [Set Type]
forall a. Ord a => Rel a -> [Set a]
Rel.sccOfClosure Rel Type
r
        ks :: [(Set Type, Set Type)]
ks = (Set Type -> (Set Type, Set Type))
-> [Set Type] -> [(Set Type, Set Type)]
forall a b. (a -> b) -> [a] -> [b]
map ((Type -> Bool) -> Set Type -> (Set Type, Set Type)
forall a. (a -> Bool) -> Set a -> (Set a, Set a)
Set.partition ( \ e :: Type
e -> case Type
e of
               TypeName _ _ n :: Int
n -> Int
n Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== 0
               _ -> String -> Bool
forall a. (?callStack::CallStack) => String -> a
error "collapser")) [Set Type]
t
        ws :: [(Set Type, Set Type)]
ws = ((Set Type, Set Type) -> Bool)
-> [(Set Type, Set Type)] -> [(Set Type, Set Type)]
forall a. (a -> Bool) -> [a] -> [a]
filter (Set Type -> Bool
forall a. Set a -> Bool
hasMany (Set Type -> Bool)
-> ((Set Type, Set Type) -> Set Type)
-> (Set Type, Set Type)
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Set Type, Set Type) -> Set Type
forall a b. (a, b) -> a
fst) [(Set Type, Set Type)]
ks
    in if [(Set Type, Set Type)] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [(Set Type, Set Type)]
ws then
       Subst -> Result Subst
forall (m :: * -> *) a. Monad m => a -> m a
return (Subst -> Result Subst) -> Subst -> Result Subst
forall a b. (a -> b) -> a -> b
$ ((Set Type, Set Type) -> Subst -> Subst)
-> Subst -> [(Set Type, Set Type)] -> Subst
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr ( \ (cs :: Set Type
cs, vs :: Set Type
vs) s :: Subst
s -> Subst -> (Type, Set Type) -> Subst
extendSubst Subst
s ((Type, Set Type) -> Subst) -> (Type, Set Type) -> Subst
forall a b. (a -> b) -> a -> b
$
               if Set Type -> Bool
forall a. Set a -> Bool
Set.null Set Type
cs then Set Type -> (Type, Set Type)
forall a. Set a -> (a, Set a)
Set.deleteFindMin Set Type
vs
               else (Set Type -> Type
forall a. Set a -> a
Set.findMin Set Type
cs, Set Type
vs)) Subst
eps [(Set Type, Set Type)]
ks
    else [Diagnosis] -> Maybe Subst -> Result Subst
forall a. [Diagnosis] -> Maybe a -> Result a
Result
         (((Set Type, Set Type) -> Diagnosis)
-> [(Set Type, Set Type)] -> [Diagnosis]
forall a b. (a -> b) -> [a] -> [b]
map ( \ (cs :: Set Type
cs, _) ->
                let (c1 :: Type
c1, rs :: Set Type
rs) = Set Type -> (Type, Set Type)
forall a. Set a -> (a, Set a)
Set.deleteFindMin Set Type
cs
                    c2 :: Type
c2 = Set Type -> Type
forall a. Set a -> a
Set.findMin Set Type
rs
                in DiagKind -> String -> Range -> Diagnosis
Diag DiagKind
Hint ("contradicting type inclusions for '"
                         String -> String -> String
forall a. [a] -> [a] -> [a]
++ Type -> String -> String
forall a. Pretty a => a -> String -> String
showDoc Type
c1 "' and '"
                         String -> String -> String
forall a. [a] -> [a] -> [a]
++ Type -> String -> String
forall a. Pretty a => a -> String -> String
showDoc Type
c2 "'") Range
nullRange) [(Set Type, Set Type)]
ws) Maybe Subst
forall a. Maybe a
Nothing

extendSubst :: Subst -> (Type, Set.Set Type) -> Subst
extendSubst :: Subst -> (Type, Set Type) -> Subst
extendSubst s :: Subst
s (t :: Type
t, vs :: Set Type
vs) = (Type -> Subst -> Subst) -> Subst -> Set Type -> Subst
forall a b. (a -> b -> b) -> b -> Set a -> b
Set.fold ( \ ~(TypeName _ _ n :: Int
n) ->
              Int -> Type -> Subst -> Subst
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert Int
n Type
t) Subst
s Set Type
vs

-- | partition into qualification and subtyping constraints
partitionC :: Constraints -> (Constraints, Constraints)
partitionC :: Constraints -> (Constraints, Constraints)
partitionC = (Constrain -> Bool) -> Constraints -> (Constraints, Constraints)
forall a. (a -> Bool) -> Set a -> (Set a, Set a)
Set.partition ( \ c :: Constrain
c -> case Constrain
c of
                             Kinding _ _ -> Bool
True
                             Subtyping _ _ -> Bool
False)

-- | convert subtypings constrains to a pair list
toListC :: Constraints -> [(Type, Type)]
toListC :: Constraints -> [(Type, Type)]
toListC l :: Constraints
l = [ (Type
t1, Type
t2) | Subtyping t1 :: Type
t1 t2 :: Type
t2 <- Constraints -> [Constrain]
forall a. Set a -> [a]
Set.toList Constraints
l ]

shapeMatchPairList :: TypeMap -> [(Type, Type)] -> Result Subst
shapeMatchPairList :: TypeMap -> [(Type, Type)] -> Result Subst
shapeMatchPairList tm :: TypeMap
tm l :: [(Type, Type)]
l = case [(Type, Type)]
l of
    [] -> Subst -> Result Subst
forall (m :: * -> *) a. Monad m => a -> m a
return Subst
eps
    (t1 :: Type
t1, t2 :: Type
t2) : rt :: [(Type, Type)]
rt -> do
        Subst
s1 <- TypeMap -> Type -> Type -> Result Subst
shapeMatch TypeMap
tm Type
t1 Type
t2
        Subst
s2 <- TypeMap -> [(Type, Type)] -> Result Subst
shapeMatchPairList TypeMap
tm ([(Type, Type)] -> Result Subst) -> [(Type, Type)] -> Result Subst
forall a b. (a -> b) -> a -> b
$ Subst -> [(Type, Type)] -> [(Type, Type)]
substPairList Subst
s1 [(Type, Type)]
rt
        Subst -> Result Subst
forall (m :: * -> *) a. Monad m => a -> m a
return (Subst -> Result Subst) -> Subst -> Result Subst
forall a b. (a -> b) -> a -> b
$ Subst -> Subst -> Subst
compSubst Subst
s1 Subst
s2

shapeRel :: Env -> [(Type, Type)] -> State Int (Result (Subst, Rel.Rel Type))
shapeRel :: Env -> [(Type, Type)] -> State Int (Result (Subst, Rel Type))
shapeRel te :: Env
te subL :: [(Type, Type)]
subL =
    case TypeMap -> [(Type, Type)] -> Result Subst
shapeMatchPairList (Env -> TypeMap
typeMap Env
te) [(Type, Type)]
subL of
       Result ds :: [Diagnosis]
ds Nothing -> Result (Subst, Rel Type) -> State Int (Result (Subst, Rel Type))
forall (m :: * -> *) a. Monad m => a -> m a
return (Result (Subst, Rel Type) -> State Int (Result (Subst, Rel Type)))
-> Result (Subst, Rel Type) -> State Int (Result (Subst, Rel Type))
forall a b. (a -> b) -> a -> b
$ [Diagnosis] -> Maybe (Subst, Rel Type) -> Result (Subst, Rel Type)
forall a. [Diagnosis] -> Maybe a -> Result a
Result [Diagnosis]
ds Maybe (Subst, Rel Type)
forall a. Maybe a
Nothing
       _ -> do
         Result rs :: [Diagnosis]
rs msa :: Maybe (Subst, [(Type, Type)])
msa <- [(Type, Type)] -> State Int (Result (Subst, [(Type, Type)]))
shapeUnify [(Type, Type)]
subL
         case Maybe (Subst, [(Type, Type)])
msa of
           Just (s1 :: Subst
s1, atoms0 :: [(Type, Type)]
atoms0) ->
               let atoms :: [(Type, Type)]
atoms = ((Type, Type) -> Bool) -> [(Type, Type)] -> [(Type, Type)]
forall a. (a -> Bool) -> [a] -> [a]
filter (Type, Type) -> Bool
isAtomic [(Type, Type)]
atoms0
                   r :: Rel Type
r = Rel Type -> Rel Type
forall a. Ord a => Rel a -> Rel a
Rel.transClosure (Rel Type -> Rel Type) -> Rel Type -> Rel Type
forall a b. (a -> b) -> a -> b
$ [(Type, Type)] -> Rel Type
forall a. Ord a => [(a, a)] -> Rel a
Rel.fromList [(Type, Type)]
atoms
                   es :: [(Type, Type)]
es = (Type -> Set Type -> [(Type, Type)] -> [(Type, Type)])
-> [(Type, Type)] -> Map Type (Set Type) -> [(Type, Type)]
forall k a b. (k -> a -> b -> b) -> b -> Map k a -> b
Map.foldrWithKey ( \ t1 :: Type
t1 st :: Set Type
st l1 :: [(Type, Type)]
l1 ->
                             case Type
t1 of
                             TypeName _ _ 0 -> (Type -> [(Type, Type)] -> [(Type, Type)])
-> [(Type, Type)] -> Set Type -> [(Type, Type)]
forall a b. (a -> b -> b) -> b -> Set a -> b
Set.fold ( \ t2 :: Type
t2 l2 :: [(Type, Type)]
l2 ->
                                 case Type
t2 of
                                 TypeName _ _ 0 -> if Env -> Type -> Type -> Bool
lesserType Env
te Type
t1 Type
t2
                                     then [(Type, Type)]
l2 else (Type
t1, Type
t2) (Type, Type) -> [(Type, Type)] -> [(Type, Type)]
forall a. a -> [a] -> [a]
: [(Type, Type)]
l2
                                 _ -> [(Type, Type)]
l2) [(Type, Type)]
l1 Set Type
st
                             _ -> [(Type, Type)]
l1) [] (Map Type (Set Type) -> [(Type, Type)])
-> Map Type (Set Type) -> [(Type, Type)]
forall a b. (a -> b) -> a -> b
$ Rel Type -> Map Type (Set Type)
forall a. Rel a -> Map a (Set a)
Rel.toMap Rel Type
r
               in Result (Subst, Rel Type) -> State Int (Result (Subst, Rel Type))
forall (m :: * -> *) a. Monad m => a -> m a
return (Result (Subst, Rel Type) -> State Int (Result (Subst, Rel Type)))
-> Result (Subst, Rel Type) -> State Int (Result (Subst, Rel Type))
forall a b. (a -> b) -> a -> b
$ if [(Type, Type)] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [(Type, Type)]
es then
                 case Rel Type -> Result Subst
collapser Rel Type
r of
                   Result ds :: [Diagnosis]
ds Nothing -> [Diagnosis] -> Maybe (Subst, Rel Type) -> Result (Subst, Rel Type)
forall a. [Diagnosis] -> Maybe a -> Result a
Result [Diagnosis]
ds Maybe (Subst, Rel Type)
forall a. Maybe a
Nothing
                   Result _ (Just s2 :: Subst
s2) ->
                       (Subst, Rel Type) -> Result (Subst, Rel Type)
forall (m :: * -> *) a. Monad m => a -> m a
return (Subst -> Subst -> Subst
compSubst Subst
s1 Subst
s2,
                                  [(Type, Type)] -> Rel Type
forall a. Ord a => [(a, a)] -> Rel a
Rel.fromList ([(Type, Type)] -> Rel Type) -> [(Type, Type)] -> Rel Type
forall a b. (a -> b) -> a -> b
$ Subst -> [(Type, Type)] -> [(Type, Type)]
substPairList Subst
s2 [(Type, Type)]
atoms0)
                 else [Diagnosis] -> Maybe (Subst, Rel Type) -> Result (Subst, Rel Type)
forall a. [Diagnosis] -> Maybe a -> Result a
Result (((Type, Type) -> Diagnosis) -> [(Type, Type)] -> [Diagnosis]
forall a b. (a -> b) -> [a] -> [b]
map ( \ (t1 :: Type
t1, t2 :: Type
t2) ->
                                 DiagKind -> String -> Constrain -> Diagnosis
forall a.
(GetRange a, Pretty a) =>
DiagKind -> String -> a -> Diagnosis
mkDiag DiagKind
Hint "rejected" (Constrain -> Diagnosis) -> Constrain -> Diagnosis
forall a b. (a -> b) -> a -> b
$
                                             Type -> Type -> Constrain
Subtyping Type
t1 Type
t2) [(Type, Type)]
es) Maybe (Subst, Rel Type)
forall a. Maybe a
Nothing
           Nothing -> Result (Subst, Rel Type) -> State Int (Result (Subst, Rel Type))
forall (m :: * -> *) a. Monad m => a -> m a
return (Result (Subst, Rel Type) -> State Int (Result (Subst, Rel Type)))
-> Result (Subst, Rel Type) -> State Int (Result (Subst, Rel Type))
forall a b. (a -> b) -> a -> b
$ [Diagnosis] -> Maybe (Subst, Rel Type) -> Result (Subst, Rel Type)
forall a. [Diagnosis] -> Maybe a -> Result a
Result [Diagnosis]
rs Maybe (Subst, Rel Type)
forall a. Maybe a
Nothing

-- | compute monotonicity of a type variable
monotonic :: Int -> Type -> (Bool, Bool)
monotonic :: Int -> Type -> (Bool, Bool)
monotonic v :: Int
v = FoldTypeRec (Bool, Bool) -> Type -> (Bool, Bool)
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 -> (Bool, Bool)
foldTypeName = \ _ _ _ i :: Int
i -> (Bool
True, Int
i Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
/= Int
v)
  , foldTypeAppl :: Type -> (Bool, Bool) -> (Bool, Bool) -> (Bool, Bool)
foldTypeAppl = \ ~t :: Type
t@(TypeAppl tf :: Type
tf _) ~(f1 :: Bool
f1, f2 :: Bool
f2) (a1 :: Bool
a1, a2 :: Bool
a2) ->
      -- avoid evaluation of (f1, f2) if it is not needed by "~"
     case Type -> Maybe Type
redStep Type
t of
      Just r :: Type
r -> Int -> Type -> (Bool, Bool)
monotonic Int
v Type
r
      Nothing -> case Type -> RawKind
rawKindOfType Type
tf of
        FunKind CoVar _ _ _ -> (Bool
f1 Bool -> Bool -> Bool
&& Bool
a1, Bool
f2 Bool -> Bool -> Bool
&& Bool
a2)
        FunKind ContraVar _ _ _ -> (Bool
f1 Bool -> Bool -> Bool
&& Bool
a2, Bool
f2 Bool -> Bool -> Bool
&& Bool
a1)
        _ -> (Bool
f1 Bool -> Bool -> Bool
&& Bool
a1 Bool -> Bool -> Bool
&& Bool
a2, Bool
f2 Bool -> Bool -> Bool
&& Bool
a1 Bool -> Bool -> Bool
&& Bool
a2)
  , foldExpandedType :: Type -> (Bool, Bool) -> (Bool, Bool) -> (Bool, Bool)
foldExpandedType = \ _ _ p :: (Bool, Bool)
p -> (Bool, Bool)
p
  , foldTypeAbs :: Type -> TypeArg -> (Bool, Bool) -> Range -> (Bool, Bool)
foldTypeAbs = \ _ _ _ _ -> (Bool
False, Bool
False)
  , foldKindedType :: Type -> (Bool, Bool) -> Set Kind -> Range -> (Bool, Bool)
foldKindedType = \ _ p :: (Bool, Bool)
p _ _ -> (Bool, Bool)
p
  , foldTypeToken :: Type -> Token -> (Bool, Bool)
foldTypeToken = \ _ _ -> String -> (Bool, Bool)
forall a. (?callStack::CallStack) => String -> a
error "monotonic.foldTypeToken"
  , foldBracketType :: Type -> BracketKind -> [(Bool, Bool)] -> Range -> (Bool, Bool)
foldBracketType = \ _ _ _ _ -> String -> (Bool, Bool)
forall a. (?callStack::CallStack) => String -> a
error "monotonic.foldBracketType"
  , foldMixfixType :: Type -> [(Bool, Bool)] -> (Bool, Bool)
foldMixfixType = \ _ -> String -> [(Bool, Bool)] -> (Bool, Bool)
forall a. (?callStack::CallStack) => String -> a
error "monotonic.foldMixfixType" }

-- | find monotonicity based instantiation
monoSubst :: Rel.Rel Type -> Type -> Subst
monoSubst :: Rel Type -> Type -> Subst
monoSubst r :: Rel Type
r t :: Type
t =
    let varSet :: Type -> Set (Int, (Id, RawKind))
varSet = [(Int, (Id, RawKind))] -> Set (Int, (Id, RawKind))
forall a. Ord a => [a] -> Set a
Set.fromList ([(Int, (Id, RawKind))] -> Set (Int, (Id, RawKind)))
-> (Type -> [(Int, (Id, RawKind))])
-> Type
-> Set (Int, (Id, RawKind))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Type -> [(Int, (Id, RawKind))]
freeTVars
        vs :: [(Int, (Id, RawKind))]
vs = Set (Int, (Id, RawKind)) -> [(Int, (Id, RawKind))]
forall a. Set a -> [a]
Set.toList (Set (Int, (Id, RawKind)) -> [(Int, (Id, RawKind))])
-> Set (Int, (Id, RawKind)) -> [(Int, (Id, RawKind))]
forall a b. (a -> b) -> a -> b
$ Set (Int, (Id, RawKind))
-> Set (Int, (Id, RawKind)) -> Set (Int, (Id, RawKind))
forall a. Ord a => Set a -> Set a -> Set a
Set.union (Type -> Set (Int, (Id, RawKind))
varSet Type
t) (Set (Int, (Id, RawKind)) -> Set (Int, (Id, RawKind)))
-> Set (Int, (Id, RawKind)) -> Set (Int, (Id, RawKind))
forall a b. (a -> b) -> a -> b
$ [Set (Int, (Id, RawKind))] -> Set (Int, (Id, RawKind))
forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
Set.unions ([Set (Int, (Id, RawKind))] -> Set (Int, (Id, RawKind)))
-> [Set (Int, (Id, RawKind))] -> Set (Int, (Id, RawKind))
forall a b. (a -> b) -> a -> b
$ (Type -> Set (Int, (Id, RawKind)))
-> [Type] -> [Set (Int, (Id, RawKind))]
forall a b. (a -> b) -> [a] -> [b]
map Type -> Set (Int, (Id, RawKind))
varSet
              ([Type] -> [Set (Int, (Id, RawKind))])
-> [Type] -> [Set (Int, (Id, RawKind))]
forall a b. (a -> b) -> a -> b
$ Set Type -> [Type]
forall a. Set a -> [a]
Set.toList (Set Type -> [Type]) -> Set Type -> [Type]
forall a b. (a -> b) -> a -> b
$ Rel Type -> Set Type
forall a. Ord a => Rel a -> Set a
Rel.nodes Rel Type
r
        monos :: [(Int, (Id, RawKind))]
monos = ((Int, (Id, RawKind)) -> Bool)
-> [(Int, (Id, RawKind))] -> [(Int, (Id, RawKind))]
forall a. (a -> Bool) -> [a] -> [a]
filter ( \ (i :: Int
i, (n :: Id
n, rk :: RawKind
rk)) -> case Int -> Type -> (Bool, Bool)
monotonic Int
i Type
t of
                                (True, _) -> Set Type -> Bool
forall a. Set a -> Bool
isSingleton
                                    (Rel Type -> Type -> Set Type
forall a. Ord a => Rel a -> a -> Set a
Rel.predecessors Rel Type
r (Type -> Set Type) -> Type -> Set Type
forall a b. (a -> b) -> a -> b
$
                                        Id -> RawKind -> Int -> Type
TypeName Id
n RawKind
rk Int
i)
                                _ -> Bool
False) [(Int, (Id, RawKind))]
vs
        antis :: [(Int, (Id, RawKind))]
antis = ((Int, (Id, RawKind)) -> Bool)
-> [(Int, (Id, RawKind))] -> [(Int, (Id, RawKind))]
forall a. (a -> Bool) -> [a] -> [a]
filter ( \ (i :: Int
i, (n :: Id
n, rk :: RawKind
rk)) -> case Int -> Type -> (Bool, Bool)
monotonic Int
i Type
t of
                                (_, True) -> Set Type -> Bool
forall a. Set a -> Bool
isSingleton
                                     (Rel Type -> Type -> Set Type
forall a. Ord a => Rel a -> a -> Set a
Rel.succs Rel Type
r (Type -> Set Type) -> Type -> Set Type
forall a b. (a -> b) -> a -> b
$
                                         Id -> RawKind -> Int -> Type
TypeName Id
n RawKind
rk Int
i)
                                _ -> Bool
False) [(Int, (Id, RawKind))]
vs
        resta :: [(Int, (Id, RawKind))]
resta = ((Int, (Id, RawKind)) -> Bool)
-> [(Int, (Id, RawKind))] -> [(Int, (Id, RawKind))]
forall a. (a -> Bool) -> [a] -> [a]
filter ( \ (i :: Int
i, (n :: Id
n, rk :: RawKind
rk)) -> case Int -> Type -> (Bool, Bool)
monotonic Int
i Type
t of
                                (True, True) -> Set Type -> Bool
forall a. Set a -> Bool
hasMany (Set Type -> Bool) -> Set Type -> Bool
forall a b. (a -> b) -> a -> b
$
                                     Rel Type -> Type -> Set Type
forall a. Ord a => Rel a -> a -> Set a
Rel.succs Rel Type
r (Type -> Set Type) -> Type -> Set Type
forall a b. (a -> b) -> a -> b
$ Id -> RawKind -> Int -> Type
TypeName Id
n RawKind
rk Int
i
                                _ -> Bool
False) [(Int, (Id, RawKind))]
vs
        restb :: [(Int, (Id, RawKind))]
restb = ((Int, (Id, RawKind)) -> Bool)
-> [(Int, (Id, RawKind))] -> [(Int, (Id, RawKind))]
forall a. (a -> Bool) -> [a] -> [a]
filter ( \ (i :: Int
i, (n :: Id
n, rk :: RawKind
rk)) -> case Int -> Type -> (Bool, Bool)
monotonic Int
i Type
t of
                                (True, True) -> Set Type -> Bool
forall a. Set a -> Bool
hasMany (Set Type -> Bool) -> Set Type -> Bool
forall a b. (a -> b) -> a -> b
$
                                     Rel Type -> Type -> Set Type
forall a. Ord a => Rel a -> a -> Set a
Rel.predecessors Rel Type
r (Type -> Set Type) -> Type -> Set Type
forall a b. (a -> b) -> a -> b
$ Id -> RawKind -> Int -> Type
TypeName Id
n RawKind
rk Int
i
                                _ -> Bool
False) [(Int, (Id, RawKind))]
vs
    in if [(Int, (Id, RawKind))] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [(Int, (Id, RawKind))]
antis then
          if [(Int, (Id, RawKind))] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [(Int, (Id, RawKind))]
monos then
             if [(Int, (Id, RawKind))] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [(Int, (Id, RawKind))]
resta then
                if [(Int, (Id, RawKind))] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [(Int, (Id, RawKind))]
restb then Subst
eps else
                    let (i :: Int
i, (n :: Id
n, rk :: RawKind
rk)) = [(Int, (Id, RawKind))] -> (Int, (Id, RawKind))
forall a. [a] -> a
head [(Int, (Id, RawKind))]
restb
                        tn :: Type
tn = Id -> RawKind -> Int -> Type
TypeName Id
n RawKind
rk Int
i
                        s :: Set Type
s = Rel Type -> Type -> Set Type
forall a. Ord a => Rel a -> a -> Set a
Rel.predecessors Rel Type
r Type
tn
                        sl :: Set Type
sl = Type -> Set Type -> Set Type
forall a. Ord a => a -> Set a -> Set a
Set.delete Type
tn (Set Type -> Set Type) -> Set Type -> Set Type
forall a b. (a -> b) -> a -> b
$ (Set Type -> Set Type -> Set Type) -> [Set Type] -> Set Type
forall (t :: * -> *) a. Foldable t => (a -> a -> a) -> t a -> a
foldl1 Set Type -> Set Type -> Set Type
forall a. Ord a => Set a -> Set a -> Set a
Set.intersection
                                      ([Set Type] -> Set Type) -> [Set Type] -> Set Type
forall a b. (a -> b) -> a -> b
$ (Type -> Set Type) -> [Type] -> [Set Type]
forall a b. (a -> b) -> [a] -> [b]
map (Rel Type -> Type -> Set Type
forall a. Ord a => Rel a -> a -> Set a
Rel.succs Rel Type
r)
                                      ([Type] -> [Set Type]) -> [Type] -> [Set Type]
forall a b. (a -> b) -> a -> b
$ Set Type -> [Type]
forall a. Set a -> [a]
Set.toList Set Type
s
                    in Int -> Type -> Subst
forall k a. k -> a -> Map k a
Map.singleton Int
i (Type -> Subst) -> Type -> Subst
forall a b. (a -> b) -> a -> b
$ Set Type -> Type
forall a. Set a -> a
Set.findMin
                       (Set Type -> Type) -> Set Type -> Type
forall a b. (a -> b) -> a -> b
$ if Set Type -> Bool
forall a. Set a -> Bool
Set.null Set Type
sl then Set Type
s else Set Type
sl
             else let
                 (i :: Int
i, (n :: Id
n, rk :: RawKind
rk)) = [(Int, (Id, RawKind))] -> (Int, (Id, RawKind))
forall a. [a] -> a
head [(Int, (Id, RawKind))]
resta
                 tn :: Type
tn = Id -> RawKind -> Int -> Type
TypeName Id
n RawKind
rk Int
i
                 s :: Set Type
s = Rel Type -> Type -> Set Type
forall a. Ord a => Rel a -> a -> Set a
Rel.succs Rel Type
r Type
tn
                 sl :: Set Type
sl = Type -> Set Type -> Set Type
forall a. Ord a => a -> Set a -> Set a
Set.delete Type
tn (Set Type -> Set Type) -> Set Type -> Set Type
forall a b. (a -> b) -> a -> b
$ (Set Type -> Set Type -> Set Type) -> [Set Type] -> Set Type
forall (t :: * -> *) a. Foldable t => (a -> a -> a) -> t a -> a
foldl1 Set Type -> Set Type -> Set Type
forall a. Ord a => Set a -> Set a -> Set a
Set.intersection
                      ([Set Type] -> Set Type) -> [Set Type] -> Set Type
forall a b. (a -> b) -> a -> b
$ (Type -> Set Type) -> [Type] -> [Set Type]
forall a b. (a -> b) -> [a] -> [b]
map (Rel Type -> Type -> Set Type
forall a. Ord a => Rel a -> a -> Set a
Rel.predecessors Rel Type
r)
                      ([Type] -> [Set Type]) -> [Type] -> [Set Type]
forall a b. (a -> b) -> a -> b
$ Set Type -> [Type]
forall a. Set a -> [a]
Set.toList Set Type
s
                 in Int -> Type -> Subst
forall k a. k -> a -> Map k a
Map.singleton Int
i (Type -> Subst) -> Type -> Subst
forall a b. (a -> b) -> a -> b
$ Set Type -> Type
forall a. Set a -> a
Set.findMin
                    (Set Type -> Type) -> Set Type -> Type
forall a b. (a -> b) -> a -> b
$ if Set Type -> Bool
forall a. Set a -> Bool
Set.null Set Type
sl then Set Type
s else Set Type
sl
          else [(Int, Type)] -> Subst
forall k a. [(k, a)] -> Map k a
Map.fromDistinctAscList ([(Int, Type)] -> Subst) -> [(Int, Type)] -> Subst
forall a b. (a -> b) -> a -> b
$ ((Int, (Id, RawKind)) -> (Int, Type))
-> [(Int, (Id, RawKind))] -> [(Int, Type)]
forall a b. (a -> b) -> [a] -> [b]
map ( \ (i :: Int
i, (n :: Id
n, rk :: RawKind
rk)) ->
                (Int
i, Set Type -> Type
forall a. Set a -> a
Set.findMin (Set Type -> Type) -> Set Type -> Type
forall a b. (a -> b) -> a -> b
$ Rel Type -> Type -> Set Type
forall a. Ord a => Rel a -> a -> Set a
Rel.predecessors Rel Type
r (Type -> Set Type) -> Type -> Set Type
forall a b. (a -> b) -> a -> b
$
                  Id -> RawKind -> Int -> Type
TypeName Id
n RawKind
rk Int
i)) [(Int, (Id, RawKind))]
monos
       else [(Int, Type)] -> Subst
forall k a. [(k, a)] -> Map k a
Map.fromDistinctAscList ([(Int, Type)] -> Subst) -> [(Int, Type)] -> Subst
forall a b. (a -> b) -> a -> b
$ ((Int, (Id, RawKind)) -> (Int, Type))
-> [(Int, (Id, RawKind))] -> [(Int, Type)]
forall a b. (a -> b) -> [a] -> [b]
map ( \ (i :: Int
i, (n :: Id
n, rk :: RawKind
rk)) ->
                (Int
i, Set Type -> Type
forall a. Set a -> a
Set.findMin (Set Type -> Type) -> Set Type -> Type
forall a b. (a -> b) -> a -> b
$ Rel Type -> Type -> Set Type
forall a. Ord a => Rel a -> a -> Set a
Rel.succs Rel Type
r (Type -> Set Type) -> Type -> Set Type
forall a b. (a -> b) -> a -> b
$
                  Id -> RawKind -> Int -> Type
TypeName Id
n RawKind
rk Int
i)) [(Int, (Id, RawKind))]
antis

monoSubsts :: Rel.Rel Type -> Type -> Subst
monoSubsts :: Rel Type -> Type -> Subst
monoSubsts r :: Rel Type
r t :: Type
t =
    let s :: Subst
s = Rel Type -> Type -> Subst
monoSubst (Rel Type -> Rel Type
forall a. Ord a => Rel a -> Rel a
Rel.transReduce (Rel Type -> Rel Type) -> Rel Type -> Rel Type
forall a b. (a -> b) -> a -> b
$ Rel Type -> Rel Type
forall a. Ord a => Rel a -> Rel a
Rel.irreflex Rel Type
r) Type
t in
    if Subst -> Bool
forall k a. Map k a -> Bool
Map.null Subst
s then Subst
s else Subst -> Subst -> Subst
compSubst Subst
s
      (Subst -> Subst) -> Subst -> Subst
forall a b. (a -> b) -> a -> b
$ Rel Type -> Type -> Subst
monoSubsts (Rel Type -> Rel Type
forall a. Ord a => Rel a -> Rel a
Rel.transClosure (Rel Type -> Rel Type) -> Rel Type -> Rel Type
forall a b. (a -> b) -> a -> b
$ (Type -> Type) -> Rel Type -> Rel Type
forall a b. (Ord a, Ord b) => (a -> b) -> Rel a -> Rel b
Rel.map (Subst -> Type -> Type
subst Subst
s) Rel Type
r) (Type -> Subst) -> Type -> Subst
forall a b. (a -> b) -> a -> b
$ Subst -> Type -> Type
subst Subst
s Type
t

shapeRelAndMono :: Env -> [(Type, Type)] -> Maybe Type
                -> State Int (Result (Subst, Rel.Rel Type))
shapeRelAndMono :: Env
-> [(Type, Type)]
-> Maybe Type
-> State Int (Result (Subst, Rel Type))
shapeRelAndMono te :: Env
te subL :: [(Type, Type)]
subL mTy :: Maybe Type
mTy = do
    res :: Result (Subst, Rel Type)
res@(Result ds :: [Diagnosis]
ds mc :: Maybe (Subst, Rel Type)
mc) <- Env -> [(Type, Type)] -> State Int (Result (Subst, Rel Type))
shapeRel Env
te
      ([(Type, Type)] -> State Int (Result (Subst, Rel Type)))
-> [(Type, Type)] -> State Int (Result (Subst, Rel Type))
forall a b. (a -> b) -> a -> b
$ if Maybe Type -> Bool
forall a. Maybe a -> Bool
isJust Maybe Type
mTy then LocalTypeVars -> [(Type, Type)]
fromTypeVars (Env -> LocalTypeVars
localTypeVars Env
te) [(Type, Type)] -> [(Type, Type)] -> [(Type, Type)]
forall a. [a] -> [a] -> [a]
++ [(Type, Type)]
subL else [(Type, Type)]
subL
    Result (Subst, Rel Type) -> State Int (Result (Subst, Rel Type))
forall (m :: * -> *) a. Monad m => a -> m a
return (Result (Subst, Rel Type) -> State Int (Result (Subst, Rel Type)))
-> Result (Subst, Rel Type) -> State Int (Result (Subst, Rel Type))
forall a b. (a -> b) -> a -> b
$ case Maybe (Subst, Rel Type)
mc of
        Nothing -> [Diagnosis] -> Maybe (Subst, Rel Type) -> Result (Subst, Rel Type)
forall a. [Diagnosis] -> Maybe a -> Result a
Result [Diagnosis]
ds Maybe (Subst, Rel Type)
forall a. Maybe a
Nothing
        Just (s :: Subst
s, trel :: Rel Type
trel) -> case Maybe Type
mTy of
          Nothing -> Result (Subst, Rel Type)
res
          Just ty :: Type
ty -> let
            ms :: Subst
ms = Rel Type -> Type -> Subst
monoSubsts
                       (Rel Type -> Rel Type
forall a. Ord a => Rel a -> Rel a
Rel.transClosure (Rel Type -> Rel Type) -> Rel Type -> Rel Type
forall a b. (a -> b) -> a -> b
$ Rel Type -> Rel Type -> Rel Type
forall a. Ord a => Rel a -> Rel a -> Rel a
Rel.union (TypeMap -> Rel Type
fromTypeMap (TypeMap -> Rel Type) -> TypeMap -> Rel Type
forall a b. (a -> b) -> a -> b
$ Env -> TypeMap
typeMap Env
te)
                          Rel Type
trel) (Subst -> Type -> Type
subst Subst
s Type
ty)
            in [Diagnosis] -> Maybe (Subst, Rel Type) -> Result (Subst, Rel Type)
forall a. [Diagnosis] -> Maybe a -> Result a
Result [Diagnosis]
ds
                 (Maybe (Subst, Rel Type) -> Result (Subst, Rel Type))
-> Maybe (Subst, Rel Type) -> Result (Subst, Rel Type)
forall a b. (a -> b) -> a -> b
$ (Subst, Rel Type) -> Maybe (Subst, Rel Type)
forall a. a -> Maybe a
Just (Subst -> Subst -> Subst
compSubst Subst
s Subst
ms, (Type -> Type) -> Rel Type -> Rel Type
forall a b. (Ord a, Ord b) => (a -> b) -> Rel a -> Rel b
Rel.map (Subst -> Type -> Type
subst Subst
ms) Rel Type
trel)

shapeRelAndSimplify :: Bool -> Env -> Constraints -> Maybe Type
                    -> State Int (Result (Subst, Constraints))
shapeRelAndSimplify :: Bool
-> Env
-> Constraints
-> Maybe Type
-> State Int (Result (Subst, Constraints))
shapeRelAndSimplify doFail :: Bool
doFail te :: Env
te cs :: Constraints
cs mTy :: Maybe Type
mTy = do
  let (qs :: Constraints
qs, subS :: Constraints
subS) = Constraints -> (Constraints, Constraints)
partitionC Constraints
cs
      subL :: [(Type, Type)]
subL = Constraints -> [(Type, Type)]
toListC Constraints
subS
  Result ds :: [Diagnosis]
ds mc :: Maybe (Subst, Rel Type)
mc <- Env
-> [(Type, Type)]
-> Maybe Type
-> State Int (Result (Subst, Rel Type))
shapeRelAndMono Env
te [(Type, Type)]
subL Maybe Type
mTy
  Result (Subst, Constraints)
-> State Int (Result (Subst, Constraints))
forall (m :: * -> *) a. Monad m => a -> m a
return (Result (Subst, Constraints)
 -> State Int (Result (Subst, Constraints)))
-> Result (Subst, Constraints)
-> State Int (Result (Subst, Constraints))
forall a b. (a -> b) -> a -> b
$ case Maybe (Subst, Rel Type)
mc of
     Nothing -> [Diagnosis]
-> Maybe (Subst, Constraints) -> Result (Subst, Constraints)
forall a. [Diagnosis] -> Maybe a -> Result a
Result [Diagnosis]
ds Maybe (Subst, Constraints)
forall a. Maybe a
Nothing
     Just (s :: Subst
s, trel :: Rel Type
trel) ->
         let (noVarCs :: Constraints
noVarCs, varCs :: Constraints
varCs) = Constraints -> (Constraints, Constraints)
partitionVarC
               (Constraints -> (Constraints, Constraints))
-> Constraints -> (Constraints, Constraints)
forall a b. (a -> b) -> a -> b
$ ((Type, Type) -> Constraints -> Constraints)
-> Constraints -> [(Type, Type)] -> Constraints
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (Constrain -> Constraints -> Constraints
insertC (Constrain -> Constraints -> Constraints)
-> ((Type, Type) -> Constrain)
-> (Type, Type)
-> Constraints
-> Constraints
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Type -> Type -> Constrain) -> (Type, Type) -> Constrain
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry Type -> Type -> Constrain
Subtyping)
                        (Subst -> Constraints -> Constraints
substC Subst
s Constraints
qs) ([(Type, Type)] -> Constraints) -> [(Type, Type)] -> Constraints
forall a b. (a -> b) -> a -> b
$ Rel Type -> [(Type, Type)]
forall a. Rel a -> [(a, a)]
Rel.toList Rel Type
trel
             (es :: [Diagnosis]
es, newCs :: Constraints
newCs) = Env -> Constraints -> ([Diagnosis], Constraints)
simplify Env
te Constraints
noVarCs
             fs :: [Diagnosis]
fs = (Diagnosis -> Diagnosis) -> [Diagnosis] -> [Diagnosis]
forall a b. (a -> b) -> [a] -> [b]
map ( \ d :: Diagnosis
d -> Diagnosis
d {diagKind :: DiagKind
diagKind = DiagKind
Hint}) [Diagnosis]
es
         in [Diagnosis]
-> Maybe (Subst, Constraints) -> Result (Subst, Constraints)
forall a. [Diagnosis] -> Maybe a -> Result a
Result ([Diagnosis]
ds [Diagnosis] -> [Diagnosis] -> [Diagnosis]
forall a. [a] -> [a] -> [a]
++ [Diagnosis]
fs)
                (Maybe (Subst, Constraints) -> Result (Subst, Constraints))
-> Maybe (Subst, Constraints) -> Result (Subst, Constraints)
forall a b. (a -> b) -> a -> b
$ if [Diagnosis] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Diagnosis]
fs Bool -> Bool -> Bool
|| Bool -> Bool
not Bool
doFail then
                      (Subst, Constraints) -> Maybe (Subst, Constraints)
forall a. a -> Maybe a
Just (Subst
s, Constraints -> Constraints -> Constraints
joinC Constraints
varCs Constraints
newCs) else Maybe (Subst, Constraints)
forall a. Maybe a
Nothing

-- | Downsets of type variables made monomorphic need to be considered
fromTypeVars :: LocalTypeVars -> [(Type, Type)]
fromTypeVars :: LocalTypeVars -> [(Type, Type)]
fromTypeVars = (Id -> TypeVarDefn -> [(Type, Type)] -> [(Type, Type)])
-> [(Type, Type)] -> LocalTypeVars -> [(Type, Type)]
forall k a b. (k -> a -> b -> b) -> b -> Map k a -> b
Map.foldrWithKey
    (\ t :: Id
t (TypeVarDefn _ vk :: VarKind
vk rk :: RawKind
rk _) c :: [(Type, Type)]
c -> case VarKind
vk of
              Downset ty :: Type
ty -> (Id -> RawKind -> Int -> Type
TypeName Id
t RawKind
rk 0, Type -> Type
monoType Type
ty) (Type, Type) -> [(Type, Type)] -> [(Type, Type)]
forall a. a -> [a] -> [a]
: [(Type, Type)]
c
              _ -> [(Type, Type)]
c) []

-- | the type relation of declared types
fromTypeMap :: TypeMap -> Rel.Rel Type
fromTypeMap :: TypeMap -> Rel Type
fromTypeMap = (Id -> TypeInfo -> Rel Type -> Rel Type)
-> Rel Type -> TypeMap -> Rel Type
forall k a b. (k -> a -> b -> b) -> b -> Map k a -> b
Map.foldrWithKey (\ t :: Id
t ti :: TypeInfo
ti r :: Rel Type
r -> let k :: RawKind
k = TypeInfo -> RawKind
typeKind TypeInfo
ti in
                    (Id -> Rel Type -> Rel Type) -> Rel Type -> Set Id -> Rel Type
forall a b. (a -> b -> b) -> b -> Set a -> b
Set.fold ( \ j :: Id
j -> Type -> Type -> Rel Type -> Rel Type
forall a. Ord a => a -> a -> Rel a -> Rel a
Rel.insertPair (Id -> RawKind -> Int -> Type
TypeName Id
t RawKind
k 0)
                                (Type -> Rel Type -> Rel Type) -> Type -> Rel Type -> Rel Type
forall a b. (a -> b) -> a -> b
$ Id -> RawKind -> Int -> Type
TypeName Id
j RawKind
k 0) Rel Type
r
                                    (Set Id -> Rel Type) -> Set Id -> Rel Type
forall a b. (a -> b) -> a -> b
$ TypeInfo -> Set Id
superTypes TypeInfo
ti) Rel Type
forall a. Rel a
Rel.empty