module Hydra.Types.Inference (
  annotateElementWithTypes,
  annotateTermWithTypes,
  inferType,
  Constraint,
) where

import Hydra.All
import Hydra.CoreDecoding
import Hydra.CoreEncoding
import qualified Hydra.Impl.Haskell.Dsl.Types as Types
import Hydra.Types.Substitution
import Hydra.Types.Unification

import qualified Control.Monad as CM
import qualified Data.List as L
import qualified Data.Map as M
import qualified Data.Set as S
import qualified Data.Maybe as Y


type InferenceContext m = (Context m, Int, TypingEnvironment m)

type TypingEnvironment m = M.Map Variable (TypeScheme m)

annotateElementWithTypes :: (Ord m, Show m) => Element m -> GraphFlow m (Element m)
annotateElementWithTypes :: forall m. (Ord m, Show m) => Element m -> GraphFlow m (Element m)
annotateElementWithTypes Element m
el = do
    forall s a. String -> Flow s a -> Flow s a
withTrace (String
"annotate element " forall a. [a] -> [a] -> [a]
++ Name -> String
unName (forall m. Element m -> Name
elementName Element m
el)) forall a b. (a -> b) -> a -> b
$ do
      Term m
term <- forall m. (Ord m, Show m) => Term m -> GraphFlow m (Term m)
annotateTermWithTypes forall a b. (a -> b) -> a -> b
$ forall m. Element m -> Term m
elementData Element m
el
      Type m
typ <- forall {m}. Term m -> Flow (Context m) (Type m)
findType Term m
term
      forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Element m
el {
        elementData :: Term m
elementData = Term m
term,
        elementSchema :: Term m
elementSchema = forall m. Type m -> Term m
encodeType Type m
typ}
  where
    findType :: Term m -> Flow (Context m) (Type m)
findType Term m
term = do
      Context m
cx <- forall s. Flow s s
getState
      Maybe (Type m)
mt <- forall m.
AnnotationClass m -> Term m -> Flow (Context m) (Maybe (Type m))
annotationClassTermType (forall m. Context m -> AnnotationClass m
contextAnnotations Context m
cx) Term m
term
      case Maybe (Type m)
mt of
        Just Type m
t -> forall (m :: * -> *) a. Monad m => a -> m a
return Type m
t
        Maybe (Type m)
Nothing -> forall (m :: * -> *) a. MonadFail m => String -> m a
fail String
"expected a type annotation"

annotateTermWithTypes :: (Ord m, Show m) => Term m -> GraphFlow m (Term m)
annotateTermWithTypes :: forall m. (Ord m, Show m) => Term m -> GraphFlow m (Term m)
annotateTermWithTypes Term m
term0 = do
  (Term (m, Type m, [Constraint m])
term1, TypeScheme m
_) <- forall m.
(Ord m, Show m) =>
Term m
-> GraphFlow m (Term (m, Type m, [Constraint m]), TypeScheme m)
inferType Term m
term0
  AnnotationClass m
anns <- forall m. Context m -> AnnotationClass m
contextAnnotations forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall s. Flow s s
getState
  Maybe (Type m)
mt <- forall m.
AnnotationClass m -> Term m -> Flow (Context m) (Maybe (Type m))
annotationClassTermType AnnotationClass m
anns Term m
term0 -- Use a provided type, if available, rather than the inferred type
  let annotType :: (m, Type m, c) -> m
annotType (m
ann, Type m
typ, c
_) = forall m. AnnotationClass m -> Maybe (Type m) -> m -> m
annotationClassSetTypeOf AnnotationClass m
anns (forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ forall a. a -> Maybe a -> a
Y.fromMaybe Type m
typ Maybe (Type m)
mt) m
ann
  forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall b a. Ord b => (a -> b) -> Term a -> Term b
rewriteTermMeta forall {c}. (m, Type m, c) -> m
annotType Term (m, Type m, [Constraint m])
term1

-- Decode a type, eliminating nominal types for the sake of unification
decodeStructuralType :: Show m => Term m -> GraphFlow m (Type m)
decodeStructuralType :: forall m. Show m => Term m -> GraphFlow m (Type m)
decodeStructuralType Term m
term = do
  Type m
typ <- forall m. Show m => Term m -> GraphFlow m (Type m)
decodeType Term m
term
  let typ' :: Type m
typ' = forall m. Type m -> Type m
stripType Type m
typ
  case Type m
typ' of
    TypeNominal Name
name -> forall m a. GraphFlow m a -> GraphFlow m a
withSchemaContext forall a b. (a -> b) -> a -> b
$ forall s a. String -> Flow s a -> Flow s a
withTrace String
"decode structural type" forall a b. (a -> b) -> a -> b
$ do
      Element m
el <- forall m. Name -> GraphFlow m (Element m)
requireElement Name
name
      forall m. Show m => Term m -> GraphFlow m (Type m)
decodeStructuralType forall a b. (a -> b) -> a -> b
$ forall m. Element m -> Term m
elementData Element m
el
    Type m
_ -> forall (f :: * -> *) a. Applicative f => a -> f a
pure Type m
typ

freshVariableType :: Flow (InferenceContext m) (Type m)
freshVariableType :: forall m. Flow (InferenceContext m) (Type m)
freshVariableType = do
    (Context m
cx, Int
s, TypingEnvironment m
e) <- forall s. Flow s s
getState
    forall s. s -> Flow s ()
putState (Context m
cx, Int
s forall a. Num a => a -> a -> a
+ Int
1, TypingEnvironment m
e)
    forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall m. String -> Type m
Types.variable (VariableType -> String
unVariableType forall a b. (a -> b) -> a -> b
$ [VariableType]
normalVariables forall a. [a] -> Int -> a
!! Int
s)

generalize :: Show m => TypingEnvironment m -> Type m -> TypeScheme m
generalize :: forall m. Show m => TypingEnvironment m -> Type m -> TypeScheme m
generalize TypingEnvironment m
env Type m
t  = forall m. [VariableType] -> Type m -> TypeScheme m
TypeScheme [VariableType]
vars Type m
t
  where
    vars :: [VariableType]
vars = forall a. Set a -> [a]
S.toList forall a b. (a -> b) -> a -> b
$ forall a. Ord a => Set a -> Set a -> Set a
S.difference
      (forall m. Type m -> Set VariableType
freeVariablesInType Type m
t)
      (forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
L.foldr (forall a. Ord a => Set a -> Set a -> Set a
S.union forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall m. Show m => TypeScheme m -> Set VariableType
freeVariablesInScheme) forall a. Set a
S.empty forall a b. (a -> b) -> a -> b
$ forall k a. Map k a -> [a]
M.elems TypingEnvironment m
env)

extendEnvironment :: Variable -> TypeScheme m -> Flow (InferenceContext m) a -> Flow (InferenceContext m) a
extendEnvironment :: forall m a.
Variable
-> TypeScheme m
-> Flow (InferenceContext m) a
-> Flow (InferenceContext m) a
extendEnvironment Variable
x TypeScheme m
sc = forall m a.
(TypingEnvironment m -> TypingEnvironment m)
-> Flow (InferenceContext m) a -> Flow (InferenceContext m) a
withEnvironment (\TypingEnvironment m
e -> forall k a. Ord k => k -> a -> Map k a -> Map k a
M.insert Variable
x TypeScheme m
sc forall a b. (a -> b) -> a -> b
$ forall k a. Ord k => k -> Map k a -> Map k a
M.delete Variable
x TypingEnvironment m
e)

findMatchingField :: Show m => FieldName -> [FieldType m] -> Flow (InferenceContext m) (FieldType m)
findMatchingField :: forall m.
Show m =>
FieldName
-> [FieldType m] -> Flow (InferenceContext m) (FieldType m)
findMatchingField FieldName
fname [FieldType m]
sfields = case forall a. (a -> Bool) -> [a] -> [a]
L.filter (\FieldType m
f -> forall m. FieldType m -> FieldName
fieldTypeName FieldType m
f forall a. Eq a => a -> a -> Bool
== FieldName
fname) [FieldType m]
sfields of
  []    -> forall (m :: * -> *) a. MonadFail m => String -> m a
fail forall a b. (a -> b) -> a -> b
$ String
"no such field: " forall a. [a] -> [a] -> [a]
++ FieldName -> String
unFieldName FieldName
fname
  (FieldType m
h:[FieldType m]
_) -> forall (m :: * -> *) a. Monad m => a -> m a
return FieldType m
h

infer :: (Ord m, Show m) => Term m -> Flow (InferenceContext m) (Term (m, Type m, [Constraint m]))
infer :: forall m.
(Ord m, Show m) =>
Term m
-> Flow (InferenceContext m) (Term (m, Type m, [Constraint m]))
infer Term m
term = do
  (Context m
cx, Int
_, TypingEnvironment m
_) <- forall s. Flow s s
getState
  Maybe (Type m)
mt <- forall m a. GraphFlow m a -> Flow (InferenceContext m) a
withGraphContext forall a b. (a -> b) -> a -> b
$ forall m.
AnnotationClass m -> Term m -> Flow (Context m) (Maybe (Type m))
annotationClassTermType (forall m. Context m -> AnnotationClass m
contextAnnotations Context m
cx) Term m
term
  case Maybe (Type m)
mt of
    Just Type m
typ -> do
      Term (m, Type m, [Constraint m])
i <- forall m.
(Ord m, Show m) =>
Term m
-> Flow (InferenceContext m) (Term (m, Type m, [Constraint m]))
inferInternal Term m
term
      forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall m. Annotated (Term m) m -> Term m
TermAnnotated forall a b. (a -> b) -> a -> b
$ forall a m. a -> m -> Annotated a m
Annotated Term (m, Type m, [Constraint m])
i (forall m. Context m -> Term m -> m
termMeta Context m
cx Term m
term, Type m
typ, []) -- TODO: unify "suggested" types with inferred types
    Maybe (Type m)
Nothing -> forall m.
(Ord m, Show m) =>
Term m
-> Flow (InferenceContext m) (Term (m, Type m, [Constraint m]))
inferInternal Term m
term

inferInternal :: (Ord m, Show m) => Term m -> Flow (InferenceContext m) (Term (m, Type m, [Constraint m]))
inferInternal :: forall m.
(Ord m, Show m) =>
Term m
-> Flow (InferenceContext m) (Term (m, Type m, [Constraint m]))
inferInternal Term m
term = case Term m
term of
    TermAnnotated (Annotated Term m
term1 m
ann) -> do
      Term (m, Type m, [Constraint m])
iterm <- forall m.
(Ord m, Show m) =>
Term m
-> Flow (InferenceContext m) (Term (m, Type m, [Constraint m]))
infer Term m
term1
      forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ case Term (m, Type m, [Constraint m])
iterm of
        -- `yield` produces the default annotation, which can just be replaced
        TermAnnotated (Annotated Term (m, Type m, [Constraint m])
trm (m
_, Type m
t, [Constraint m]
c)) -> forall m. Annotated (Term m) m -> Term m
TermAnnotated (forall a m. a -> m -> Annotated a m
Annotated Term (m, Type m, [Constraint m])
trm (m
ann, Type m
t, [Constraint m]
c))

    TermApplication (Application Term m
fun Term m
arg) -> do
      Term (m, Type m, [Constraint m])
ifun <- forall m.
(Ord m, Show m) =>
Term m
-> Flow (InferenceContext m) (Term (m, Type m, [Constraint m]))
infer Term m
fun
      Term (m, Type m, [Constraint m])
iarg <- forall m.
(Ord m, Show m) =>
Term m
-> Flow (InferenceContext m) (Term (m, Type m, [Constraint m]))
infer Term m
arg
      Type m
v <- forall m. Flow (InferenceContext m) (Type m)
freshVariableType
      let c :: [Constraint m]
c = (forall m. Term (m, Type m, [Constraint m]) -> [Constraint m]
termConstraints Term (m, Type m, [Constraint m])
ifun) forall a. [a] -> [a] -> [a]
++ (forall m. Term (m, Type m, [Constraint m]) -> [Constraint m]
termConstraints Term (m, Type m, [Constraint m])
iarg) forall a. [a] -> [a] -> [a]
++ [(forall m. Term (m, Type m, [Constraint m]) -> Type m
termType Term (m, Type m, [Constraint m])
ifun, forall m. Type m -> Type m -> Type m
Types.function (forall m. Term (m, Type m, [Constraint m]) -> Type m
termType Term (m, Type m, [Constraint m])
iarg) Type m
v)]
      let app :: Term (m, Type m, [Constraint m])
app = forall m. Application m -> Term m
TermApplication forall a b. (a -> b) -> a -> b
$ forall m. Term m -> Term m -> Application m
Application Term (m, Type m, [Constraint m])
ifun Term (m, Type m, [Constraint m])
iarg
      forall {a} {b} {c} {b} {c}.
Term (a, b, c) -> b -> c -> Flow (Context a, b, c) (Term (a, b, c))
yield Term (m, Type m, [Constraint m])
app Type m
v [Constraint m]
c

    TermElement Name
name -> do
      Type m
et <- forall m a. GraphFlow m a -> Flow (InferenceContext m) a
withGraphContext forall a b. (a -> b) -> a -> b
$ forall m. Show m => Name -> GraphFlow m (Type m)
typeOfElement Name
name
      forall {a} {b} {c} {b} {c}.
Term (a, b, c) -> b -> c -> Flow (Context a, b, c) (Term (a, b, c))
yield (forall m. Name -> Term m
TermElement Name
name) (forall m. Type m -> Type m
Types.element Type m
et) []

    TermFunction Function m
f -> case Function m
f of

      -- Note: here we assume that compareTo evaluates to an integer, not a Comparison value.
      --       For the latter, Comparison would have to be added to the literal type grammar.
      FunctionCompareTo Term m
other -> do
        Term (m, Type m, [Constraint m])
i <- forall m.
(Ord m, Show m) =>
Term m
-> Flow (InferenceContext m) (Term (m, Type m, [Constraint m]))
infer Term m
other
        forall {a} {b} {c} {b} {c}.
Function (a, b, c)
-> b -> c -> Flow (Context a, b, c) (Term (a, b, c))
yieldFunction (forall m. Term m -> Function m
FunctionCompareTo Term (m, Type m, [Constraint m])
i) (forall m. Type m -> Type m -> Type m
Types.function (forall m. Term (m, Type m, [Constraint m]) -> Type m
termType Term (m, Type m, [Constraint m])
i) forall m. Type m
Types.int8) (forall m. Term (m, Type m, [Constraint m]) -> [Constraint m]
termConstraints Term (m, Type m, [Constraint m])
i)

      FunctionElimination Elimination m
e -> case Elimination m
e of

        Elimination m
EliminationElement -> do
          Type m
et <- forall m. Flow (InferenceContext m) (Type m)
freshVariableType
          forall {a} {b} {c} {b} {c}.
Elimination (a, b, c)
-> b -> c -> Flow (Context a, b, c) (Term (a, b, c))
yieldElimination forall m. Elimination m
EliminationElement (forall m. Type m -> Type m -> Type m
Types.function (forall m. Type m -> Type m
Types.element Type m
et) Type m
et) []

        EliminationList Term m
fun -> do
          Type m
a <- forall m. Flow (InferenceContext m) (Type m)
freshVariableType
          Type m
b <- forall m. Flow (InferenceContext m) (Type m)
freshVariableType
          let expected :: Type m
expected = forall m. [Type m] -> Type m -> Type m
Types.functionN [Type m
b, Type m
a] Type m
b
          Term (m, Type m, [Constraint m])
i <- forall m.
(Ord m, Show m) =>
Term m
-> Flow (InferenceContext m) (Term (m, Type m, [Constraint m]))
infer Term m
fun
          let elim :: Type m
elim = forall m. [Type m] -> Type m -> Type m
Types.functionN [Type m
b, forall m. Type m -> Type m
Types.list Type m
a] Type m
b
          forall {a} {b} {c} {b} {c}.
Elimination (a, b, c)
-> b -> c -> Flow (Context a, b, c) (Term (a, b, c))
yieldElimination (forall m. Term m -> Elimination m
EliminationList Term (m, Type m, [Constraint m])
i) Type m
elim [(Type m
expected, forall m. Term (m, Type m, [Constraint m]) -> Type m
termType Term (m, Type m, [Constraint m])
i)]

        EliminationNominal Name
name -> do
          Type m
typ <- forall m a. GraphFlow m a -> Flow (InferenceContext m) a
withGraphContext forall a b. (a -> b) -> a -> b
$ forall m. Show m => String -> Name -> GraphFlow m (Type m)
namedType String
"eliminate nominal" Name
name
          forall {a} {b} {c} {b} {c}.
Elimination (a, b, c)
-> b -> c -> Flow (Context a, b, c) (Term (a, b, c))
yieldElimination (forall m. Name -> Elimination m
EliminationNominal Name
name) (forall m. Type m -> Type m -> Type m
Types.function (forall m. Name -> Type m
Types.nominal Name
name) Type m
typ) []

        EliminationOptional (OptionalCases Term m
n Term m
j) -> do
          Type m
dom <- forall m. Flow (InferenceContext m) (Type m)
freshVariableType
          Type m
cod <- forall m. Flow (InferenceContext m) (Type m)
freshVariableType
          Term (m, Type m, [Constraint m])
ni <- forall m.
(Ord m, Show m) =>
Term m
-> Flow (InferenceContext m) (Term (m, Type m, [Constraint m]))
infer Term m
n
          Term (m, Type m, [Constraint m])
ji <- forall m.
(Ord m, Show m) =>
Term m
-> Flow (InferenceContext m) (Term (m, Type m, [Constraint m]))
infer Term m
j
          let t :: Type m
t = forall m. Type m -> Type m -> Type m
Types.function (forall m. Type m -> Type m
Types.optional Type m
dom) Type m
cod
          let constraints :: [Constraint m]
constraints = [(Type m
cod, forall m. Term (m, Type m, [Constraint m]) -> Type m
termType Term (m, Type m, [Constraint m])
ni), (forall m. Type m -> Type m -> Type m
Types.function Type m
dom Type m
cod, forall m. Term (m, Type m, [Constraint m]) -> Type m
termType Term (m, Type m, [Constraint m])
ji)]
          forall {a} {b} {c} {b} {c}.
Elimination (a, b, c)
-> b -> c -> Flow (Context a, b, c) (Term (a, b, c))
yieldElimination (forall m. OptionalCases m -> Elimination m
EliminationOptional forall a b. (a -> b) -> a -> b
$ forall m. Term m -> Term m -> OptionalCases m
OptionalCases Term (m, Type m, [Constraint m])
ni Term (m, Type m, [Constraint m])
ji) Type m
t [Constraint m]
constraints

        -- Note: type inference cannot recover complete record types from projections; type annotations are needed
        EliminationRecord (Projection Name
name FieldName
fname) -> do
          RowType m
rt <- forall m a. GraphFlow m a -> Flow (InferenceContext m) a
withGraphContext forall a b. (a -> b) -> a -> b
$ forall m. Show m => Bool -> Name -> GraphFlow m (RowType m)
requireRecordType Bool
True Name
name
          FieldType m
sfield <- forall m.
Show m =>
FieldName
-> [FieldType m] -> Flow (InferenceContext m) (FieldType m)
findMatchingField FieldName
fname (forall m. RowType m -> [FieldType m]
rowTypeFields RowType m
rt)
          forall {a} {b} {c} {b} {c}.
Elimination (a, b, c)
-> b -> c -> Flow (Context a, b, c) (Term (a, b, c))
yieldElimination (forall m. Projection -> Elimination m
EliminationRecord forall a b. (a -> b) -> a -> b
$ Name -> FieldName -> Projection
Projection Name
name FieldName
fname)
            (forall m. Type m -> Type m -> Type m
Types.function (forall m. RowType m -> Type m
TypeRecord RowType m
rt) forall a b. (a -> b) -> a -> b
$ forall m. FieldType m -> Type m
fieldTypeType FieldType m
sfield) []

        EliminationUnion (CaseStatement Name
name [Field m]
cases) -> do
            RowType m
rt <- forall m a. GraphFlow m a -> Flow (InferenceContext m) a
withGraphContext forall a b. (a -> b) -> a -> b
$ forall m. Show m => Bool -> Name -> GraphFlow m (RowType m)
requireUnionType Bool
True Name
name
            let sfields :: [FieldType m]
sfields = forall m. RowType m -> [FieldType m]
rowTypeFields RowType m
rt

            [Field (m, Type m, [Constraint m])]
icases <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
CM.mapM forall m.
(Ord m, Show m) =>
Field m
-> Flow (InferenceContext m) (Field (m, Type m, [Constraint m]))
inferFieldType [Field m]
cases
            let innerConstraints :: [Constraint m]
innerConstraints = forall (t :: * -> *) a. Foldable t => t [a] -> [a]
L.concat (forall m. Term (m, Type m, [Constraint m]) -> [Constraint m]
termConstraints forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall m. Field m -> Term m
fieldTerm forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Field (m, Type m, [Constraint m])]
icases)

            let idoms :: [Type m]
idoms = forall m. Term (m, Type m, [Constraint m]) -> Type m
termType forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall m. Field m -> Term m
fieldTerm forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Field (m, Type m, [Constraint m])]
icases
            let sdoms :: [Type m]
sdoms = forall m. FieldType m -> Type m
fieldTypeType forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [FieldType m]
sfields
            Type m
cod <- forall m. Flow (InferenceContext m) (Type m)
freshVariableType
            let outerConstraints :: [Constraint m]
outerConstraints = forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
L.zipWith (\Type m
t Type m
d -> (Type m
t, forall m. Type m -> Type m -> Type m
Types.function Type m
d Type m
cod)) [Type m]
idoms [Type m]
sdoms

            forall {a} {b} {c} {b} {c}.
Elimination (a, b, c)
-> b -> c -> Flow (Context a, b, c) (Term (a, b, c))
yieldElimination (forall m. CaseStatement m -> Elimination m
EliminationUnion (forall m. Name -> [Field m] -> CaseStatement m
CaseStatement Name
name [Field (m, Type m, [Constraint m])]
icases))
              (forall m. Type m -> Type m -> Type m
Types.function (forall m. RowType m -> Type m
TypeUnion RowType m
rt) Type m
cod)
              ([Constraint m]
innerConstraints forall a. [a] -> [a] -> [a]
++ [Constraint m]
outerConstraints)

      FunctionLambda (Lambda Variable
v Term m
body) -> do
        Type m
tv <- forall m. Flow (InferenceContext m) (Type m)
freshVariableType
        Term (m, Type m, [Constraint m])
i <- forall m a.
Variable
-> TypeScheme m
-> Flow (InferenceContext m) a
-> Flow (InferenceContext m) a
extendEnvironment Variable
v (forall m. [VariableType] -> Type m -> TypeScheme m
TypeScheme [] Type m
tv) forall a b. (a -> b) -> a -> b
$ forall m.
(Ord m, Show m) =>
Term m
-> Flow (InferenceContext m) (Term (m, Type m, [Constraint m]))
infer Term m
body
        forall {a} {b} {c} {b} {c}.
Function (a, b, c)
-> b -> c -> Flow (Context a, b, c) (Term (a, b, c))
yieldFunction (forall m. Lambda m -> Function m
FunctionLambda forall a b. (a -> b) -> a -> b
$ forall m. Variable -> Term m -> Lambda m
Lambda Variable
v Term (m, Type m, [Constraint m])
i) (forall m. Type m -> Type m -> Type m
Types.function Type m
tv (forall m. Term (m, Type m, [Constraint m]) -> Type m
termType Term (m, Type m, [Constraint m])
i)) (forall m. Term (m, Type m, [Constraint m]) -> [Constraint m]
termConstraints Term (m, Type m, [Constraint m])
i)

      FunctionPrimitive Name
name -> do
        FunctionType Type m
dom Type m
cod <- forall m a. GraphFlow m a -> Flow (InferenceContext m) a
withGraphContext forall a b. (a -> b) -> a -> b
$ forall m. Name -> GraphFlow m (FunctionType m)
typeOfPrimitiveFunction Name
name
        forall {a} {b} {c} {b} {c}.
Function (a, b, c)
-> b -> c -> Flow (Context a, b, c) (Term (a, b, c))
yieldFunction (forall m. Name -> Function m
FunctionPrimitive Name
name) (forall m. Type m -> Type m -> Type m
Types.function Type m
dom Type m
cod) []

    TermLet (Let Variable
x Term m
e1 Term m
e2) -> do
      (Context m
_, Int
_, TypingEnvironment m
env) <- forall s. Flow s s
getState
      Term (m, Type m, [Constraint m])
i1 <- forall m.
(Ord m, Show m) =>
Term m
-> Flow (InferenceContext m) (Term (m, Type m, [Constraint m]))
infer Term m
e1
      let t1 :: Type m
t1 = forall m. Term (m, Type m, [Constraint m]) -> Type m
termType Term (m, Type m, [Constraint m])
i1
      let c1 :: [Constraint m]
c1 = forall m. Term (m, Type m, [Constraint m]) -> [Constraint m]
termConstraints Term (m, Type m, [Constraint m])
i1
      Subst m
sub <- forall m a. GraphFlow m a -> Flow (InferenceContext m) a
withGraphContext forall a b. (a -> b) -> a -> b
$ forall m. (Eq m, Show m) => [Constraint m] -> GraphFlow m (Subst m)
solveConstraints [Constraint m]
c1
      let t1' :: Type m
t1' = forall m. (Ord m, Show m) => Type m -> Type m
reduceType forall a b. (a -> b) -> a -> b
$ forall m. Map VariableType (Type m) -> Type m -> Type m
substituteInType Subst m
sub Type m
t1
      let sc :: TypeScheme m
sc = forall m. Show m => TypingEnvironment m -> Type m -> TypeScheme m
generalize (forall a b k. (a -> b) -> Map k a -> Map k b
M.map (forall m. Map VariableType (Type m) -> TypeScheme m -> TypeScheme m
substituteInScheme Subst m
sub) TypingEnvironment m
env) Type m
t1'
      Term (m, Type m, [Constraint m])
i2 <- forall m a.
Variable
-> TypeScheme m
-> Flow (InferenceContext m) a
-> Flow (InferenceContext m) a
extendEnvironment Variable
x TypeScheme m
sc forall a b. (a -> b) -> a -> b
$ forall m a.
(TypingEnvironment m -> TypingEnvironment m)
-> Flow (InferenceContext m) a -> Flow (InferenceContext m) a
withEnvironment (forall a b k. (a -> b) -> Map k a -> Map k b
M.map (forall m. Map VariableType (Type m) -> TypeScheme m -> TypeScheme m
substituteInScheme Subst m
sub)) forall a b. (a -> b) -> a -> b
$ forall m.
(Ord m, Show m) =>
Term m
-> Flow (InferenceContext m) (Term (m, Type m, [Constraint m]))
infer Term m
e2
      let t2 :: Type m
t2 = forall m. Term (m, Type m, [Constraint m]) -> Type m
termType Term (m, Type m, [Constraint m])
i2
      let c2 :: [Constraint m]
c2 = forall m. Term (m, Type m, [Constraint m]) -> [Constraint m]
termConstraints Term (m, Type m, [Constraint m])
i2
      forall {a} {b} {c} {b} {c}.
Term (a, b, c) -> b -> c -> Flow (Context a, b, c) (Term (a, b, c))
yield (forall m. Let m -> Term m
TermLet forall a b. (a -> b) -> a -> b
$ forall m. Variable -> Term m -> Term m -> Let m
Let Variable
x Term (m, Type m, [Constraint m])
i1 Term (m, Type m, [Constraint m])
i2) Type m
t2 ([Constraint m]
c1 forall a. [a] -> [a] -> [a]
++ [Constraint m]
c2) -- TODO: is x constant?

    TermList [Term m]
els -> do
      Type m
v <- forall m. Flow (InferenceContext m) (Type m)
freshVariableType
      [Term (m, Type m, [Constraint m])]
iels <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
CM.mapM forall m.
(Ord m, Show m) =>
Term m
-> Flow (InferenceContext m) (Term (m, Type m, [Constraint m]))
infer [Term m]
els
      let co :: [Constraint m]
co = (\Term (m, Type m, [Constraint m])
e -> (Type m
v, forall m. Term (m, Type m, [Constraint m]) -> Type m
termType Term (m, Type m, [Constraint m])
e)) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Term (m, Type m, [Constraint m])]
iels
      let ci :: [Constraint m]
ci = forall (t :: * -> *) a. Foldable t => t [a] -> [a]
L.concat (forall m. Term (m, Type m, [Constraint m]) -> [Constraint m]
termConstraints forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Term (m, Type m, [Constraint m])]
iels)
      forall {a} {b} {c} {b} {c}.
Term (a, b, c) -> b -> c -> Flow (Context a, b, c) (Term (a, b, c))
yield (forall m. [Term m] -> Term m
TermList [Term (m, Type m, [Constraint m])]
iels) (forall m. Type m -> Type m
Types.list Type m
v) ([Constraint m]
co forall a. [a] -> [a] -> [a]
++ [Constraint m]
ci)

    TermLiteral Literal
l -> forall {a} {b} {c} {b} {c}.
Term (a, b, c) -> b -> c -> Flow (Context a, b, c) (Term (a, b, c))
yield (forall m. Literal -> Term m
TermLiteral Literal
l) (forall m. LiteralType -> Type m
Types.literal forall a b. (a -> b) -> a -> b
$ Literal -> LiteralType
literalType Literal
l) []

    TermMap Map (Term m) (Term m)
m -> do
        Type m
kv <- forall m. Flow (InferenceContext m) (Type m)
freshVariableType
        Type m
vv <- forall m. Flow (InferenceContext m) (Type m)
freshVariableType
        [(Term (m, Type m, [Constraint m]),
  Term (m, Type m, [Constraint m]))]
pairs <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
CM.mapM forall {m}.
(Ord m, Show m) =>
(Term m, Term m)
-> Flow
     (InferenceContext m)
     (Term (m, Type m, [Constraint m]),
      Term (m, Type m, [Constraint m]))
toPair forall a b. (a -> b) -> a -> b
$ forall k a. Map k a -> [(k, a)]
M.toList Map (Term m) (Term m)
m
        let co :: [Constraint m]
co = forall (t :: * -> *) a. Foldable t => t [a] -> [a]
L.concat ((\(Term (m, Type m, [Constraint m])
k, Term (m, Type m, [Constraint m])
v) -> [(Type m
kv, forall m. Term (m, Type m, [Constraint m]) -> Type m
termType Term (m, Type m, [Constraint m])
k), (Type m
vv, forall m. Term (m, Type m, [Constraint m]) -> Type m
termType Term (m, Type m, [Constraint m])
v)]) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(Term (m, Type m, [Constraint m]),
  Term (m, Type m, [Constraint m]))]
pairs)
        let ci :: [Constraint m]
ci = forall (t :: * -> *) a. Foldable t => t [a] -> [a]
L.concat ((\(Term (m, Type m, [Constraint m])
k, Term (m, Type m, [Constraint m])
v) -> forall m. Term (m, Type m, [Constraint m]) -> [Constraint m]
termConstraints Term (m, Type m, [Constraint m])
k forall a. [a] -> [a] -> [a]
++ forall m. Term (m, Type m, [Constraint m]) -> [Constraint m]
termConstraints Term (m, Type m, [Constraint m])
v) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(Term (m, Type m, [Constraint m]),
  Term (m, Type m, [Constraint m]))]
pairs)
        forall {a} {b} {c} {b} {c}.
Term (a, b, c) -> b -> c -> Flow (Context a, b, c) (Term (a, b, c))
yield (forall m. Map (Term m) (Term m) -> Term m
TermMap forall a b. (a -> b) -> a -> b
$ forall k a. Ord k => [(k, a)] -> Map k a
M.fromList [(Term (m, Type m, [Constraint m]),
  Term (m, Type m, [Constraint m]))]
pairs) (forall m. Type m -> Type m -> Type m
Types.map Type m
kv Type m
vv) ([Constraint m]
co forall a. [a] -> [a] -> [a]
++ [Constraint m]
ci)
      where
        toPair :: (Term m, Term m)
-> Flow
     (InferenceContext m)
     (Term (m, Type m, [Constraint m]),
      Term (m, Type m, [Constraint m]))
toPair (Term m
k, Term m
v) = do
          Term (m, Type m, [Constraint m])
ik <- forall m.
(Ord m, Show m) =>
Term m
-> Flow (InferenceContext m) (Term (m, Type m, [Constraint m]))
infer Term m
k
          Term (m, Type m, [Constraint m])
iv <- forall m.
(Ord m, Show m) =>
Term m
-> Flow (InferenceContext m) (Term (m, Type m, [Constraint m]))
infer Term m
v
          forall (m :: * -> *) a. Monad m => a -> m a
return (Term (m, Type m, [Constraint m])
ik, Term (m, Type m, [Constraint m])
iv)

    TermNominal (Named Name
name Term m
term1) -> do
      Type m
typ <- forall m a. GraphFlow m a -> Flow (InferenceContext m) a
withGraphContext forall a b. (a -> b) -> a -> b
$ forall m. Show m => String -> Name -> GraphFlow m (Type m)
namedType String
"nominal" Name
name
      Term (m, Type m, [Constraint m])
i <- forall m.
(Ord m, Show m) =>
Term m
-> Flow (InferenceContext m) (Term (m, Type m, [Constraint m]))
infer Term m
term1
      forall {a} {b} {c} {b} {c}.
Term (a, b, c) -> b -> c -> Flow (Context a, b, c) (Term (a, b, c))
yield (forall m. Named m -> Term m
TermNominal forall a b. (a -> b) -> a -> b
$ forall m. Name -> Term m -> Named m
Named Name
name Term (m, Type m, [Constraint m])
i) (forall m. Name -> Type m
Types.nominal Name
name) (forall m. Term (m, Type m, [Constraint m]) -> [Constraint m]
termConstraints Term (m, Type m, [Constraint m])
i forall a. [a] -> [a] -> [a]
++ [(Type m
typ, forall m. Term (m, Type m, [Constraint m]) -> Type m
termType Term (m, Type m, [Constraint m])
i)])

    TermOptional Maybe (Term m)
m -> do
      Type m
v <- forall m. Flow (InferenceContext m) (Type m)
freshVariableType
      case Maybe (Term m)
m of
        Maybe (Term m)
Nothing -> forall {a} {b} {c} {b} {c}.
Term (a, b, c) -> b -> c -> Flow (Context a, b, c) (Term (a, b, c))
yield (forall m. Maybe (Term m) -> Term m
TermOptional forall a. Maybe a
Nothing) (forall m. Type m -> Type m
Types.optional Type m
v) []
        Just Term m
e -> do
          Term (m, Type m, [Constraint m])
i <- forall m.
(Ord m, Show m) =>
Term m
-> Flow (InferenceContext m) (Term (m, Type m, [Constraint m]))
infer Term m
e
          forall {a} {b} {c} {b} {c}.
Term (a, b, c) -> b -> c -> Flow (Context a, b, c) (Term (a, b, c))
yield (forall m. Maybe (Term m) -> Term m
TermOptional forall a b. (a -> b) -> a -> b
$ forall a. a -> Maybe a
Just Term (m, Type m, [Constraint m])
i) (forall m. Type m -> Type m
Types.optional Type m
v) ((Type m
v, forall m. Term (m, Type m, [Constraint m]) -> Type m
termType Term (m, Type m, [Constraint m])
i)forall a. a -> [a] -> [a]
:(forall m. Term (m, Type m, [Constraint m]) -> [Constraint m]
termConstraints Term (m, Type m, [Constraint m])
i))

    TermProduct [Term m]
tuple -> do
      [Term (m, Type m, [Constraint m])]
is <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
CM.mapM forall m.
(Ord m, Show m) =>
Term m
-> Flow (InferenceContext m) (Term (m, Type m, [Constraint m]))
infer [Term m]
tuple
      forall {a} {b} {c} {b} {c}.
Term (a, b, c) -> b -> c -> Flow (Context a, b, c) (Term (a, b, c))
yield (forall m. [Term m] -> Term m
TermProduct [Term (m, Type m, [Constraint m])]
is) (forall m. [Type m] -> Type m
TypeProduct forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall m. Term (m, Type m, [Constraint m]) -> Type m
termType [Term (m, Type m, [Constraint m])]
is) (forall (t :: * -> *) a. Foldable t => t [a] -> [a]
L.concat forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall m. Term (m, Type m, [Constraint m]) -> [Constraint m]
termConstraints [Term (m, Type m, [Constraint m])]
is)

    TermRecord (Record Name
n [Field m]
fields) -> do
        RowType m
rt <- forall m a. GraphFlow m a -> Flow (InferenceContext m) a
withGraphContext forall a b. (a -> b) -> a -> b
$ forall m. Show m => Bool -> Name -> GraphFlow m (RowType m)
requireRecordType Bool
True Name
n
        let sfields :: [FieldType m]
sfields = forall m. RowType m -> [FieldType m]
rowTypeFields RowType m
rt
        ([Field (m, Type m, [Constraint m])]
fields0, [FieldType m]
ftypes0, [Constraint m]
c1) <- forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
CM.foldM forall {m}.
(Ord m, Show m) =>
([Field (m, Type m, [Constraint m])], [FieldType m],
 [Constraint m])
-> (Field m, FieldType m)
-> Flow
     (InferenceContext m)
     ([Field (m, Type m, [Constraint m])], [FieldType m],
      [Constraint m])
forField ([], [], []) forall a b. (a -> b) -> a -> b
$ forall a b. [a] -> [b] -> [(a, b)]
L.zip [Field m]
fields [FieldType m]
sfields
        forall {a} {b} {c} {b} {c}.
Term (a, b, c) -> b -> c -> Flow (Context a, b, c) (Term (a, b, c))
yield (forall m. Record m -> Term m
TermRecord forall a b. (a -> b) -> a -> b
$ forall m. Name -> [Field m] -> Record m
Record Name
n forall a b. (a -> b) -> a -> b
$ forall a. [a] -> [a]
L.reverse [Field (m, Type m, [Constraint m])]
fields0) (forall m. RowType m -> Type m
TypeRecord forall a b. (a -> b) -> a -> b
$ forall m. Name -> Maybe Name -> [FieldType m] -> RowType m
RowType Name
n (forall m. RowType m -> Maybe Name
rowTypeExtends RowType m
rt) forall a b. (a -> b) -> a -> b
$ forall a. [a] -> [a]
L.reverse [FieldType m]
ftypes0) [Constraint m]
c1
      where
        forField :: ([Field (m, Type m, [Constraint m])], [FieldType m],
 [Constraint m])
-> (Field m, FieldType m)
-> Flow
     (InferenceContext m)
     ([Field (m, Type m, [Constraint m])], [FieldType m],
      [Constraint m])
forField ([Field (m, Type m, [Constraint m])]
typed, [FieldType m]
ftypes, [Constraint m]
c) (Field m
field, FieldType m
sfield) = do
          Field (m, Type m, [Constraint m])
i <- forall m.
(Ord m, Show m) =>
Field m
-> Flow (InferenceContext m) (Field (m, Type m, [Constraint m]))
inferFieldType Field m
field
          let ft :: Type m
ft = forall m. Term (m, Type m, [Constraint m]) -> Type m
termType forall a b. (a -> b) -> a -> b
$ forall m. Field m -> Term m
fieldTerm Field (m, Type m, [Constraint m])
i
          let cinternal :: [Constraint m]
cinternal = forall m. Term (m, Type m, [Constraint m]) -> [Constraint m]
termConstraints forall a b. (a -> b) -> a -> b
$ forall m. Field m -> Term m
fieldTerm Field (m, Type m, [Constraint m])
i
          let cnominal :: Constraint m
cnominal = (Type m
ft, forall m. FieldType m -> Type m
fieldTypeType FieldType m
sfield)
          forall (m :: * -> *) a. Monad m => a -> m a
return (Field (m, Type m, [Constraint m])
iforall a. a -> [a] -> [a]
:[Field (m, Type m, [Constraint m])]
typed, (forall m. FieldName -> Type m -> FieldType m
FieldType (forall m. Field m -> FieldName
fieldName Field m
field) Type m
ft)forall a. a -> [a] -> [a]
:[FieldType m]
ftypes, Constraint m
cnominalforall a. a -> [a] -> [a]
:([Constraint m]
cinternal forall a. [a] -> [a] -> [a]
++ [Constraint m]
c))

    TermSet Set (Term m)
els -> do
      Type m
v <- forall m. Flow (InferenceContext m) (Type m)
freshVariableType
      [Term (m, Type m, [Constraint m])]
iels <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
CM.mapM forall m.
(Ord m, Show m) =>
Term m
-> Flow (InferenceContext m) (Term (m, Type m, [Constraint m]))
infer forall a b. (a -> b) -> a -> b
$ forall a. Set a -> [a]
S.toList Set (Term m)
els
      let co :: [Constraint m]
co = (\Term (m, Type m, [Constraint m])
e -> (Type m
v, forall m. Term (m, Type m, [Constraint m]) -> Type m
termType Term (m, Type m, [Constraint m])
e)) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Term (m, Type m, [Constraint m])]
iels
      let ci :: [Constraint m]
ci = forall (t :: * -> *) a. Foldable t => t [a] -> [a]
L.concat (forall m. Term (m, Type m, [Constraint m]) -> [Constraint m]
termConstraints forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Term (m, Type m, [Constraint m])]
iels)
      forall {a} {b} {c} {b} {c}.
Term (a, b, c) -> b -> c -> Flow (Context a, b, c) (Term (a, b, c))
yield (forall m. Set (Term m) -> Term m
TermSet forall a b. (a -> b) -> a -> b
$ forall a. Ord a => [a] -> Set a
S.fromList [Term (m, Type m, [Constraint m])]
iels) (forall m. Type m -> Type m
Types.set Type m
v) ([Constraint m]
co forall a. [a] -> [a] -> [a]
++ [Constraint m]
ci)

    TermSum (Sum Int
i Int
s Term m
trm) -> do
        Term (m, Type m, [Constraint m])
it <- forall m.
(Ord m, Show m) =>
Term m
-> Flow (InferenceContext m) (Term (m, Type m, [Constraint m]))
infer Term m
trm
        [Type m]
types <- forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
CM.sequence (forall {m}.
Term (m, Type m, [Constraint m])
-> Int -> Flow (InferenceContext m) (Type m)
varOrTerm Term (m, Type m, [Constraint m])
it forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Int
0..(Int
sforall a. Num a => a -> a -> a
-Int
1)])
        forall {a} {b} {c} {b} {c}.
Term (a, b, c) -> b -> c -> Flow (Context a, b, c) (Term (a, b, c))
yield (forall m. Sum m -> Term m
TermSum forall a b. (a -> b) -> a -> b
$ forall m. Int -> Int -> Term m -> Sum m
Sum Int
i Int
s Term (m, Type m, [Constraint m])
it) (forall m. [Type m] -> Type m
TypeSum [Type m]
types) (forall m. Term (m, Type m, [Constraint m]) -> [Constraint m]
termConstraints Term (m, Type m, [Constraint m])
it)
      where
        varOrTerm :: Term (m, Type m, [Constraint m])
-> Int -> Flow (InferenceContext m) (Type m)
varOrTerm Term (m, Type m, [Constraint m])
it Int
j = if Int
i forall a. Eq a => a -> a -> Bool
== Int
j
          then forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall m. Term (m, Type m, [Constraint m]) -> Type m
termType Term (m, Type m, [Constraint m])
it
          else forall m. Flow (InferenceContext m) (Type m)
freshVariableType

    -- Note: type inference cannot recover complete union types from union values; type annotations are needed
    TermUnion (Union Name
n Field m
field) -> do
        RowType m
rt <- forall m a. GraphFlow m a -> Flow (InferenceContext m) a
withGraphContext forall a b. (a -> b) -> a -> b
$ forall m. Show m => Bool -> Name -> GraphFlow m (RowType m)
requireUnionType Bool
True Name
n
        FieldType m
sfield <- forall m.
Show m =>
FieldName
-> [FieldType m] -> Flow (InferenceContext m) (FieldType m)
findMatchingField (forall m. Field m -> FieldName
fieldName Field m
field) (forall m. RowType m -> [FieldType m]
rowTypeFields RowType m
rt)
        Field (m, Type m, [Constraint m])
ifield <- forall m.
(Ord m, Show m) =>
Field m
-> Flow (InferenceContext m) (Field (m, Type m, [Constraint m]))
inferFieldType Field m
field
        let cinternal :: [Constraint m]
cinternal = forall m. Term (m, Type m, [Constraint m]) -> [Constraint m]
termConstraints forall a b. (a -> b) -> a -> b
$ forall m. Field m -> Term m
fieldTerm Field (m, Type m, [Constraint m])
ifield
        let cnominal :: Constraint m
cnominal = (forall m. Term (m, Type m, [Constraint m]) -> Type m
termType forall a b. (a -> b) -> a -> b
$ forall m. Field m -> Term m
fieldTerm Field (m, Type m, [Constraint m])
ifield, forall m. FieldType m -> Type m
fieldTypeType FieldType m
sfield)
        let constraints :: [Constraint m]
constraints = Constraint m
cnominalforall a. a -> [a] -> [a]
:[Constraint m]
cinternal
        forall {a} {b} {c} {b} {c}.
Term (a, b, c) -> b -> c -> Flow (Context a, b, c) (Term (a, b, c))
yield (forall m. Union m -> Term m
TermUnion forall a b. (a -> b) -> a -> b
$ forall m. Name -> Field m -> Union m
Union Name
n Field (m, Type m, [Constraint m])
ifield) (forall m. RowType m -> Type m
TypeUnion RowType m
rt) [Constraint m]
constraints

    TermVariable Variable
x -> do
      Type m
t <- forall m. Show m => Variable -> Flow (InferenceContext m) (Type m)
lookupTypeInEnvironment Variable
x
      forall {a} {b} {c} {b} {c}.
Term (a, b, c) -> b -> c -> Flow (Context a, b, c) (Term (a, b, c))
yield (forall m. Variable -> Term m
TermVariable Variable
x) Type m
t []
  where
    yieldFunction :: Function (a, b, c)
-> b -> c -> Flow (Context a, b, c) (Term (a, b, c))
yieldFunction Function (a, b, c)
fun = forall {a} {b} {c} {b} {c}.
Term (a, b, c) -> b -> c -> Flow (Context a, b, c) (Term (a, b, c))
yield (forall m. Function m -> Term m
TermFunction Function (a, b, c)
fun)

    yieldElimination :: Elimination (a, b, c)
-> b -> c -> Flow (Context a, b, c) (Term (a, b, c))
yieldElimination Elimination (a, b, c)
e = forall {a} {b} {c} {b} {c}.
Term (a, b, c) -> b -> c -> Flow (Context a, b, c) (Term (a, b, c))
yield (forall m. Function m -> Term m
TermFunction forall a b. (a -> b) -> a -> b
$ forall m. Elimination m -> Function m
FunctionElimination Elimination (a, b, c)
e)

    yield :: Term (a, b, c) -> b -> c -> Flow (Context a, b, c) (Term (a, b, c))
yield Term (a, b, c)
term b
typ c
constraints = do
      (Context a
cx, b
_, c
_) <- forall s. Flow s s
getState
      forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall m. Annotated (Term m) m -> Term m
TermAnnotated forall a b. (a -> b) -> a -> b
$ forall a m. a -> m -> Annotated a m
Annotated Term (a, b, c)
term (forall m. AnnotationClass m -> m
annotationClassDefault forall a b. (a -> b) -> a -> b
$ forall m. Context m -> AnnotationClass m
contextAnnotations Context a
cx, b
typ, c
constraints)

inferFieldType :: (Ord m, Show m) => Field m -> Flow (InferenceContext m) (Field (m, Type m, [Constraint m]))
inferFieldType :: forall m.
(Ord m, Show m) =>
Field m
-> Flow (InferenceContext m) (Field (m, Type m, [Constraint m]))
inferFieldType (Field FieldName
fname Term m
term) = forall m. FieldName -> Term m -> Field m
Field FieldName
fname forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall m.
(Ord m, Show m) =>
Term m
-> Flow (InferenceContext m) (Term (m, Type m, [Constraint m]))
infer Term m
term

-- | Solve for the toplevel type of an expression in a given environment
inferType :: (Ord m, Show m) => Term m -> GraphFlow m (Term (m, Type m, [Constraint m]), TypeScheme m)
inferType :: forall m.
(Ord m, Show m) =>
Term m
-> GraphFlow m (Term (m, Type m, [Constraint m]), TypeScheme m)
inferType Term m
term = do
    forall s a. String -> Flow s a -> Flow s a
withTrace (String
"infer type") forall a b. (a -> b) -> a -> b
$ do
--    withTrace ("infer type of " ++ show term) $ do
      Context m
cx <- forall s. Flow s s
getState
      forall s1 a s2. s1 -> Flow s1 a -> Flow s2 a
withState (forall m. Context m -> InferenceContext m
startContext Context m
cx) forall a b. (a -> b) -> a -> b
$ do
        Term (m, Type m, [Constraint m])
term1 <- forall m.
(Ord m, Show m) =>
Term m
-> Flow (InferenceContext m) (Term (m, Type m, [Constraint m]))
infer Term m
term
        forall s a. String -> Flow s a -> Flow s a
withTrace (String
"original term (without annotations): " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (forall m. Ord m => Term m -> Term m
removeTermAnnotations Term m
term) forall a. [a] -> [a] -> [a]
++ String
" ### inferred term: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Term (m, Type m, [Constraint m])
term1) forall a b. (a -> b) -> a -> b
$ do
          Subst m
subst <- forall m a. GraphFlow m a -> Flow (InferenceContext m) a
withGraphContext forall a b. (a -> b) -> a -> b
$ forall m a. GraphFlow m a -> GraphFlow m a
withSchemaContext forall a b. (a -> b) -> a -> b
$ forall m. (Eq m, Show m) => [Constraint m] -> GraphFlow m (Subst m)
solveConstraints (forall m. Term (m, Type m, [Constraint m]) -> [Constraint m]
termConstraints Term (m, Type m, [Constraint m])
term1)
          let term2 :: Term (m, Type m, [Constraint m])
term2 = forall m.
Ord m =>
(Type m -> Type m)
-> Term (m, Type m, [Constraint m])
-> Term (m, Type m, [Constraint m])
rewriteDataType (forall m. Map VariableType (Type m) -> Type m -> Type m
substituteInType Subst m
subst) Term (m, Type m, [Constraint m])
term1
          forall (m :: * -> *) a. Monad m => a -> m a
return (Term (m, Type m, [Constraint m])
term2, Type m -> TypeScheme m
closeOver forall a b. (a -> b) -> a -> b
$ forall m. Term (m, Type m, [Constraint m]) -> Type m
termType Term (m, Type m, [Constraint m])
term2)
  where
    -- | Canonicalize and return the polymorphic toplevel type.
    closeOver :: Type m -> TypeScheme m
closeOver = forall m. Show m => TypeScheme m -> TypeScheme m
normalizeScheme forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall m. Show m => TypingEnvironment m -> Type m -> TypeScheme m
generalize forall k a. Map k a
M.empty forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall m. (Ord m, Show m) => Type m -> Type m
reduceType

instantiate :: TypeScheme m -> Flow (InferenceContext m) (Type m)
instantiate :: forall m. TypeScheme m -> Flow (InferenceContext m) (Type m)
instantiate (TypeScheme [VariableType]
vars Type m
t) = do
    [Type m]
vars1 <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (forall a b. a -> b -> a
const forall m. Flow (InferenceContext m) (Type m)
freshVariableType) [VariableType]
vars
    forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall m. Map VariableType (Type m) -> Type m -> Type m
substituteInType (forall k a. Ord k => [(k, a)] -> Map k a
M.fromList forall a b. (a -> b) -> a -> b
$ forall a b. [a] -> [b] -> [(a, b)]
zip [VariableType]
vars [Type m]
vars1) Type m
t

lookupTypeInEnvironment :: Show m => Variable -> Flow (InferenceContext m) (Type m)
lookupTypeInEnvironment :: forall m. Show m => Variable -> Flow (InferenceContext m) (Type m)
lookupTypeInEnvironment Variable
v = do
  (Context m
_, Int
_, TypingEnvironment m
env) <- forall s. Flow s s
getState
  case forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup Variable
v TypingEnvironment m
env of
    Maybe (TypeScheme m)
Nothing -> forall (m :: * -> *) a. MonadFail m => String -> m a
fail forall a b. (a -> b) -> a -> b
$ String
"unbound variable: " forall a. [a] -> [a] -> [a]
++ Variable -> String
unVariable Variable
v
    Just TypeScheme m
s  -> forall m. TypeScheme m -> Flow (InferenceContext m) (Type m)
instantiate TypeScheme m
s

namedType :: Show m => String -> Name -> GraphFlow m (Type m)
namedType :: forall m. Show m => String -> Name -> GraphFlow m (Type m)
namedType String
debug Name
name = do
  forall s a. String -> Flow s a -> Flow s a
withTrace (String
debug forall a. [a] -> [a] -> [a]
++ String
": " forall a. [a] -> [a] -> [a]
++ Name -> String
unName Name
name) forall a b. (a -> b) -> a -> b
$ do
    forall m a. GraphFlow m a -> GraphFlow m a
withSchemaContext forall a b. (a -> b) -> a -> b
$ do
      Element m
el <- forall m. Name -> GraphFlow m (Element m)
requireElement Name
name
      forall m. Show m => Term m -> GraphFlow m (Type m)
decodeStructuralType forall a b. (a -> b) -> a -> b
$ forall m. Element m -> Term m
elementData Element m
el

reduceType :: (Ord m, Show m) => Type m -> Type m
reduceType :: forall m. (Ord m, Show m) => Type m -> Type m
reduceType Type m
t = Type m
t -- betaReduceType cx t

rewriteDataType :: Ord m => (Type m -> Type m) -> Term (m, Type m, [Constraint m]) -> Term (m, Type m, [Constraint m])
rewriteDataType :: forall m.
Ord m =>
(Type m -> Type m)
-> Term (m, Type m, [Constraint m])
-> Term (m, Type m, [Constraint m])
rewriteDataType Type m -> Type m
f = forall b a. Ord b => (a -> b) -> Term a -> Term b
rewriteTermMeta forall {a} {c}. (a, Type m, c) -> (a, Type m, c)
rewrite
  where
    rewrite :: (a, Type m, c) -> (a, Type m, c)
rewrite (a
x, Type m
typ, c
c) = (a
x, Type m -> Type m
f Type m
typ, c
c)

startContext :: Context m -> InferenceContext m
startContext :: forall m. Context m -> InferenceContext m
startContext Context m
cx = (Context m
cx, Int
0, forall k a. Map k a
M.empty)

termConstraints :: Term (m, Type m, [Constraint m]) -> [Constraint m]
termConstraints :: forall m. Term (m, Type m, [Constraint m]) -> [Constraint m]
termConstraints (TermAnnotated (Annotated Term (m, Type m, [Constraint m])
_ (m
_, Type m
_, [Constraint m]
constraints))) = [Constraint m]
constraints

termType :: Term (m, Type m, [Constraint m]) -> Type m
termType :: forall m. Term (m, Type m, [Constraint m]) -> Type m
termType (TermAnnotated (Annotated Term (m, Type m, [Constraint m])
_ (m
_, Type m
typ, [Constraint m]
_))) = Type m
typ

typeOfElement :: Show m => Name -> GraphFlow m (Type m)
typeOfElement :: forall m. Show m => Name -> GraphFlow m (Type m)
typeOfElement Name
name = forall s a. String -> Flow s a -> Flow s a
withTrace String
"type of element" forall a b. (a -> b) -> a -> b
$ do
  Element m
el <- forall m. Name -> GraphFlow m (Element m)
requireElement Name
name
  forall m. Show m => Term m -> GraphFlow m (Type m)
decodeStructuralType forall a b. (a -> b) -> a -> b
$ forall m. Element m -> Term m
elementSchema Element m
el

typeOfPrimitiveFunction :: Name -> GraphFlow m (FunctionType m)
typeOfPrimitiveFunction :: forall m. Name -> GraphFlow m (FunctionType m)
typeOfPrimitiveFunction Name
name = forall m. PrimitiveFunction m -> FunctionType m
primitiveFunctionType forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall m. Name -> GraphFlow m (PrimitiveFunction m)
requirePrimitiveFunction Name
name

withEnvironment :: (TypingEnvironment m -> TypingEnvironment m) -> Flow (InferenceContext m) a -> Flow (InferenceContext m) a
withEnvironment :: forall m a.
(TypingEnvironment m -> TypingEnvironment m)
-> Flow (InferenceContext m) a -> Flow (InferenceContext m) a
withEnvironment TypingEnvironment m -> TypingEnvironment m
m Flow (InferenceContext m) a
f = do
  (Context m
cx, Int
i, TypingEnvironment m
e) <- forall s. Flow s s
getState
  forall s1 a s2. s1 -> Flow s1 a -> Flow s2 a
withState (Context m
cx, Int
i, TypingEnvironment m -> TypingEnvironment m
m TypingEnvironment m
e) Flow (InferenceContext m) a
f

withGraphContext :: GraphFlow m a -> Flow (InferenceContext m) a
withGraphContext :: forall m a. GraphFlow m a -> Flow (InferenceContext m) a
withGraphContext GraphFlow m a
f = do
  (Context m
cx, Int
_, TypingEnvironment m
_) <- forall s. Flow s s
getState
  forall s1 a s2. s1 -> Flow s1 a -> Flow s2 a
withState Context m
cx GraphFlow m a
f