{- | Type inference

Our type inference algorithm works in stages:

First, we __elaborate__ the AST and collect __constraints__.
Then, we solve these constraints and get back a __substitution__.
We go over the AST again, replacing the type variables we added in the elaboration stage
with concrete types.

The constraints of each group of definitions are solved separately and in order.

-}

{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE NamedFieldPuns #-}
{-# LANGUAGE ViewPatterns #-}

{-# options_ghc  -Wno-orphans #-}

module Language.Giml.Types.Infer where

import Control.Monad.State
import Control.Monad.Reader
import Control.Monad.Except

import Data.List (sort)
import qualified Data.Text as T
import qualified Data.Map as M
import qualified Data.Map.Merge.Strict as M
import qualified Data.Set as S
import qualified Data.Generics.Uniplate.Data as U

import Utils
import Language.Giml.Syntax.Ast
import Language.Giml.Builtins
import qualified Language.Giml.Syntax.Parser as Parser

-- for debugging purposes --
import Data.Text.Prettyprint.Doc (Pretty, Doc, pretty, (<+>), align)
import Language.Giml.Pretty (ppType, ppSourcePos, braced', render)
----------------------------
import Language.Giml.Logging

---------------
-- * Run

-- | Infer the types for all expressions in a source file
infer :: MonadBase b b => LogAction b LogMsg -> File InputAnn -> ExceptT TypeErrorA b (File Ann)
infer :: LogAction b LogMsg
-> File InputAnn -> ExceptT TypeErrorA b (File Ann)
infer LogAction b LogMsg
logact File InputAnn
file = do
  LogAction b LogMsg
-> ReaderT (CompileInfo b) (ExceptT TypeErrorA b) ()
-> ExceptT TypeErrorA b ()
forall (b :: * -> *) (m :: * -> *).
MonadBase b m =>
LogAction b LogMsg -> ReaderT (CompileInfo b) m () -> m ()
withLogAction LogAction b LogMsg
logact (ReaderT (CompileInfo b) (ExceptT TypeErrorA b) ()
 -> ExceptT TypeErrorA b ())
-> ReaderT (CompileInfo b) (ExceptT TypeErrorA b) ()
-> ExceptT TypeErrorA b ()
forall a b. (a -> b) -> a -> b
$ Stage
-> ReaderT (CompileInfo b) (ExceptT TypeErrorA b) ()
-> ReaderT (CompileInfo b) (ExceptT TypeErrorA b) ()
forall env (b :: * -> *) (m :: * -> *) a.
HasLog' LogMsg env b m =>
Stage -> m a -> m a
setStage Stage
TypeInference (ReaderT (CompileInfo b) (ExceptT TypeErrorA b) ()
 -> ReaderT (CompileInfo b) (ExceptT TypeErrorA b) ())
-> ReaderT (CompileInfo b) (ExceptT TypeErrorA b) ()
-> ReaderT (CompileInfo b) (ExceptT TypeErrorA b) ()
forall a b. (a -> b) -> a -> b
$
    Text -> ReaderT (CompileInfo b) (ExceptT TypeErrorA b) ()
forall env (b :: * -> *) (m :: * -> *).
HasLog' LogMsg env b m =>
Text -> m ()
logGeneral Text
"Type inference stage"

  (File Ann
elaborated, ElabState
s) <- LogAction b LogMsg
-> [Datatype ()]
-> Env Type
-> File InputAnn
-> ExceptT TypeErrorA b (File Ann, ElabState)
forall (b :: * -> *).
MonadBase b b =>
LogAction b LogMsg
-> [Datatype ()]
-> Env Type
-> File InputAnn
-> ExceptT TypeErrorA b (File Ann, ElabState)
elaborate LogAction b LogMsg
logact [Datatype ()]
builtinDatatypes ((Builtin -> Type) -> Map Text Builtin -> Env Type
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Builtin -> Type
bType Map Text Builtin
builtins) File InputAnn
file

  LogAction b LogMsg
-> ReaderT (CompileInfo b) (ExceptT TypeErrorA b) ()
-> ExceptT TypeErrorA b ()
forall (b :: * -> *) (m :: * -> *).
MonadBase b m =>
LogAction b LogMsg -> ReaderT (CompileInfo b) m () -> m ()
withLogAction LogAction b LogMsg
logact (ReaderT (CompileInfo b) (ExceptT TypeErrorA b) ()
 -> ExceptT TypeErrorA b ())
-> ReaderT (CompileInfo b) (ExceptT TypeErrorA b) ()
-> ExceptT TypeErrorA b ()
forall a b. (a -> b) -> a -> b
$ Stage
-> ReaderT (CompileInfo b) (ExceptT TypeErrorA b) ()
-> ReaderT (CompileInfo b) (ExceptT TypeErrorA b) ()
forall env (b :: * -> *) (m :: * -> *) a.
HasLog' LogMsg env b m =>
Stage -> m a -> m a
setStage Stage
TypeInference (ReaderT (CompileInfo b) (ExceptT TypeErrorA b) ()
 -> ReaderT (CompileInfo b) (ExceptT TypeErrorA b) ())
-> ReaderT (CompileInfo b) (ExceptT TypeErrorA b) ()
-> ReaderT (CompileInfo b) (ExceptT TypeErrorA b) ()
forall a b. (a -> b) -> a -> b
$
    Text -> ReaderT (CompileInfo b) (ExceptT TypeErrorA b) ()
forall env (b :: * -> *) (m :: * -> *).
HasLog' LogMsg env b m =>
Text -> m ()
logDetailed (Text
"elaborated: " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> File Ann -> Text
forall a. Show a => a -> Text
pShow File Ann
elaborated)
  LogAction b LogMsg
-> ReaderT (CompileInfo b) (ExceptT TypeErrorA b) ()
-> ExceptT TypeErrorA b ()
forall (b :: * -> *) (m :: * -> *).
MonadBase b m =>
LogAction b LogMsg -> ReaderT (CompileInfo b) m () -> m ()
withLogAction LogAction b LogMsg
logact (ReaderT (CompileInfo b) (ExceptT TypeErrorA b) ()
 -> ExceptT TypeErrorA b ())
-> ReaderT (CompileInfo b) (ExceptT TypeErrorA b) ()
-> ExceptT TypeErrorA b ()
forall a b. (a -> b) -> a -> b
$ Stage
-> ReaderT (CompileInfo b) (ExceptT TypeErrorA b) ()
-> ReaderT (CompileInfo b) (ExceptT TypeErrorA b) ()
forall env (b :: * -> *) (m :: * -> *) a.
HasLog' LogMsg env b m =>
Stage -> m a -> m a
setStage Stage
TypeInference (ReaderT (CompileInfo b) (ExceptT TypeErrorA b) ()
 -> ReaderT (CompileInfo b) (ExceptT TypeErrorA b) ())
-> ReaderT (CompileInfo b) (ExceptT TypeErrorA b) ()
-> ReaderT (CompileInfo b) (ExceptT TypeErrorA b) ()
forall a b. (a -> b) -> a -> b
$
    Text -> ReaderT (CompileInfo b) (ExceptT TypeErrorA b) ()
forall env (b :: * -> *) (m :: * -> *).
HasLog' LogMsg env b m =>
Text -> m ()
logDetailed (Text
"constraints: " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> [Set ConstraintA] -> Text
ppShowCAss (ElabState -> [Set ConstraintA]
esConstraints ElabState
s))

  (Map Text (InputAnn, Type)
sub, Int
_) <- ((Map Text (InputAnn, Type), Int)
 -> Set ConstraintA
 -> ExceptT TypeErrorA b (Map Text (InputAnn, Type), Int))
-> (Map Text (InputAnn, Type), Int)
-> [Set ConstraintA]
-> ExceptT TypeErrorA b (Map Text (InputAnn, Type), Int)
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM
    ( \(Map Text (InputAnn, Type)
acc, Int
seed) ->
      ( \(Map Text (InputAnn, Type)
sub, Int
seed') -> do
        LogAction b LogMsg
-> ReaderT (CompileInfo b) (ExceptT TypeErrorA b) ()
-> ExceptT TypeErrorA b ()
forall (b :: * -> *) (m :: * -> *).
MonadBase b m =>
LogAction b LogMsg -> ReaderT (CompileInfo b) m () -> m ()
withLogAction LogAction b LogMsg
logact (ReaderT (CompileInfo b) (ExceptT TypeErrorA b) ()
 -> ExceptT TypeErrorA b ())
-> ReaderT (CompileInfo b) (ExceptT TypeErrorA b) ()
-> ExceptT TypeErrorA b ()
forall a b. (a -> b) -> a -> b
$ Stage
-> ReaderT (CompileInfo b) (ExceptT TypeErrorA b) ()
-> ReaderT (CompileInfo b) (ExceptT TypeErrorA b) ()
forall env (b :: * -> *) (m :: * -> *) a.
HasLog' LogMsg env b m =>
Stage -> m a -> m a
setStage Stage
TypeInference (ReaderT (CompileInfo b) (ExceptT TypeErrorA b) ()
 -> ReaderT (CompileInfo b) (ExceptT TypeErrorA b) ())
-> ReaderT (CompileInfo b) (ExceptT TypeErrorA b) ()
-> ReaderT (CompileInfo b) (ExceptT TypeErrorA b) ()
forall a b. (a -> b) -> a -> b
$
          Text -> ReaderT (CompileInfo b) (ExceptT TypeErrorA b) ()
forall env (b :: * -> *) (m :: * -> *).
HasLog' LogMsg env b m =>
Text -> m ()
logDetailed (Text
"solved: " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Map Text (InputAnn, Type) -> Text
forall ann (f :: * -> *).
(Pretty ann, Functor f, Show (f Text)) =>
f ann -> Text
ppShow Map Text (InputAnn, Type)
sub)
        (Map Text (InputAnn, Type), Int)
-> ExceptT TypeErrorA b (Map Text (InputAnn, Type), Int)
forall (f :: * -> *) a. Applicative f => a -> f a
pure
          ( Map Text (InputAnn, Type)
-> Map Text (InputAnn, Type) -> Map Text (InputAnn, Type)
forall k a. Ord k => Map k a -> Map k a -> Map k a
M.union Map Text (InputAnn, Type)
acc Map Text (InputAnn, Type)
sub
          , Int
seed'
          )
      )
      ((Map Text (InputAnn, Type), Int)
 -> ExceptT TypeErrorA b (Map Text (InputAnn, Type), Int))
-> (Set ConstraintA
    -> ExceptT TypeErrorA b (Map Text (InputAnn, Type), Int))
-> Set ConstraintA
-> ExceptT TypeErrorA b (Map Text (InputAnn, Type), Int)
forall (m :: * -> *) b c a.
Monad m =>
(b -> m c) -> (a -> m b) -> a -> m c
<=< LogAction b LogMsg
-> Int
-> Set ConstraintA
-> ExceptT TypeErrorA b (Map Text (InputAnn, Type), Int)
forall (b :: * -> *).
MonadBase b b =>
LogAction b LogMsg
-> Int
-> Set ConstraintA
-> ExceptT TypeErrorA b (Map Text (InputAnn, Type), Int)
solve LogAction b LogMsg
logact Int
seed
      (Set ConstraintA
 -> ExceptT TypeErrorA b (Map Text (InputAnn, Type), Int))
-> ([ConstraintA] -> Set ConstraintA)
-> [ConstraintA]
-> ExceptT TypeErrorA b (Map Text (InputAnn, Type), Int)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [ConstraintA] -> Set ConstraintA
forall a. Ord a => [a] -> Set a
S.fromList
      ([ConstraintA]
 -> ExceptT TypeErrorA b (Map Text (InputAnn, Type), Int))
-> (Set ConstraintA -> ExceptT TypeErrorA b [ConstraintA])
-> Set ConstraintA
-> ExceptT TypeErrorA b (Map Text (InputAnn, Type), Int)
forall (m :: * -> *) b c a.
Monad m =>
(b -> m c) -> (a -> m b) -> a -> m c
<=< Map Text (InputAnn, Type)
-> [ConstraintA] -> ExceptT TypeErrorA b [ConstraintA]
forall (m :: * -> *).
Substitute m =>
Map Text (InputAnn, Type) -> [ConstraintA] -> m [ConstraintA]
substituteConstraints Map Text (InputAnn, Type)
acc ([ConstraintA] -> ExceptT TypeErrorA b [ConstraintA])
-> (Set ConstraintA -> [ConstraintA])
-> Set ConstraintA
-> ExceptT TypeErrorA b [ConstraintA]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Set ConstraintA -> [ConstraintA]
forall a. Set a -> [a]
S.toList
    )
    (Map Text (InputAnn, Type)
forall a. Monoid a => a
mempty, ElabState -> Int
esTypeVarCounter ElabState
s)
    (ElabState -> [Set ConstraintA]
esConstraints ElabState
s)
  Map Text (InputAnn, Type)
-> File Ann -> ExceptT TypeErrorA b (File Ann)
forall (m :: * -> *) f.
(Substitute m, Data f) =>
Map Text (InputAnn, Type) -> f -> m f
substitute Map Text (InputAnn, Type)
sub File Ann
elaborated

---------------
-- * Types

-- | The annotation of the input
type InputAnn = Parser.Ann

-- | The annotation of the output: the input + the type
data Ann
  = Ann
    { Ann -> InputAnn
annInput :: InputAnn
    , Ann -> Type
annType :: Type
    }
  deriving (Int -> Ann -> ShowS
[Ann] -> ShowS
Ann -> String
(Int -> Ann -> ShowS)
-> (Ann -> String) -> ([Ann] -> ShowS) -> Show Ann
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Ann] -> ShowS
$cshowList :: [Ann] -> ShowS
show :: Ann -> String
$cshow :: Ann -> String
showsPrec :: Int -> Ann -> ShowS
$cshowsPrec :: Int -> Ann -> ShowS
Show, Ann -> Ann -> Bool
(Ann -> Ann -> Bool) -> (Ann -> Ann -> Bool) -> Eq Ann
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Ann -> Ann -> Bool
$c/= :: Ann -> Ann -> Bool
== :: Ann -> Ann -> Bool
$c== :: Ann -> Ann -> Bool
Eq, Eq Ann
Eq Ann
-> (Ann -> Ann -> Ordering)
-> (Ann -> Ann -> Bool)
-> (Ann -> Ann -> Bool)
-> (Ann -> Ann -> Bool)
-> (Ann -> Ann -> Bool)
-> (Ann -> Ann -> Ann)
-> (Ann -> Ann -> Ann)
-> Ord Ann
Ann -> Ann -> Bool
Ann -> Ann -> Ordering
Ann -> Ann -> Ann
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: Ann -> Ann -> Ann
$cmin :: Ann -> Ann -> Ann
max :: Ann -> Ann -> Ann
$cmax :: Ann -> Ann -> Ann
>= :: Ann -> Ann -> Bool
$c>= :: Ann -> Ann -> Bool
> :: Ann -> Ann -> Bool
$c> :: Ann -> Ann -> Bool
<= :: Ann -> Ann -> Bool
$c<= :: Ann -> Ann -> Bool
< :: Ann -> Ann -> Bool
$c< :: Ann -> Ann -> Bool
compare :: Ann -> Ann -> Ordering
$ccompare :: Ann -> Ann -> Ordering
$cp1Ord :: Eq Ann
Ord, Typeable Ann
DataType
Constr
Typeable Ann
-> (forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> Ann -> c Ann)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c Ann)
-> (Ann -> Constr)
-> (Ann -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c Ann))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Ann))
-> ((forall b. Data b => b -> b) -> Ann -> Ann)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Ann -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Ann -> r)
-> (forall u. (forall d. Data d => d -> u) -> Ann -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> Ann -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> Ann -> m Ann)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> Ann -> m Ann)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> Ann -> m Ann)
-> Data Ann
Ann -> DataType
Ann -> Constr
(forall b. Data b => b -> b) -> Ann -> Ann
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Ann -> c Ann
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Ann
forall a.
Typeable a
-> (forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u. Int -> (forall d. Data d => d -> u) -> Ann -> u
forall u. (forall d. Data d => d -> u) -> Ann -> [u]
forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Ann -> r
forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Ann -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Ann -> m Ann
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Ann -> m Ann
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Ann
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Ann -> c Ann
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Ann)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Ann)
$cAnn :: Constr
$tAnn :: DataType
gmapMo :: (forall d. Data d => d -> m d) -> Ann -> m Ann
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Ann -> m Ann
gmapMp :: (forall d. Data d => d -> m d) -> Ann -> m Ann
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Ann -> m Ann
gmapM :: (forall d. Data d => d -> m d) -> Ann -> m Ann
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Ann -> m Ann
gmapQi :: Int -> (forall d. Data d => d -> u) -> Ann -> u
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> Ann -> u
gmapQ :: (forall d. Data d => d -> u) -> Ann -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> Ann -> [u]
gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Ann -> r
$cgmapQr :: forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Ann -> r
gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Ann -> r
$cgmapQl :: forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Ann -> r
gmapT :: (forall b. Data b => b -> b) -> Ann -> Ann
$cgmapT :: (forall b. Data b => b -> b) -> Ann -> Ann
dataCast2 :: (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Ann)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Ann)
dataCast1 :: (forall d. Data d => c (t d)) -> Maybe (c Ann)
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Ann)
dataTypeOf :: Ann -> DataType
$cdataTypeOf :: Ann -> DataType
toConstr :: Ann -> Constr
$ctoConstr :: Ann -> Constr
gunfold :: (forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Ann
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Ann
gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Ann -> c Ann
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Ann -> c Ann
$cp1Data :: Typeable Ann
Data)

type TypeErrorA = ([InputAnn], TypeError)

-- | The type of type errors.
data TypeError
  = TypeMismatch Type Type
  | UnboundVar Var
  | InfiniteType TypeVar Type
  | ArityMismatch Type Type
  | UnboundTypeVarsInType (Datatype InputAnn)
  | DuplicateTypeVarsInSig (Datatype InputAnn)
  | DuplicateConstrs (Datatype InputAnn)
  | DuplicateConstrs2 [(Constr, (VariantSig InputAnn, VariantSig InputAnn))]
  | NoSuchVariant Constr
  | RecordDiff Type Type [Label] [Label]
  | VariantDiff Type Type [Constr] [Constr]
  | NotARecord Type
  | NotAVariant Type
  | DuplicateVarsInPattern Pattern
  deriving (Int -> TypeError -> ShowS
[TypeError] -> ShowS
TypeError -> String
(Int -> TypeError -> ShowS)
-> (TypeError -> String)
-> ([TypeError] -> ShowS)
-> Show TypeError
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [TypeError] -> ShowS
$cshowList :: [TypeError] -> ShowS
show :: TypeError -> String
$cshow :: TypeError -> String
showsPrec :: Int -> TypeError -> ShowS
$cshowsPrec :: Int -> TypeError -> ShowS
Show, TypeError -> TypeError -> Bool
(TypeError -> TypeError -> Bool)
-> (TypeError -> TypeError -> Bool) -> Eq TypeError
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: TypeError -> TypeError -> Bool
$c/= :: TypeError -> TypeError -> Bool
== :: TypeError -> TypeError -> Bool
$c== :: TypeError -> TypeError -> Bool
Eq, Eq TypeError
Eq TypeError
-> (TypeError -> TypeError -> Ordering)
-> (TypeError -> TypeError -> Bool)
-> (TypeError -> TypeError -> Bool)
-> (TypeError -> TypeError -> Bool)
-> (TypeError -> TypeError -> Bool)
-> (TypeError -> TypeError -> TypeError)
-> (TypeError -> TypeError -> TypeError)
-> Ord TypeError
TypeError -> TypeError -> Bool
TypeError -> TypeError -> Ordering
TypeError -> TypeError -> TypeError
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: TypeError -> TypeError -> TypeError
$cmin :: TypeError -> TypeError -> TypeError
max :: TypeError -> TypeError -> TypeError
$cmax :: TypeError -> TypeError -> TypeError
>= :: TypeError -> TypeError -> Bool
$c>= :: TypeError -> TypeError -> Bool
> :: TypeError -> TypeError -> Bool
$c> :: TypeError -> TypeError -> Bool
<= :: TypeError -> TypeError -> Bool
$c<= :: TypeError -> TypeError -> Bool
< :: TypeError -> TypeError -> Bool
$c< :: TypeError -> TypeError -> Bool
compare :: TypeError -> TypeError -> Ordering
$ccompare :: TypeError -> TypeError -> Ordering
$cp1Ord :: Eq TypeError
Ord)

-- | Represents the constraints on types we collect during the elaboration phase.
data Constraint
  -- | The two type should be equal.
  = Equality Type Type
  -- | The first type is an instantiation of the second (see @instantiate@).
  | InstanceOf Type Type
  deriving (Int -> Constraint -> ShowS
[Constraint] -> ShowS
Constraint -> String
(Int -> Constraint -> ShowS)
-> (Constraint -> String)
-> ([Constraint] -> ShowS)
-> Show Constraint
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Constraint] -> ShowS
$cshowList :: [Constraint] -> ShowS
show :: Constraint -> String
$cshow :: Constraint -> String
showsPrec :: Int -> Constraint -> ShowS
$cshowsPrec :: Int -> Constraint -> ShowS
Show, Constraint -> Constraint -> Bool
(Constraint -> Constraint -> Bool)
-> (Constraint -> Constraint -> Bool) -> Eq Constraint
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Constraint -> Constraint -> Bool
$c/= :: Constraint -> Constraint -> Bool
== :: Constraint -> Constraint -> Bool
$c== :: Constraint -> Constraint -> Bool
Eq, Eq Constraint
Eq Constraint
-> (Constraint -> Constraint -> Ordering)
-> (Constraint -> Constraint -> Bool)
-> (Constraint -> Constraint -> Bool)
-> (Constraint -> Constraint -> Bool)
-> (Constraint -> Constraint -> Bool)
-> (Constraint -> Constraint -> Constraint)
-> (Constraint -> Constraint -> Constraint)
-> Ord Constraint
Constraint -> Constraint -> Bool
Constraint -> Constraint -> Ordering
Constraint -> Constraint -> Constraint
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: Constraint -> Constraint -> Constraint
$cmin :: Constraint -> Constraint -> Constraint
max :: Constraint -> Constraint -> Constraint
$cmax :: Constraint -> Constraint -> Constraint
>= :: Constraint -> Constraint -> Bool
$c>= :: Constraint -> Constraint -> Bool
> :: Constraint -> Constraint -> Bool
$c> :: Constraint -> Constraint -> Bool
<= :: Constraint -> Constraint -> Bool
$c<= :: Constraint -> Constraint -> Bool
< :: Constraint -> Constraint -> Bool
$c< :: Constraint -> Constraint -> Bool
compare :: Constraint -> Constraint -> Ordering
$ccompare :: Constraint -> Constraint -> Ordering
$cp1Ord :: Eq Constraint
Ord, Typeable Constraint
DataType
Constr
Typeable Constraint
-> (forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> Constraint -> c Constraint)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c Constraint)
-> (Constraint -> Constr)
-> (Constraint -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c Constraint))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e))
    -> Maybe (c Constraint))
-> ((forall b. Data b => b -> b) -> Constraint -> Constraint)
-> (forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> Constraint -> r)
-> (forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> Constraint -> r)
-> (forall u. (forall d. Data d => d -> u) -> Constraint -> [u])
-> (forall u.
    Int -> (forall d. Data d => d -> u) -> Constraint -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> Constraint -> m Constraint)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> Constraint -> m Constraint)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> Constraint -> m Constraint)
-> Data Constraint
Constraint -> DataType
Constraint -> Constr
(forall b. Data b => b -> b) -> Constraint -> Constraint
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Constraint -> c Constraint
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Constraint
forall a.
Typeable a
-> (forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u. Int -> (forall d. Data d => d -> u) -> Constraint -> u
forall u. (forall d. Data d => d -> u) -> Constraint -> [u]
forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> Constraint -> r
forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> Constraint -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Constraint -> m Constraint
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Constraint -> m Constraint
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Constraint
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Constraint -> c Constraint
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Constraint)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Constraint)
$cInstanceOf :: Constr
$cEquality :: Constr
$tConstraint :: DataType
gmapMo :: (forall d. Data d => d -> m d) -> Constraint -> m Constraint
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Constraint -> m Constraint
gmapMp :: (forall d. Data d => d -> m d) -> Constraint -> m Constraint
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Constraint -> m Constraint
gmapM :: (forall d. Data d => d -> m d) -> Constraint -> m Constraint
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Constraint -> m Constraint
gmapQi :: Int -> (forall d. Data d => d -> u) -> Constraint -> u
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> Constraint -> u
gmapQ :: (forall d. Data d => d -> u) -> Constraint -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> Constraint -> [u]
gmapQr :: (r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> Constraint -> r
$cgmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> Constraint -> r
gmapQl :: (r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> Constraint -> r
$cgmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> Constraint -> r
gmapT :: (forall b. Data b => b -> b) -> Constraint -> Constraint
$cgmapT :: (forall b. Data b => b -> b) -> Constraint -> Constraint
dataCast2 :: (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Constraint)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Constraint)
dataCast1 :: (forall d. Data d => c (t d)) -> Maybe (c Constraint)
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Constraint)
dataTypeOf :: Constraint -> DataType
$cdataTypeOf :: Constraint -> DataType
toConstr :: Constraint -> Constr
$ctoConstr :: Constraint -> Constr
gunfold :: (forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Constraint
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Constraint
gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Constraint -> c Constraint
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Constraint -> c Constraint
$cp1Data :: Typeable Constraint
Data)

-- | A constraint with the input annotation.
type ConstraintA = (Constraint, InputAnn)

-- | A @Set@ of constraints.
type Constraints = Set ConstraintA

-- | A mapping from type variable to types. Also contains the source position for error reporting.
--   This is the output of the constraint solving phase.
type Substitution
  = Map TypeVar (InputAnn, Type)

-- | Used during elaboration to represent the type of names in scope.
data Typer
  -- | This type is a monomorphic type so we can just use it.
  = Monomorphic Type
  -- | This type represents an polymorphic type that should be instantiate later.
  | Polymorphic TypeVar
  deriving (Int -> Typer -> ShowS
[Typer] -> ShowS
Typer -> String
(Int -> Typer -> ShowS)
-> (Typer -> String) -> ([Typer] -> ShowS) -> Show Typer
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Typer] -> ShowS
$cshowList :: [Typer] -> ShowS
show :: Typer -> String
$cshow :: Typer -> String
showsPrec :: Int -> Typer -> ShowS
$cshowsPrec :: Int -> Typer -> ShowS
Show, Typer -> Typer -> Bool
(Typer -> Typer -> Bool) -> (Typer -> Typer -> Bool) -> Eq Typer
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Typer -> Typer -> Bool
$c/= :: Typer -> Typer -> Bool
== :: Typer -> Typer -> Bool
$c== :: Typer -> Typer -> Bool
Eq, Eq Typer
Eq Typer
-> (Typer -> Typer -> Ordering)
-> (Typer -> Typer -> Bool)
-> (Typer -> Typer -> Bool)
-> (Typer -> Typer -> Bool)
-> (Typer -> Typer -> Bool)
-> (Typer -> Typer -> Typer)
-> (Typer -> Typer -> Typer)
-> Ord Typer
Typer -> Typer -> Bool
Typer -> Typer -> Ordering
Typer -> Typer -> Typer
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: Typer -> Typer -> Typer
$cmin :: Typer -> Typer -> Typer
max :: Typer -> Typer -> Typer
$cmax :: Typer -> Typer -> Typer
>= :: Typer -> Typer -> Bool
$c>= :: Typer -> Typer -> Bool
> :: Typer -> Typer -> Bool
$c> :: Typer -> Typer -> Bool
<= :: Typer -> Typer -> Bool
$c<= :: Typer -> Typer -> Bool
< :: Typer -> Typer -> Bool
$c< :: Typer -> Typer -> Bool
compare :: Typer -> Typer -> Ordering
$ccompare :: Typer -> Typer -> Ordering
$cp1Ord :: Eq Typer
Ord, Typeable Typer
DataType
Constr
Typeable Typer
-> (forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> Typer -> c Typer)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c Typer)
-> (Typer -> Constr)
-> (Typer -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c Typer))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Typer))
-> ((forall b. Data b => b -> b) -> Typer -> Typer)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Typer -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Typer -> r)
-> (forall u. (forall d. Data d => d -> u) -> Typer -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> Typer -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> Typer -> m Typer)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> Typer -> m Typer)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> Typer -> m Typer)
-> Data Typer
Typer -> DataType
Typer -> Constr
(forall b. Data b => b -> b) -> Typer -> Typer
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Typer -> c Typer
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Typer
forall a.
Typeable a
-> (forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u. Int -> (forall d. Data d => d -> u) -> Typer -> u
forall u. (forall d. Data d => d -> u) -> Typer -> [u]
forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Typer -> r
forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Typer -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Typer -> m Typer
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Typer -> m Typer
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Typer
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Typer -> c Typer
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Typer)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Typer)
$cPolymorphic :: Constr
$cMonomorphic :: Constr
$tTyper :: DataType
gmapMo :: (forall d. Data d => d -> m d) -> Typer -> m Typer
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Typer -> m Typer
gmapMp :: (forall d. Data d => d -> m d) -> Typer -> m Typer
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Typer -> m Typer
gmapM :: (forall d. Data d => d -> m d) -> Typer -> m Typer
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Typer -> m Typer
gmapQi :: Int -> (forall d. Data d => d -> u) -> Typer -> u
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> Typer -> u
gmapQ :: (forall d. Data d => d -> u) -> Typer -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> Typer -> [u]
gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Typer -> r
$cgmapQr :: forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Typer -> r
gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Typer -> r
$cgmapQl :: forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Typer -> r
gmapT :: (forall b. Data b => b -> b) -> Typer -> Typer
$cgmapT :: (forall b. Data b => b -> b) -> Typer -> Typer
dataCast2 :: (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Typer)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Typer)
dataCast1 :: (forall d. Data d => c (t d)) -> Maybe (c Typer)
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Typer)
dataTypeOf :: Typer -> DataType
$cdataTypeOf :: Typer -> DataType
toConstr :: Typer -> Constr
$ctoConstr :: Typer -> Constr
gunfold :: (forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Typer
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Typer
gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Typer -> c Typer
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Typer -> c Typer
$cp1Data :: Typeable Typer
Data)

------------------
-- * General Utils

-- | Throw an error with annotation.
throwErr :: MonadError TypeErrorA m => [InputAnn] -> TypeError -> m a
throwErr :: [InputAnn] -> TypeError -> m a
throwErr [InputAnn]
ann TypeError
err = TypeErrorA -> m a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError ([InputAnn]
ann, TypeError
err)

-- | Retrieve the type of an expression. Will explode when used on a non @EAnnotated@ node.
getType :: Expr Ann -> Type
getType :: Expr Ann -> Type
getType = Ann -> Type
annType (Ann -> Type) -> (Expr Ann -> Ann) -> Expr Ann -> Type
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Expr Ann -> Ann
forall a. Show a => Expr a -> a
getExprAnn

-----------------------------------------------
-- * Elaborate

{- |

During the elaboration phase we annotate the AST with the types
we know. When we don't know what the type of something is, we generate
a new type variable as a placeholder and mark that type with a @Constraint@
depending on its syntactic use.

- Input: AST
- Output: Annotated AST with types (to the best of our abilities) + constraints on those types

-}

elaborate :: MonadBase b b => LogAction b LogMsg -> [Datatype ()] -> Env Type -> File InputAnn -> ExceptT TypeErrorA b (File Ann, ElabState)
elaborate :: LogAction b LogMsg
-> [Datatype ()]
-> Env Type
-> File InputAnn
-> ExceptT TypeErrorA b (File Ann, ElabState)
elaborate = LogAction b LogMsg
-> [Datatype ()]
-> Env Type
-> File InputAnn
-> ExceptT TypeErrorA b (File Ann, ElabState)
forall (b :: * -> *).
(MonadBase b b, Functor b) =>
LogAction b LogMsg
-> [Datatype ()]
-> Env Type
-> File InputAnn
-> ExceptT TypeErrorA b (File Ann, ElabState)
runElaborate

------------
-- ** Types

-- | An environment from a name to something.
type Env a = Map Var a

-- | A mapping from a data constructor to the type that defines it and the type it holds.
type VariantEnv a
  = Map Constr (VariantSig a)

-- | Relevant information about a data constructor.
data VariantSig a
  = VariantSig
    { VariantSig a -> Type
vsDatatype :: Type
    , VariantSig a -> Maybe Type
vsPayloadTemplate :: Maybe Type
    , VariantSig a -> a
vsAnn :: a
    }
  deriving (Int -> VariantSig a -> ShowS
[VariantSig a] -> ShowS
VariantSig a -> String
(Int -> VariantSig a -> ShowS)
-> (VariantSig a -> String)
-> ([VariantSig a] -> ShowS)
-> Show (VariantSig a)
forall a. Show a => Int -> VariantSig a -> ShowS
forall a. Show a => [VariantSig a] -> ShowS
forall a. Show a => VariantSig a -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [VariantSig a] -> ShowS
$cshowList :: forall a. Show a => [VariantSig a] -> ShowS
show :: VariantSig a -> String
$cshow :: forall a. Show a => VariantSig a -> String
showsPrec :: Int -> VariantSig a -> ShowS
$cshowsPrec :: forall a. Show a => Int -> VariantSig a -> ShowS
Show, VariantSig a -> VariantSig a -> Bool
(VariantSig a -> VariantSig a -> Bool)
-> (VariantSig a -> VariantSig a -> Bool) -> Eq (VariantSig a)
forall a. Eq a => VariantSig a -> VariantSig a -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: VariantSig a -> VariantSig a -> Bool
$c/= :: forall a. Eq a => VariantSig a -> VariantSig a -> Bool
== :: VariantSig a -> VariantSig a -> Bool
$c== :: forall a. Eq a => VariantSig a -> VariantSig a -> Bool
Eq, Eq (VariantSig a)
Eq (VariantSig a)
-> (VariantSig a -> VariantSig a -> Ordering)
-> (VariantSig a -> VariantSig a -> Bool)
-> (VariantSig a -> VariantSig a -> Bool)
-> (VariantSig a -> VariantSig a -> Bool)
-> (VariantSig a -> VariantSig a -> Bool)
-> (VariantSig a -> VariantSig a -> VariantSig a)
-> (VariantSig a -> VariantSig a -> VariantSig a)
-> Ord (VariantSig a)
VariantSig a -> VariantSig a -> Bool
VariantSig a -> VariantSig a -> Ordering
VariantSig a -> VariantSig a -> VariantSig a
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
forall a. Ord a => Eq (VariantSig a)
forall a. Ord a => VariantSig a -> VariantSig a -> Bool
forall a. Ord a => VariantSig a -> VariantSig a -> Ordering
forall a. Ord a => VariantSig a -> VariantSig a -> VariantSig a
min :: VariantSig a -> VariantSig a -> VariantSig a
$cmin :: forall a. Ord a => VariantSig a -> VariantSig a -> VariantSig a
max :: VariantSig a -> VariantSig a -> VariantSig a
$cmax :: forall a. Ord a => VariantSig a -> VariantSig a -> VariantSig a
>= :: VariantSig a -> VariantSig a -> Bool
$c>= :: forall a. Ord a => VariantSig a -> VariantSig a -> Bool
> :: VariantSig a -> VariantSig a -> Bool
$c> :: forall a. Ord a => VariantSig a -> VariantSig a -> Bool
<= :: VariantSig a -> VariantSig a -> Bool
$c<= :: forall a. Ord a => VariantSig a -> VariantSig a -> Bool
< :: VariantSig a -> VariantSig a -> Bool
$c< :: forall a. Ord a => VariantSig a -> VariantSig a -> Bool
compare :: VariantSig a -> VariantSig a -> Ordering
$ccompare :: forall a. Ord a => VariantSig a -> VariantSig a -> Ordering
$cp1Ord :: forall a. Ord a => Eq (VariantSig a)
Ord, Typeable (VariantSig a)
DataType
Constr
Typeable (VariantSig a)
-> (forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> VariantSig a -> c (VariantSig a))
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c (VariantSig a))
-> (VariantSig a -> Constr)
-> (VariantSig a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c (VariantSig a)))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e))
    -> Maybe (c (VariantSig a)))
-> ((forall b. Data b => b -> b) -> VariantSig a -> VariantSig a)
-> (forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> VariantSig a -> r)
-> (forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> VariantSig a -> r)
-> (forall u. (forall d. Data d => d -> u) -> VariantSig a -> [u])
-> (forall u.
    Int -> (forall d. Data d => d -> u) -> VariantSig a -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> VariantSig a -> m (VariantSig a))
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> VariantSig a -> m (VariantSig a))
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> VariantSig a -> m (VariantSig a))
-> Data (VariantSig a)
VariantSig a -> DataType
VariantSig a -> Constr
(forall d. Data d => c (t d)) -> Maybe (c (VariantSig a))
(forall b. Data b => b -> b) -> VariantSig a -> VariantSig a
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> VariantSig a -> c (VariantSig a)
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (VariantSig a)
forall a. Data a => Typeable (VariantSig a)
forall a. Data a => VariantSig a -> DataType
forall a. Data a => VariantSig a -> Constr
forall a.
Data a =>
(forall b. Data b => b -> b) -> VariantSig a -> VariantSig a
forall a u.
Data a =>
Int -> (forall d. Data d => d -> u) -> VariantSig a -> u
forall a u.
Data a =>
(forall d. Data d => d -> u) -> VariantSig a -> [u]
forall a r r'.
Data a =>
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> VariantSig a -> r
forall a r r'.
Data a =>
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> VariantSig a -> r
forall a (m :: * -> *).
(Data a, Monad m) =>
(forall d. Data d => d -> m d) -> VariantSig a -> m (VariantSig a)
forall a (m :: * -> *).
(Data a, MonadPlus m) =>
(forall d. Data d => d -> m d) -> VariantSig a -> m (VariantSig a)
forall a (c :: * -> *).
Data a =>
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (VariantSig a)
forall a (c :: * -> *).
Data a =>
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> VariantSig a -> c (VariantSig a)
forall a (t :: * -> *) (c :: * -> *).
(Data a, Typeable t) =>
(forall d. Data d => c (t d)) -> Maybe (c (VariantSig a))
forall a (t :: * -> * -> *) (c :: * -> *).
(Data a, Typeable t) =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c (VariantSig a))
forall a.
Typeable a
-> (forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u. Int -> (forall d. Data d => d -> u) -> VariantSig a -> u
forall u. (forall d. Data d => d -> u) -> VariantSig a -> [u]
forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> VariantSig a -> r
forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> VariantSig a -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> VariantSig a -> m (VariantSig a)
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> VariantSig a -> m (VariantSig a)
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (VariantSig a)
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> VariantSig a -> c (VariantSig a)
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c (VariantSig a))
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c (VariantSig a))
$cVariantSig :: Constr
$tVariantSig :: DataType
gmapMo :: (forall d. Data d => d -> m d) -> VariantSig a -> m (VariantSig a)
$cgmapMo :: forall a (m :: * -> *).
(Data a, MonadPlus m) =>
(forall d. Data d => d -> m d) -> VariantSig a -> m (VariantSig a)
gmapMp :: (forall d. Data d => d -> m d) -> VariantSig a -> m (VariantSig a)
$cgmapMp :: forall a (m :: * -> *).
(Data a, MonadPlus m) =>
(forall d. Data d => d -> m d) -> VariantSig a -> m (VariantSig a)
gmapM :: (forall d. Data d => d -> m d) -> VariantSig a -> m (VariantSig a)
$cgmapM :: forall a (m :: * -> *).
(Data a, Monad m) =>
(forall d. Data d => d -> m d) -> VariantSig a -> m (VariantSig a)
gmapQi :: Int -> (forall d. Data d => d -> u) -> VariantSig a -> u
$cgmapQi :: forall a u.
Data a =>
Int -> (forall d. Data d => d -> u) -> VariantSig a -> u
gmapQ :: (forall d. Data d => d -> u) -> VariantSig a -> [u]
$cgmapQ :: forall a u.
Data a =>
(forall d. Data d => d -> u) -> VariantSig a -> [u]
gmapQr :: (r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> VariantSig a -> r
$cgmapQr :: forall a r r'.
Data a =>
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> VariantSig a -> r
gmapQl :: (r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> VariantSig a -> r
$cgmapQl :: forall a r r'.
Data a =>
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> VariantSig a -> r
gmapT :: (forall b. Data b => b -> b) -> VariantSig a -> VariantSig a
$cgmapT :: forall a.
Data a =>
(forall b. Data b => b -> b) -> VariantSig a -> VariantSig a
dataCast2 :: (forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c (VariantSig a))
$cdataCast2 :: forall a (t :: * -> * -> *) (c :: * -> *).
(Data a, Typeable t) =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c (VariantSig a))
dataCast1 :: (forall d. Data d => c (t d)) -> Maybe (c (VariantSig a))
$cdataCast1 :: forall a (t :: * -> *) (c :: * -> *).
(Data a, Typeable t) =>
(forall d. Data d => c (t d)) -> Maybe (c (VariantSig a))
dataTypeOf :: VariantSig a -> DataType
$cdataTypeOf :: forall a. Data a => VariantSig a -> DataType
toConstr :: VariantSig a -> Constr
$ctoConstr :: forall a. Data a => VariantSig a -> Constr
gunfold :: (forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (VariantSig a)
$cgunfold :: forall a (c :: * -> *).
Data a =>
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (VariantSig a)
gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> VariantSig a -> c (VariantSig a)
$cgfoldl :: forall a (c :: * -> *).
Data a =>
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> VariantSig a -> c (VariantSig a)
$cp1Data :: forall a. Data a => Typeable (VariantSig a)
Data)

-- | The state we keep during elaboration.
data ElabState
  = ElabState
    { ElabState -> Int
esTypeVarCounter :: Int
    -- ^ Used to generate unique type variable names.
    , ElabState -> [Set ConstraintA]
esConstraints :: [Constraints]
    -- ^ The constraints we collect.
    , ElabState -> VariantEnv InputAnn
esVariantEnv :: VariantEnv InputAnn
    -- ^ Mapping from a data constructor name to the data type
    --   and variant type signature.
    }

-- | The environment we use.
data ElabEnv b
  = ElabEnv
    { ElabEnv b -> Env Typer
eeTypeEnv :: Env Typer
    -- ^ Represents the variables in scope and their types (including if they are let-polymorphic or not).
    , ElabEnv b -> Env Type
eeBuiltins :: Env Type
    , ElabEnv b -> LogAction b LogMsg
logAction :: LogAction b LogMsg
    }
  deriving (forall x. ElabEnv b -> Rep (ElabEnv b) x)
-> (forall x. Rep (ElabEnv b) x -> ElabEnv b)
-> Generic (ElabEnv b)
forall x. Rep (ElabEnv b) x -> ElabEnv b
forall x. ElabEnv b -> Rep (ElabEnv b) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall (b :: * -> *) x. Rep (ElabEnv b) x -> ElabEnv b
forall (b :: * -> *) x. ElabEnv b -> Rep (ElabEnv b) x
$cto :: forall (b :: * -> *) x. Rep (ElabEnv b) x -> ElabEnv b
$cfrom :: forall (b :: * -> *) x. ElabEnv b -> Rep (ElabEnv b) x
Generic

-- | The monadic capabilities for the elaboration phase.
type Elaborate b m
  = ( MonadBase b m
    , MonadState ElabState m
    , MonadReader (ElabEnv b) m
    , MonadError TypeErrorA m
    )

-- | Return type for some elaboration functions.
data ElabInfo a
  = ElabInfo
    { ElabInfo a -> a
eiResult :: a
      -- ^ The result of the current elaboration
    , ElabInfo a -> Type
eiType :: Type
      -- ^ The type of the result
    , ElabInfo a -> Env Typer
eiNewEnv :: Env Typer
      -- ^ A definition to add to the environment for the next statements, if needed.
    }

-------------
-- ** Utils

-- | Try to find the type of a variable in scope.
lookupVarMaybe :: Elaborate b m => Var -> m (Maybe Typer)
lookupVarMaybe :: Text -> m (Maybe Typer)
lookupVarMaybe Text
var = do
  Env Typer
env <- (ElabEnv b -> Env Typer) -> m (Env Typer)
forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks ElabEnv b -> Env Typer
forall (b :: * -> *). ElabEnv b -> Env Typer
eeTypeEnv
  Maybe Typer -> m (Maybe Typer)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Text -> Env Typer -> Maybe Typer
forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup Text
var Env Typer
env)

-- | Same as @lookupVarMaybe@ but throws an @UnboundVar@ error on failure.
lookupVar :: Elaborate b m => InputAnn -> Var -> m Typer
lookupVar :: InputAnn -> Text -> m Typer
lookupVar InputAnn
ann Text
var = do
  Env Typer
env <- (ElabEnv b -> Env Typer) -> m (Env Typer)
forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks ElabEnv b -> Env Typer
forall (b :: * -> *). ElabEnv b -> Env Typer
eeTypeEnv
  m Typer -> (Typer -> m Typer) -> Maybe Typer -> m Typer
forall b a. b -> (a -> b) -> Maybe a -> b
maybe
    ([InputAnn] -> TypeError -> m Typer
forall (m :: * -> *) a.
MonadError TypeErrorA m =>
[InputAnn] -> TypeError -> m a
throwErr [InputAnn
ann] (TypeError -> m Typer) -> TypeError -> m Typer
forall a b. (a -> b) -> a -> b
$ Text -> TypeError
UnboundVar Text
var)
    Typer -> m Typer
forall (f :: * -> *) a. Applicative f => a -> f a
pure
    (Text -> Env Typer -> Maybe Typer
forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup Text
var Env Typer
env)

-- | Look for a builtin value/function. Throws an @UnboundVar@ error on failure.
lookupBuiltin :: Elaborate b m => InputAnn -> Var -> m Type
lookupBuiltin :: InputAnn -> Text -> m Type
lookupBuiltin InputAnn
ann Text
var = do
  Env Type
env <- (ElabEnv b -> Env Type) -> m (Env Type)
forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks ElabEnv b -> Env Type
forall (b :: * -> *). ElabEnv b -> Env Type
eeBuiltins
  m Type -> (Type -> m Type) -> Maybe Type -> m Type
forall b a. b -> (a -> b) -> Maybe a -> b
maybe
    ([InputAnn] -> TypeError -> m Type
forall (m :: * -> *) a.
MonadError TypeErrorA m =>
[InputAnn] -> TypeError -> m a
throwErr [InputAnn
ann] (TypeError -> m Type) -> TypeError -> m Type
forall a b. (a -> b) -> a -> b
$ Text -> TypeError
UnboundVar Text
var)
    Type -> m Type
forall (f :: * -> *) a. Applicative f => a -> f a
pure
    (Text -> Env Type -> Maybe Type
forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup Text
var Env Type
env)

-- | Adding new variable into the scope
insertToEnv :: Env Typer -> ElabEnv b -> ElabEnv b
insertToEnv :: Env Typer -> ElabEnv b -> ElabEnv b
insertToEnv Env Typer
vars ElabEnv b
elabEnv =
  ElabEnv b
elabEnv
    { eeTypeEnv :: Env Typer
eeTypeEnv = Env Typer -> Env Typer -> Env Typer
forall k a. Ord k => Map k a -> Map k a -> Map k a
M.union Env Typer
vars (ElabEnv b -> Env Typer
forall (b :: * -> *). ElabEnv b -> Env Typer
eeTypeEnv ElabEnv b
elabEnv)
    }

-- | Remove variables from the scope
removeFromEnv :: [Var] -> ElabEnv b -> ElabEnv b
removeFromEnv :: [Text] -> ElabEnv b -> ElabEnv b
removeFromEnv [Text]
vars ElabEnv b
elabEnv =
  ElabEnv b
elabEnv
    { eeTypeEnv :: Env Typer
eeTypeEnv = (Text -> Env Typer -> Env Typer)
-> Env Typer -> [Text] -> Env Typer
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr Text -> Env Typer -> Env Typer
forall k a. Ord k => k -> Map k a -> Map k a
M.delete (ElabEnv b -> Env Typer
forall (b :: * -> *). ElabEnv b -> Env Typer
eeTypeEnv ElabEnv b
elabEnv) [Text]
vars
    }

-- | Run an elaboration function with extra variables in scope.
withEnv :: Elaborate b m => [(Var, Typer)] -> m a -> m a
withEnv :: [(Text, Typer)] -> m a -> m a
withEnv = (ElabEnv b -> ElabEnv b) -> m a -> m a
forall r (m :: * -> *) a. MonadReader r m => (r -> r) -> m a -> m a
local ((ElabEnv b -> ElabEnv b) -> m a -> m a)
-> ([(Text, Typer)] -> ElabEnv b -> ElabEnv b)
-> [(Text, Typer)]
-> m a
-> m a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Env Typer -> ElabEnv b -> ElabEnv b
forall (b :: * -> *). Env Typer -> ElabEnv b -> ElabEnv b
insertToEnv (Env Typer -> ElabEnv b -> ElabEnv b)
-> ([(Text, Typer)] -> Env Typer)
-> [(Text, Typer)]
-> ElabEnv b
-> ElabEnv b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [(Text, Typer)] -> Env Typer
forall k a. Ord k => [(k, a)] -> Map k a
M.fromList

-- | Run an elaboration function with extra variables in scope (Map version).
withEnv' :: Elaborate b m => Env Typer -> m a -> m a
withEnv' :: Env Typer -> m a -> m a
withEnv' = (ElabEnv b -> ElabEnv b) -> m a -> m a
forall r (m :: * -> *) a. MonadReader r m => (r -> r) -> m a -> m a
local ((ElabEnv b -> ElabEnv b) -> m a -> m a)
-> (Env Typer -> ElabEnv b -> ElabEnv b) -> Env Typer -> m a -> m a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Env Typer -> ElabEnv b -> ElabEnv b
forall (b :: * -> *). Env Typer -> ElabEnv b -> ElabEnv b
insertToEnv

-- | Run an elaboration function without some variables in scope.
withoutEnv :: Elaborate b m => [Var] -> m a -> m a
withoutEnv :: [Text] -> m a -> m a
withoutEnv = (ElabEnv b -> ElabEnv b) -> m a -> m a
forall r (m :: * -> *) a. MonadReader r m => (r -> r) -> m a -> m a
local ((ElabEnv b -> ElabEnv b) -> m a -> m a)
-> ([Text] -> ElabEnv b -> ElabEnv b) -> [Text] -> m a -> m a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Text] -> ElabEnv b -> ElabEnv b
forall (b :: * -> *). [Text] -> ElabEnv b -> ElabEnv b
removeFromEnv

-- | Lookup variant in env
lookupVariant :: Elaborate b m => InputAnn -> Constr -> m (VariantSig InputAnn)
lookupVariant :: InputAnn -> Text -> m (VariantSig InputAnn)
lookupVariant InputAnn
ann Text
constr = do
  m (VariantSig InputAnn)
-> (VariantSig InputAnn -> m (VariantSig InputAnn))
-> Maybe (VariantSig InputAnn)
-> m (VariantSig InputAnn)
forall b a. b -> (a -> b) -> Maybe a -> b
maybe ([InputAnn] -> TypeError -> m (VariantSig InputAnn)
forall (m :: * -> *) a.
MonadError TypeErrorA m =>
[InputAnn] -> TypeError -> m a
throwErr [InputAnn
ann] (TypeError -> m (VariantSig InputAnn))
-> TypeError -> m (VariantSig InputAnn)
forall a b. (a -> b) -> a -> b
$ Text -> TypeError
NoSuchVariant Text
constr) VariantSig InputAnn -> m (VariantSig InputAnn)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Maybe (VariantSig InputAnn) -> m (VariantSig InputAnn))
-> (ElabState -> Maybe (VariantSig InputAnn))
-> ElabState
-> m (VariantSig InputAnn)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Text -> VariantEnv InputAnn -> Maybe (VariantSig InputAnn)
forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup Text
constr (VariantEnv InputAnn -> Maybe (VariantSig InputAnn))
-> (ElabState -> VariantEnv InputAnn)
-> ElabState
-> Maybe (VariantSig InputAnn)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ElabState -> VariantEnv InputAnn
esVariantEnv (ElabState -> m (VariantSig InputAnn))
-> m ElabState -> m (VariantSig InputAnn)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< m ElabState
forall s (m :: * -> *). MonadState s m => m s
get

-- | Add a datatype information into the environment
addVariantSigs :: Elaborate b m => VariantEnv InputAnn -> m ()
addVariantSigs :: VariantEnv InputAnn -> m ()
addVariantSigs VariantEnv InputAnn
venv = do
  ElabState
s <- m ElabState
forall s (m :: * -> *). MonadState s m => m s
get
  let
    env :: VariantEnv InputAnn
env = ElabState -> VariantEnv InputAnn
esVariantEnv ElabState
s
    duplicates :: [(Text, (VariantSig InputAnn, VariantSig InputAnn))]
duplicates = Map Text (VariantSig InputAnn, VariantSig InputAnn)
-> [(Text, (VariantSig InputAnn, VariantSig InputAnn))]
forall k a. Map k a -> [(k, a)]
M.toList (Map Text (VariantSig InputAnn, VariantSig InputAnn)
 -> [(Text, (VariantSig InputAnn, VariantSig InputAnn))])
-> Map Text (VariantSig InputAnn, VariantSig InputAnn)
-> [(Text, (VariantSig InputAnn, VariantSig InputAnn))]
forall a b. (a -> b) -> a -> b
$ (VariantSig InputAnn
 -> VariantSig InputAnn
 -> (VariantSig InputAnn, VariantSig InputAnn))
-> VariantEnv InputAnn
-> VariantEnv InputAnn
-> Map Text (VariantSig InputAnn, VariantSig InputAnn)
forall k a b c.
Ord k =>
(a -> b -> c) -> Map k a -> Map k b -> Map k c
M.intersectionWith (,) VariantEnv InputAnn
venv VariantEnv InputAnn
env

  -- check for duplicate variants
  case [(Text, (VariantSig InputAnn, VariantSig InputAnn))]
duplicates of
    [] -> () -> m ()
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
    (Text
d, (VariantSig InputAnn, VariantSig InputAnn)
v) : [(Text, (VariantSig InputAnn, VariantSig InputAnn))]
rest -> do
      [InputAnn] -> TypeError -> m ()
forall (m :: * -> *) a.
MonadError TypeErrorA m =>
[InputAnn] -> TypeError -> m a
throwErr [VariantSig InputAnn -> InputAnn
forall a. VariantSig a -> a
vsAnn (VariantSig InputAnn -> InputAnn)
-> VariantSig InputAnn -> InputAnn
forall a b. (a -> b) -> a -> b
$ (VariantSig InputAnn, VariantSig InputAnn) -> VariantSig InputAnn
forall a b. (a, b) -> a
fst (VariantSig InputAnn, VariantSig InputAnn)
v] (TypeError -> m ()) -> TypeError -> m ()
forall a b. (a -> b) -> a -> b
$ [(Text, (VariantSig InputAnn, VariantSig InputAnn))] -> TypeError
DuplicateConstrs2 ((Text
d,(VariantSig InputAnn, VariantSig InputAnn)
v ) (Text, (VariantSig InputAnn, VariantSig InputAnn))
-> [(Text, (VariantSig InputAnn, VariantSig InputAnn))]
-> [(Text, (VariantSig InputAnn, VariantSig InputAnn))]
forall a. a -> [a] -> [a]
: [(Text, (VariantSig InputAnn, VariantSig InputAnn))]
rest)

  ElabState -> m ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put (ElabState -> m ()) -> ElabState -> m ()
forall a b. (a -> b) -> a -> b
$ ElabState
s { esVariantEnv :: VariantEnv InputAnn
esVariantEnv = VariantEnv InputAnn
env VariantEnv InputAnn -> VariantEnv InputAnn -> VariantEnv InputAnn
forall k a. Ord k => Map k a -> Map k a -> Map k a
`M.union` VariantEnv InputAnn
venv }

-- | Generate a new type variable.
genTypeVar :: MonadState ElabState m => Text -> m TypeVar
genTypeVar :: Text -> m Text
genTypeVar Text
prefix = do
  Int
n <- ElabState -> Int
esTypeVarCounter (ElabState -> Int) -> m ElabState -> m Int
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m ElabState
forall s (m :: * -> *). MonadState s m => m s
get
  (ElabState -> ElabState) -> m ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify ((ElabState -> ElabState) -> m ())
-> (ElabState -> ElabState) -> m ()
forall a b. (a -> b) -> a -> b
$ \ElabState
s -> ElabState
s { esTypeVarCounter :: Int
esTypeVarCounter = Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1 }
  Text -> m Text
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Text -> m Text) -> Text -> m Text
forall a b. (a -> b) -> a -> b
$ Text
prefix Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> String -> Text
toText (Int -> String
forall a. Show a => a -> String
show Int
n)

-- | Add a new constraint.
constrain :: Elaborate b m => InputAnn -> Constraint -> m ()
constrain :: InputAnn -> Constraint -> m ()
constrain InputAnn
ann Constraint
constraint =
  (ElabState -> ElabState) -> m ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify ((ElabState -> ElabState) -> m ())
-> (ElabState -> ElabState) -> m ()
forall a b. (a -> b) -> a -> b
$ \ElabState
s -> ElabState
s
    { esConstraints :: [Set ConstraintA]
esConstraints =
      case (ElabState -> [Set ConstraintA]
esConstraints ElabState
s) of
        [] -> String -> [Set ConstraintA]
forall a. HasCallStack => String -> a
error String
"Current constraints group is missing."
        Set ConstraintA
current : [Set ConstraintA]
rest ->
          ConstraintA -> Set ConstraintA -> Set ConstraintA
forall a. Ord a => a -> Set a -> Set a
S.insert (Constraint
constraint, InputAnn
ann) Set ConstraintA
current Set ConstraintA -> [Set ConstraintA] -> [Set ConstraintA]
forall a. a -> [a] -> [a]
: [Set ConstraintA]
rest
    }

newConstraintsGroup :: Elaborate b m => m ()
newConstraintsGroup :: m ()
newConstraintsGroup = do
  (ElabState -> ElabState) -> m ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify ((ElabState -> ElabState) -> m ())
-> (ElabState -> ElabState) -> m ()
forall a b. (a -> b) -> a -> b
$ \ElabState
s -> ElabState
s { esConstraints :: [Set ConstraintA]
esConstraints = Set ConstraintA
forall a. Set a
S.empty Set ConstraintA -> [Set ConstraintA] -> [Set ConstraintA]
forall a. a -> [a] -> [a]
: (ElabState -> [Set ConstraintA]
esConstraints ElabState
s) }

------------------
-- ** Algorithm

-- | Run the algorithm.
runElaborate :: MonadBase b b => Functor b => LogAction b LogMsg -> [Datatype ()] -> Env Type -> File InputAnn -> ExceptT TypeErrorA b (File Ann, ElabState)
runElaborate :: LogAction b LogMsg
-> [Datatype ()]
-> Env Type
-> File InputAnn
-> ExceptT TypeErrorA b (File Ann, ElabState)
runElaborate LogAction b LogMsg
logact [Datatype ()]
builtinDats Env Type
builtinsTypes =
  ( ((File Ann, ElabState) -> (File Ann, ElabState))
-> ExceptT TypeErrorA b (File Ann, ElabState)
-> ExceptT TypeErrorA b (File Ann, ElabState)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((ElabState -> ElabState)
-> (File Ann, ElabState) -> (File Ann, ElabState)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\ElabState
s -> ElabState
s { esConstraints :: [Set ConstraintA]
esConstraints = [Set ConstraintA] -> [Set ConstraintA]
forall a. [a] -> [a]
reverse (ElabState -> [Set ConstraintA]
esConstraints ElabState
s) }))
  (ExceptT TypeErrorA b (File Ann, ElabState)
 -> ExceptT TypeErrorA b (File Ann, ElabState))
-> (File InputAnn -> ExceptT TypeErrorA b (File Ann, ElabState))
-> File InputAnn
-> ExceptT TypeErrorA b (File Ann, ElabState)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (StateT ElabState (ExceptT TypeErrorA b) (File Ann)
 -> ElabState -> ExceptT TypeErrorA b (File Ann, ElabState))
-> ElabState
-> StateT ElabState (ExceptT TypeErrorA b) (File Ann)
-> ExceptT TypeErrorA b (File Ann, ElabState)
forall a b c. (a -> b -> c) -> b -> a -> c
flip StateT ElabState (ExceptT TypeErrorA b) (File Ann)
-> ElabState -> ExceptT TypeErrorA b (File Ann, ElabState)
forall s (m :: * -> *) a. StateT s m a -> s -> m (a, s)
runStateT (Int -> [Set ConstraintA] -> VariantEnv InputAnn -> ElabState
ElabState Int
0 [Set ConstraintA]
forall a. Monoid a => a
mempty VariantEnv InputAnn
forall a. Monoid a => a
mempty)
  (StateT ElabState (ExceptT TypeErrorA b) (File Ann)
 -> ExceptT TypeErrorA b (File Ann, ElabState))
-> (File InputAnn
    -> StateT ElabState (ExceptT TypeErrorA b) (File Ann))
-> File InputAnn
-> ExceptT TypeErrorA b (File Ann, ElabState)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (ReaderT
   (ElabEnv b) (StateT ElabState (ExceptT TypeErrorA b)) (File Ann)
 -> ElabEnv b -> StateT ElabState (ExceptT TypeErrorA b) (File Ann))
-> ElabEnv b
-> ReaderT
     (ElabEnv b) (StateT ElabState (ExceptT TypeErrorA b)) (File Ann)
-> StateT ElabState (ExceptT TypeErrorA b) (File Ann)
forall a b c. (a -> b -> c) -> b -> a -> c
flip ReaderT
  (ElabEnv b) (StateT ElabState (ExceptT TypeErrorA b)) (File Ann)
-> ElabEnv b -> StateT ElabState (ExceptT TypeErrorA b) (File Ann)
forall r (m :: * -> *) a. ReaderT r m a -> r -> m a
runReaderT (Env Typer -> Env Type -> LogAction b LogMsg -> ElabEnv b
forall (b :: * -> *).
Env Typer -> Env Type -> LogAction b LogMsg -> ElabEnv b
ElabEnv Env Typer
forall a. Monoid a => a
mempty Env Type
builtinsTypes LogAction b LogMsg
logact)
  (ReaderT
   (ElabEnv b) (StateT ElabState (ExceptT TypeErrorA b)) (File Ann)
 -> StateT ElabState (ExceptT TypeErrorA b) (File Ann))
-> (File InputAnn
    -> ReaderT
         (ElabEnv b) (StateT ElabState (ExceptT TypeErrorA b)) (File Ann))
-> File InputAnn
-> StateT ElabState (ExceptT TypeErrorA b) (File Ann)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Stage
-> ReaderT
     (ElabEnv b) (StateT ElabState (ExceptT TypeErrorA b)) (File Ann)
-> ReaderT
     (ElabEnv b) (StateT ElabState (ExceptT TypeErrorA b)) (File Ann)
forall env (b :: * -> *) (m :: * -> *) a.
HasLog' LogMsg env b m =>
Stage -> m a -> m a
setStage Stage
TypeInference
  (ReaderT
   (ElabEnv b) (StateT ElabState (ExceptT TypeErrorA b)) (File Ann)
 -> ReaderT
      (ElabEnv b) (StateT ElabState (ExceptT TypeErrorA b)) (File Ann))
-> (File InputAnn
    -> ReaderT
         (ElabEnv b) (StateT ElabState (ExceptT TypeErrorA b)) (File Ann))
-> File InputAnn
-> ReaderT
     (ElabEnv b) (StateT ElabState (ExceptT TypeErrorA b)) (File Ann)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Datatype ()]
-> File InputAnn
-> ReaderT
     (ElabEnv b) (StateT ElabState (ExceptT TypeErrorA b)) (File Ann)
forall (b :: * -> *) (m :: * -> *).
Elaborate b m =>
[Datatype ()] -> File InputAnn -> m (File Ann)
elaborateFile [Datatype ()]
builtinDats
  )

-- | Elaborate a source file
elaborateFile :: Elaborate b m => [Datatype ()] -> File InputAnn -> m (File Ann)
elaborateFile :: [Datatype ()] -> File InputAnn -> m (File Ann)
elaborateFile [Datatype ()]
builtinDats (File [Datatype InputAnn]
typeDefs [[TermDef InputAnn]]
termDefs) = do
  [Datatype Ann]
_ <- (Datatype InputAnn -> m (Datatype Ann))
-> [Datatype InputAnn] -> m [Datatype Ann]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse Datatype InputAnn -> m (Datatype Ann)
forall (b :: * -> *) (m :: * -> *).
Elaborate b m =>
Datatype InputAnn -> m (Datatype Ann)
elaborateTypeDef ([Datatype InputAnn] -> m [Datatype Ann])
-> [Datatype InputAnn] -> m [Datatype Ann]
forall a b. (a -> b) -> a -> b
$
    (Datatype () -> Datatype InputAnn)
-> [Datatype ()] -> [Datatype InputAnn]
forall a b. (a -> b) -> [a] -> [b]
map (InputAnn -> Datatype () -> Datatype InputAnn
forall b a. b -> Datatype a -> Datatype b
setTypeAnn (InputAnn -> Datatype () -> Datatype InputAnn)
-> InputAnn -> Datatype () -> Datatype InputAnn
forall a b. (a -> b) -> a -> b
$ String -> InputAnn
Parser.dummyAnn String
"builtin") [Datatype ()]
builtinDats
  -- We invent types for top level term definitions.
  -- These should be let polymorphic so we use @Polymorphic@ instead of @Monomorphic@
  [Datatype Ann]
typeDefs' <- (Datatype InputAnn -> m (Datatype Ann))
-> [Datatype InputAnn] -> m [Datatype Ann]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse Datatype InputAnn -> m (Datatype Ann)
forall (b :: * -> *) (m :: * -> *).
Elaborate b m =>
Datatype InputAnn -> m (Datatype Ann)
elaborateTypeDef [Datatype InputAnn]
typeDefs
  let
    names :: [[Text]]
names = ([TermDef InputAnn] -> [Text]) -> [[TermDef InputAnn]] -> [[Text]]
forall a b. (a -> b) -> [a] -> [b]
map ((TermDef InputAnn -> Text) -> [TermDef InputAnn] -> [Text]
forall a b. (a -> b) -> [a] -> [b]
map TermDef InputAnn -> Text
forall a. TermDef a -> Text
getTermName) [[TermDef InputAnn]]
termDefs
  [(Text, Typer)]
vars <- [[(Text, Typer)]] -> [(Text, Typer)]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ([[(Text, Typer)]] -> [(Text, Typer)])
-> m [[(Text, Typer)]] -> m [(Text, Typer)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ([Text] -> m [(Text, Typer)]) -> [[Text]] -> m [[(Text, Typer)]]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse ((Text -> m (Text, Typer)) -> [Text] -> m [(Text, Typer)]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse ((Text -> m (Text, Typer)) -> [Text] -> m [(Text, Typer)])
-> (Text -> m (Text, Typer)) -> [Text] -> m [(Text, Typer)]
forall a b. (a -> b) -> a -> b
$ \Text
name -> (,) Text
name (Typer -> (Text, Typer))
-> (Text -> Typer) -> Text -> (Text, Typer)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Text -> Typer
Polymorphic (Text -> (Text, Typer)) -> m Text -> m (Text, Typer)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Text -> m Text
forall (m :: * -> *). MonadState ElabState m => Text -> m Text
genTypeVar Text
"top") [[Text]]
names
  [Datatype Ann] -> [[TermDef Ann]] -> File Ann
forall a. [Datatype a] -> [[TermDef a]] -> File a
File [Datatype Ann]
typeDefs' ([[TermDef Ann]] -> File Ann) -> m [[TermDef Ann]] -> m (File Ann)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ([(Text, Typer)] -> m [[TermDef Ann]] -> m [[TermDef Ann]]
forall (b :: * -> *) (m :: * -> *) a.
Elaborate b m =>
[(Text, Typer)] -> m a -> m a
withEnv [(Text, Typer)]
vars (m [[TermDef Ann]] -> m [[TermDef Ann]])
-> m [[TermDef Ann]] -> m [[TermDef Ann]]
forall a b. (a -> b) -> a -> b
$ ([TermDef InputAnn] -> m [TermDef Ann])
-> [[TermDef InputAnn]] -> m [[TermDef Ann]]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse [TermDef InputAnn] -> m [TermDef Ann]
forall (b :: * -> *) (m :: * -> *).
Elaborate b m =>
[TermDef InputAnn] -> m [TermDef Ann]
elaborateGroup [[TermDef InputAnn]]
termDefs)

elaborateGroup :: Elaborate b m => [TermDef InputAnn] -> m [TermDef Ann]
elaborateGroup :: [TermDef InputAnn] -> m [TermDef Ann]
elaborateGroup [TermDef InputAnn]
termDefs = do
  m ()
forall (b :: * -> *) (m :: * -> *). Elaborate b m => m ()
newConstraintsGroup
  (TermDef InputAnn -> m (TermDef Ann))
-> [TermDef InputAnn] -> m [TermDef Ann]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse TermDef InputAnn -> m (TermDef Ann)
forall (b :: * -> *) (m :: * -> *).
Elaborate b m =>
TermDef InputAnn -> m (TermDef Ann)
elaborateDef [TermDef InputAnn]
termDefs


-- | Add a data type to the VariantEnv and elaborate it with a dummy type.
elaborateTypeDef :: Elaborate b m => Datatype InputAnn -> m (Datatype Ann)
elaborateTypeDef :: Datatype InputAnn -> m (Datatype Ann)
elaborateTypeDef = \case
  dt :: Datatype InputAnn
dt@(Datatype InputAnn
ann Text
typename [Text]
args [Variant (Maybe Type)]
variants) -> do
    let
      datatype :: Type
datatype = (Type -> Type -> Type) -> Type -> [Type] -> Type
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' Type -> Type -> Type
TypeApp (Text -> Type
TypeCon Text
typename) ((Text -> Type) -> [Text] -> [Type]
forall a b. (a -> b) -> [a] -> [b]
map Text -> Type
TypeVar [Text]
args)
      boundvars :: Set Text
boundvars = [Text] -> Set Text
forall a. Ord a => [a] -> Set a
S.fromList [Text]
args
      variantsvars :: [Text]
variantsvars = [ Text
t | TypeVar Text
t <- [Variant (Maybe Type)] -> [Type]
forall from to. Biplate from to => from -> [to]
U.universeBi [Variant (Maybe Type)]
variants ]
      constrs :: Set Text
constrs = [Text] -> Set Text
forall a. Ord a => [a] -> Set a
S.fromList ([Text] -> Set Text) -> [Text] -> Set Text
forall a b. (a -> b) -> a -> b
$ (Variant (Maybe Type) -> Text) -> [Variant (Maybe Type)] -> [Text]
forall a b. (a -> b) -> [a] -> [b]
map (\(Variant Text
constr Maybe Type
_) -> Text
constr) [Variant (Maybe Type)]
variants
    
    -- check for duplicate data constructors, duplicate type variables
    -- and unbound type vars
    Bool -> m () -> m ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Set Text -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length Set Text
boundvars Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== [Text] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Text]
args) (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$
      [InputAnn] -> TypeError -> m ()
forall (m :: * -> *) a.
MonadError TypeErrorA m =>
[InputAnn] -> TypeError -> m a
throwErr [InputAnn
ann] (TypeError -> m ()) -> TypeError -> m ()
forall a b. (a -> b) -> a -> b
$ Datatype InputAnn -> TypeError
DuplicateTypeVarsInSig Datatype InputAnn
dt

    Bool -> m () -> m ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless ([Variant (Maybe Type)] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Variant (Maybe Type)]
variants Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Set Text -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length Set Text
constrs) (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$
      [InputAnn] -> TypeError -> m ()
forall (m :: * -> *) a.
MonadError TypeErrorA m =>
[InputAnn] -> TypeError -> m a
throwErr [InputAnn
ann] (TypeError -> m ()) -> TypeError -> m ()
forall a b. (a -> b) -> a -> b
$ Datatype InputAnn -> TypeError
DuplicateConstrs Datatype InputAnn
dt

    Bool -> m () -> m ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless ((Text -> Bool) -> [Text] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (Text -> Set Text -> Bool
forall a. Ord a => a -> Set a -> Bool
`S.member` Set Text
boundvars) [Text]
variantsvars) (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$
      [InputAnn] -> TypeError -> m ()
forall (m :: * -> *) a.
MonadError TypeErrorA m =>
[InputAnn] -> TypeError -> m a
throwErr [InputAnn
ann] (TypeError -> m ()) -> TypeError -> m ()
forall a b. (a -> b) -> a -> b
$ Datatype InputAnn -> TypeError
UnboundTypeVarsInType Datatype InputAnn
dt

    -- convert to @VariantSig@s
    let
      variantsigs :: VariantEnv InputAnn
variantsigs = [(Text, VariantSig InputAnn)] -> VariantEnv InputAnn
forall k a. Ord k => [(k, a)] -> Map k a
M.fromList ([(Text, VariantSig InputAnn)] -> VariantEnv InputAnn)
-> [(Text, VariantSig InputAnn)] -> VariantEnv InputAnn
forall a b. (a -> b) -> a -> b
$
        (Variant (Maybe Type) -> (Text, VariantSig InputAnn))
-> [Variant (Maybe Type)] -> [(Text, VariantSig InputAnn)]
forall a b. (a -> b) -> [a] -> [b]
map (\(Variant Text
constr Maybe Type
template) -> (Text
constr, Type -> Maybe Type -> InputAnn -> VariantSig InputAnn
forall a. Type -> Maybe Type -> a -> VariantSig a
VariantSig Type
datatype Maybe Type
template InputAnn
ann)) [Variant (Maybe Type)]
variants
    VariantEnv InputAnn -> m ()
forall (b :: * -> *) (m :: * -> *).
Elaborate b m =>
VariantEnv InputAnn -> m ()
addVariantSigs VariantEnv InputAnn
variantsigs
    
    Datatype Ann -> m (Datatype Ann)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Ann -> Text -> [Text] -> [Variant (Maybe Type)] -> Datatype Ann
forall a.
a -> Text -> [Text] -> [Variant (Maybe Type)] -> Datatype a
Datatype (InputAnn -> Type -> Ann
Ann InputAnn
ann Type
tUnit) Text
typename [Text]
args [Variant (Maybe Type)]
variants)

-- | Elaborate a @TermDef@
elaborateDef :: Elaborate b m => TermDef InputAnn -> m (TermDef Ann)
elaborateDef :: TermDef InputAnn -> m (TermDef Ann)
elaborateDef TermDef InputAnn
def = do
  
  -- we need to change the type of def in the current environment for recursive functions
  let
    name :: Text
name = TermDef InputAnn -> Text
forall a. TermDef a -> Text
getTermName TermDef InputAnn
def
    ann :: InputAnn
ann = TermDef InputAnn -> InputAnn
forall ann. TermDef ann -> ann
getTermAnn TermDef InputAnn
def
  Text
t <- InputAnn -> Text -> m Typer
forall (b :: * -> *) (m :: * -> *).
Elaborate b m =>
InputAnn -> Text -> m Typer
lookupVar InputAnn
ann Text
name m Typer -> (Typer -> m Text) -> m Text
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
    Polymorphic Text
t' ->
      Text -> m Text
forall (f :: * -> *) a. Applicative f => a -> f a
pure Text
t'
      -- @t'@ is the type other definitions see.
      -- It is an instantiation of the type we just elaborated for def.
    Monomorphic Type
t' ->
      String -> m Text
forall a. HasCallStack => String -> a
error (String -> m Text) -> String -> m Text
forall a b. (a -> b) -> a -> b
$ Text -> String
toString (Text -> String) -> Text -> String
forall a b. (a -> b) -> a -> b
$ Text
"unexpected Typer: " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Type -> Text
forall a. Show a => a -> Text
pShow Type
t'
  -- When evaluating a definition, the type should not be let polymorphic.
  ElabInfo (TermDef Ann)
elab <- [(Text, Typer)]
-> m (ElabInfo (TermDef Ann)) -> m (ElabInfo (TermDef Ann))
forall (b :: * -> *) (m :: * -> *) a.
Elaborate b m =>
[(Text, Typer)] -> m a -> m a
withEnv [(Text
name, Type -> Typer
Monomorphic (Type -> Typer) -> Type -> Typer
forall a b. (a -> b) -> a -> b
$ Text -> Type
TypeVar Text
t)] (m (ElabInfo (TermDef Ann)) -> m (ElabInfo (TermDef Ann)))
-> m (ElabInfo (TermDef Ann)) -> m (ElabInfo (TermDef Ann))
forall a b. (a -> b) -> a -> b
$ TermDef InputAnn -> m (ElabInfo (TermDef Ann))
forall (b :: * -> *) (m :: * -> *).
Elaborate b m =>
TermDef InputAnn -> m (ElabInfo (TermDef Ann))
elaborateTermDef TermDef InputAnn
def
  InputAnn -> Constraint -> m ()
forall (b :: * -> *) (m :: * -> *).
Elaborate b m =>
InputAnn -> Constraint -> m ()
constrain InputAnn
ann (Constraint -> m ()) -> Constraint -> m ()
forall a b. (a -> b) -> a -> b
$ Type -> Type -> Constraint
Equality (Text -> Type
TypeVar Text
t) (ElabInfo (TermDef Ann) -> Type
forall a. ElabInfo a -> Type
eiType ElabInfo (TermDef Ann)
elab)
  TermDef Ann -> m (TermDef Ann)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (TermDef Ann -> m (TermDef Ann)) -> TermDef Ann -> m (TermDef Ann)
forall a b. (a -> b) -> a -> b
$ Ann -> TermDef Ann -> TermDef Ann
forall a. a -> TermDef a -> TermDef a
setTermAnn (InputAnn -> Type -> Ann
Ann InputAnn
ann (Type -> Ann) -> Type -> Ann
forall a b. (a -> b) -> a -> b
$ ElabInfo (TermDef Ann) -> Type
forall a. ElabInfo a -> Type
eiType ElabInfo (TermDef Ann)
elab) (TermDef Ann -> TermDef Ann) -> TermDef Ann -> TermDef Ann
forall a b. (a -> b) -> a -> b
$ ElabInfo (TermDef Ann) -> TermDef Ann
forall a. ElabInfo a -> a
eiResult ElabInfo (TermDef Ann)
elab

-- | Elaborate a term definition helper function
elaborateTermDef :: Elaborate b m => TermDef InputAnn -> m (ElabInfo (TermDef Ann))
elaborateTermDef :: TermDef InputAnn -> m (ElabInfo (TermDef Ann))
elaborateTermDef = \case
  Variable InputAnn
ann Text
name Expr InputAnn
expr -> do
    Expr Ann
expr' <- InputAnn -> Expr InputAnn -> m (Expr Ann)
forall (b :: * -> *) (m :: * -> *).
Elaborate b m =>
InputAnn -> Expr InputAnn -> m (Expr Ann)
elaborateExpr InputAnn
ann Expr InputAnn
expr
    Bool -> m () -> m ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Text
name Text -> Text -> Bool
forall a. Eq a => a -> a -> Bool
== Text
"main") (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$
      InputAnn -> Constraint -> m ()
forall (b :: * -> *) (m :: * -> *).
Elaborate b m =>
InputAnn -> Constraint -> m ()
constrain InputAnn
ann (Constraint -> m ()) -> Constraint -> m ()
forall a b. (a -> b) -> a -> b
$ Type -> Type -> Constraint
Equality (Expr Ann -> Type
getType Expr Ann
expr') (Type -> Type
tIO Type
tUnit)
    ElabInfo (TermDef Ann) -> m (ElabInfo (TermDef Ann))
forall (f :: * -> *) a. Applicative f => a -> f a
pure (ElabInfo (TermDef Ann) -> m (ElabInfo (TermDef Ann)))
-> ElabInfo (TermDef Ann) -> m (ElabInfo (TermDef Ann))
forall a b. (a -> b) -> a -> b
$ ElabInfo :: forall a. a -> Type -> Env Typer -> ElabInfo a
ElabInfo
      { eiType :: Type
eiType = Expr Ann -> Type
getType Expr Ann
expr'
      , eiResult :: TermDef Ann
eiResult = Ann -> Text -> Expr Ann -> TermDef Ann
forall a. a -> Text -> Expr a -> TermDef a
Variable (InputAnn -> Type -> Ann
Ann InputAnn
ann (Type -> Ann) -> Type -> Ann
forall a b. (a -> b) -> a -> b
$ Expr Ann -> Type
getType Expr Ann
expr') Text
name Expr Ann
expr'
      , eiNewEnv :: Env Typer
eiNewEnv = Env Typer
forall a. Monoid a => a
mempty
      }
  Function InputAnn
ann Text
name [Maybe Text]
args Expr InputAnn
body -> do
    Text
tfun <- Text -> m Text
forall (m :: * -> *). MonadState ElabState m => Text -> m Text
genTypeVar Text
"tfun"
    [(Maybe Text, Text)]
targsEnv <- (Maybe Text -> m (Maybe Text, Text))
-> [Maybe Text] -> m [(Maybe Text, Text)]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse (\Maybe Text
arg -> (,) Maybe Text
arg (Text -> (Maybe Text, Text)) -> m Text -> m (Maybe Text, Text)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Text -> m Text
forall (m :: * -> *). MonadState ElabState m => Text -> m Text
genTypeVar Text
"targ") [Maybe Text]
args
    Expr Ann
body' <- [(Text, Typer)] -> m (Expr Ann) -> m (Expr Ann)
forall (b :: * -> *) (m :: * -> *) a.
Elaborate b m =>
[(Text, Typer)] -> m a -> m a
withEnv
      ( (Text
name, Type -> Typer
Monomorphic (Type -> Typer) -> Type -> Typer
forall a b. (a -> b) -> a -> b
$ Text -> Type
TypeVar Text
tfun)
        (Text, Typer) -> [(Text, Typer)] -> [(Text, Typer)]
forall a. a -> [a] -> [a]
: ((Maybe Text, Text) -> Maybe (Text, Typer))
-> [(Maybe Text, Text)] -> [(Text, Typer)]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe (\(Maybe Text
var, Text
t) -> (Text -> Typer -> (Text, Typer)) -> Typer -> Text -> (Text, Typer)
forall a b c. (a -> b -> c) -> b -> a -> c
flip (,) (Type -> Typer
Monomorphic (Type -> Typer) -> Type -> Typer
forall a b. (a -> b) -> a -> b
$ Text -> Type
TypeVar Text
t) (Text -> (Text, Typer)) -> Maybe Text -> Maybe (Text, Typer)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe Text
var)
        [(Maybe Text, Text)]
targsEnv
      )
      (InputAnn -> Expr InputAnn -> m (Expr Ann)
forall (b :: * -> *) (m :: * -> *).
Elaborate b m =>
InputAnn -> Expr InputAnn -> m (Expr Ann)
elaborateExpr InputAnn
ann Expr InputAnn
body)

    let
      tret :: Type
tret = Expr Ann -> Type
getType Expr Ann
body'
      tfunexpanded :: Type
tfunexpanded = [Type] -> Type -> Type
typeFun (((Maybe Text, Text) -> Type) -> [(Maybe Text, Text)] -> [Type]
forall a b. (a -> b) -> [a] -> [b]
map (Text -> Type
TypeVar (Text -> Type)
-> ((Maybe Text, Text) -> Text) -> (Maybe Text, Text) -> Type
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Maybe Text, Text) -> Text
forall a b. (a, b) -> b
snd) [(Maybe Text, Text)]
targsEnv) Type
tret

    InputAnn -> Constraint -> m ()
forall (b :: * -> *) (m :: * -> *).
Elaborate b m =>
InputAnn -> Constraint -> m ()
constrain InputAnn
ann (Constraint -> m ()) -> Constraint -> m ()
forall a b. (a -> b) -> a -> b
$ Type -> Type -> Constraint
Equality
      (Text -> Type
TypeVar Text
tfun)
      Type
tfunexpanded

    Bool -> m () -> m ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Text
name Text -> Text -> Bool
forall a. Eq a => a -> a -> Bool
== Text
"main") (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$
      InputAnn -> Constraint -> m ()
forall (b :: * -> *) (m :: * -> *).
Elaborate b m =>
InputAnn -> Constraint -> m ()
constrain InputAnn
ann (Constraint -> m ()) -> Constraint -> m ()
forall a b. (a -> b) -> a -> b
$ Type -> Type -> Constraint
Equality (Text -> Type
TypeVar Text
tfun) (Type -> Type
tIO Type
tUnit)

    ElabInfo (TermDef Ann) -> m (ElabInfo (TermDef Ann))
forall (f :: * -> *) a. Applicative f => a -> f a
pure (ElabInfo (TermDef Ann) -> m (ElabInfo (TermDef Ann)))
-> ElabInfo (TermDef Ann) -> m (ElabInfo (TermDef Ann))
forall a b. (a -> b) -> a -> b
$ ElabInfo :: forall a. a -> Type -> Env Typer -> ElabInfo a
ElabInfo
      { eiType :: Type
eiType = Type
tfunexpanded
      , eiResult :: TermDef Ann
eiResult = Ann -> Text -> [Maybe Text] -> Expr Ann -> TermDef Ann
forall a. a -> Text -> [Maybe Text] -> Expr a -> TermDef a
Function (InputAnn -> Type -> Ann
Ann InputAnn
ann Type
tfunexpanded) Text
name [Maybe Text]
args Expr Ann
body'
      , eiNewEnv :: Env Typer
eiNewEnv = Env Typer
forall a. Monoid a => a
mempty
      }

-- | Elaborate a list of statements.
--   Returns the type of the final statement as well.
elaborateBlock :: Elaborate b m => Block InputAnn -> m (Type, Block Ann)
elaborateBlock :: Block InputAnn -> m (Type, Block Ann)
elaborateBlock Block InputAnn
block = do
  -- we want to fold over the list of statements, and for each new definition,
  -- add it to the environment for the elaboration of the next expressions
  ElabInfo (Block Ann)
block' <- (ElabInfo (Block Ann)
 -> Statement InputAnn -> m (ElabInfo (Block Ann)))
-> ElabInfo (Block Ann)
-> Block InputAnn
-> m (ElabInfo (Block Ann))
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM
    ( \ElabInfo (Block Ann)
blockinfo Statement InputAnn
stmt -> do
      ElabInfo (Statement Ann)
stmt' <- Env Typer
-> m (ElabInfo (Statement Ann)) -> m (ElabInfo (Statement Ann))
forall (b :: * -> *) (m :: * -> *) a.
Elaborate b m =>
Env Typer -> m a -> m a
withEnv' (ElabInfo (Block Ann) -> Env Typer
forall a. ElabInfo a -> Env Typer
eiNewEnv ElabInfo (Block Ann)
blockinfo) (m (ElabInfo (Statement Ann)) -> m (ElabInfo (Statement Ann)))
-> m (ElabInfo (Statement Ann)) -> m (ElabInfo (Statement Ann))
forall a b. (a -> b) -> a -> b
$ Statement InputAnn -> m (ElabInfo (Statement Ann))
forall (b :: * -> *) (m :: * -> *).
Elaborate b m =>
Statement InputAnn -> m (ElabInfo (Statement Ann))
elaborateStmt Statement InputAnn
stmt
      ElabInfo (Block Ann) -> m (ElabInfo (Block Ann))
forall (f :: * -> *) a. Applicative f => a -> f a
pure (ElabInfo (Block Ann) -> m (ElabInfo (Block Ann)))
-> ElabInfo (Block Ann) -> m (ElabInfo (Block Ann))
forall a b. (a -> b) -> a -> b
$ ElabInfo :: forall a. a -> Type -> Env Typer -> ElabInfo a
ElabInfo
        { eiResult :: Block Ann
eiResult = ElabInfo (Statement Ann) -> Statement Ann
forall a. ElabInfo a -> a
eiResult ElabInfo (Statement Ann)
stmt' Statement Ann -> Block Ann -> Block Ann
forall a. a -> [a] -> [a]
: ElabInfo (Block Ann) -> Block Ann
forall a. ElabInfo a -> a
eiResult ElabInfo (Block Ann)
blockinfo
        , eiType :: Type
eiType = ElabInfo (Statement Ann) -> Type
forall a. ElabInfo a -> Type
eiType ElabInfo (Statement Ann)
stmt'
        , eiNewEnv :: Env Typer
eiNewEnv = Env Typer -> Env Typer -> Env Typer
forall k a. Ord k => Map k a -> Map k a -> Map k a
M.union (ElabInfo (Statement Ann) -> Env Typer
forall a. ElabInfo a -> Env Typer
eiNewEnv ElabInfo (Statement Ann)
stmt') (ElabInfo (Block Ann) -> Env Typer
forall a. ElabInfo a -> Env Typer
eiNewEnv ElabInfo (Block Ann)
blockinfo)
        }
    )
    (Block Ann -> Type -> Env Typer -> ElabInfo (Block Ann)
forall a. a -> Type -> Env Typer -> ElabInfo a
ElabInfo [] (Type -> Type
tIO Type
tUnit) Env Typer
forall a. Monoid a => a
mempty)
    Block InputAnn
block
  (Type, Block Ann) -> m (Type, Block Ann)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (ElabInfo (Block Ann) -> Type
forall a. ElabInfo a -> Type
eiType ElabInfo (Block Ann)
block', Block Ann -> Block Ann
forall a. [a] -> [a]
reverse (ElabInfo (Block Ann) -> Block Ann
forall a. ElabInfo a -> a
eiResult ElabInfo (Block Ann)
block'))

-- | Elaborate a single statement.
elaborateStmt :: Elaborate b m => Statement InputAnn -> m (ElabInfo (Statement Ann))
elaborateStmt :: Statement InputAnn -> m (ElabInfo (Statement Ann))
elaborateStmt = \case
  SExpr InputAnn
ann Expr InputAnn
expr -> do
    Expr Ann
expr' <- InputAnn -> Expr InputAnn -> m (Expr Ann)
forall (b :: * -> *) (m :: * -> *).
Elaborate b m =>
InputAnn -> Expr InputAnn -> m (Expr Ann)
elaborateExpr InputAnn
ann Expr InputAnn
expr
    Type
t <- Text -> Type
TypeVar (Text -> Type) -> m Text -> m Type
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Text -> m Text
forall (m :: * -> *). MonadState ElabState m => Text -> m Text
genTypeVar Text
"t"
    InputAnn -> Constraint -> m ()
forall (b :: * -> *) (m :: * -> *).
Elaborate b m =>
InputAnn -> Constraint -> m ()
constrain InputAnn
ann (Constraint -> m ()) -> Constraint -> m ()
forall a b. (a -> b) -> a -> b
$ Type -> Type -> Constraint
Equality (Expr Ann -> Type
getType Expr Ann
expr') (Type -> Type
tIO Type
t)
    ElabInfo (Statement Ann) -> m (ElabInfo (Statement Ann))
forall (f :: * -> *) a. Applicative f => a -> f a
pure (ElabInfo (Statement Ann) -> m (ElabInfo (Statement Ann)))
-> ElabInfo (Statement Ann) -> m (ElabInfo (Statement Ann))
forall a b. (a -> b) -> a -> b
$ ElabInfo :: forall a. a -> Type -> Env Typer -> ElabInfo a
ElabInfo
      { eiResult :: Statement Ann
eiResult = Ann -> Expr Ann -> Statement Ann
forall a. a -> Expr a -> Statement a
SExpr (InputAnn -> Type -> Ann
Ann InputAnn
ann (Expr Ann -> Type
getType Expr Ann
expr')) Expr Ann
expr'
      , eiType :: Type
eiType = Expr Ann -> Type
getType Expr Ann
expr'
      , eiNewEnv :: Env Typer
eiNewEnv = Env Typer
forall a. Monoid a => a
mempty
      }

  SDef InputAnn
ann TermDef InputAnn
def -> do
    ElabInfo TermDef Ann
def' Type
t Env Typer
_ <- TermDef InputAnn -> m (ElabInfo (TermDef Ann))
forall (b :: * -> *) (m :: * -> *).
Elaborate b m =>
TermDef InputAnn -> m (ElabInfo (TermDef Ann))
elaborateTermDef TermDef InputAnn
def
    ElabInfo (Statement Ann) -> m (ElabInfo (Statement Ann))
forall (f :: * -> *) a. Applicative f => a -> f a
pure (ElabInfo (Statement Ann) -> m (ElabInfo (Statement Ann)))
-> ElabInfo (Statement Ann) -> m (ElabInfo (Statement Ann))
forall a b. (a -> b) -> a -> b
$ ElabInfo :: forall a. a -> Type -> Env Typer -> ElabInfo a
ElabInfo
      { eiResult :: Statement Ann
eiResult = Ann -> TermDef Ann -> Statement Ann
forall a. a -> TermDef a -> Statement a
SDef (InputAnn -> Type -> Ann
Ann InputAnn
ann Type
t) TermDef Ann
def'
      , eiType :: Type
eiType = Type
t
      , eiNewEnv :: Env Typer
eiNewEnv = Text -> Typer -> Env Typer
forall k a. k -> a -> Map k a
M.singleton (TermDef Ann -> Text
forall a. TermDef a -> Text
getTermName TermDef Ann
def') (Type -> Typer
Monomorphic Type
t)
      }

  SBind InputAnn
ann Text
name Expr InputAnn
expr -> do
    Expr Ann
expr' <- InputAnn -> Expr InputAnn -> m (Expr Ann)
forall (b :: * -> *) (m :: * -> *).
Elaborate b m =>
InputAnn -> Expr InputAnn -> m (Expr Ann)
elaborateExpr InputAnn
ann Expr InputAnn
expr
    Type
t <- Text -> Type
TypeVar (Text -> Type) -> m Text -> m Type
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Text -> m Text
forall (m :: * -> *). MonadState ElabState m => Text -> m Text
genTypeVar Text
"t"
    let t' :: Type
t' = Expr Ann -> Type
getType Expr Ann
expr'
    InputAnn -> Constraint -> m ()
forall (b :: * -> *) (m :: * -> *).
Elaborate b m =>
InputAnn -> Constraint -> m ()
constrain InputAnn
ann (Constraint -> m ()) -> Constraint -> m ()
forall a b. (a -> b) -> a -> b
$ Type -> Type -> Constraint
Equality Type
t' (Type -> Type
tIO Type
t)
    ElabInfo (Statement Ann) -> m (ElabInfo (Statement Ann))
forall (f :: * -> *) a. Applicative f => a -> f a
pure (ElabInfo (Statement Ann) -> m (ElabInfo (Statement Ann)))
-> ElabInfo (Statement Ann) -> m (ElabInfo (Statement Ann))
forall a b. (a -> b) -> a -> b
$ ElabInfo :: forall a. a -> Type -> Env Typer -> ElabInfo a
ElabInfo
      { eiResult :: Statement Ann
eiResult = Ann -> Text -> Expr Ann -> Statement Ann
forall a. a -> Text -> Expr a -> Statement a
SBind (InputAnn -> Type -> Ann
Ann InputAnn
ann Type
t) Text
name Expr Ann
expr'
      , eiType :: Type
eiType = Type
t'
      , eiNewEnv :: Env Typer
eiNewEnv = Text -> Typer -> Env Typer
forall k a. k -> a -> Map k a
M.singleton Text
name (Type -> Typer
Monomorphic Type
t)
      }

-- | Elaborate an expression.
--   Traverses the expression Top-Down.
elaborateExpr :: Elaborate b m => InputAnn -> Expr InputAnn -> m (Expr Ann)
elaborateExpr :: InputAnn -> Expr InputAnn -> m (Expr Ann)
elaborateExpr InputAnn
ann = \case
  -- Replace the current annotation an evaluate the inner expression
  EAnnotated InputAnn
ann' Expr InputAnn
e ->
    InputAnn -> Expr InputAnn -> m (Expr Ann)
forall (b :: * -> *) (m :: * -> *).
Elaborate b m =>
InputAnn -> Expr InputAnn -> m (Expr Ann)
elaborateExpr InputAnn
ann' Expr InputAnn
e

  -- The types of literals are known.
  ELit Lit
lit ->
    Expr Ann -> m (Expr Ann)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Expr Ann -> m (Expr Ann)) -> Expr Ann -> m (Expr Ann)
forall a b. (a -> b) -> a -> b
$ Ann -> Expr Ann -> Expr Ann
forall a. a -> Expr a -> Expr a
EAnnotated (InputAnn -> Type -> Ann
Ann InputAnn
ann (Type -> Ann) -> Type -> Ann
forall a b. (a -> b) -> a -> b
$ Lit -> Type
getLitType Lit
lit) (Lit -> Expr Ann
forall a. Lit -> Expr a
ELit Lit
lit)

  -- For variables, we look it up in the environment
  EVar Text
var -> do
    Maybe Typer
typer <- Text -> m (Maybe Typer)
forall (b :: * -> *) (m :: * -> *).
Elaborate b m =>
Text -> m (Maybe Typer)
lookupVarMaybe Text
var
    Type
typ <- case Maybe Typer
typer of
      Just (Monomorphic Type
t) -> Type -> m Type
forall (f :: * -> *) a. Applicative f => a -> f a
pure Type
t
      -- For let-polymorphism
      Just (Polymorphic Text
t) -> do
        Text
tv <- Text -> m Text
forall (m :: * -> *). MonadState ElabState m => Text -> m Text
genTypeVar (Text -> m Text) -> Text -> m Text
forall a b. (a -> b) -> a -> b
$ Text
t Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
"_i"
        InputAnn -> Constraint -> m ()
forall (b :: * -> *) (m :: * -> *).
Elaborate b m =>
InputAnn -> Constraint -> m ()
constrain InputAnn
ann (Constraint -> m ()) -> Constraint -> m ()
forall a b. (a -> b) -> a -> b
$ Type -> Type -> Constraint
InstanceOf (Text -> Type
TypeVar Text
tv) (Text -> Type
TypeVar Text
t)
        Type -> m Type
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Type -> m Type) -> Type -> m Type
forall a b. (a -> b) -> a -> b
$ Text -> Type
TypeVar Text
tv
      Maybe Typer
Nothing -> do
        Type
t <- InputAnn -> Text -> m Type
forall (b :: * -> *) (m :: * -> *).
Elaborate b m =>
InputAnn -> Text -> m Type
lookupBuiltin InputAnn
ann Text
var
        (Env Text, Type) -> Type
forall a b. (a, b) -> b
snd ((Env Text, Type) -> Type) -> m (Env Text, Type) -> m Type
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Text -> Type -> m (Env Text, Type)
forall (b :: * -> *) (m :: * -> *).
Solve b m =>
Text -> Type -> m (Env Text, Type)
instantiate Text
"ti" Type
t

    Expr Ann -> m (Expr Ann)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Expr Ann -> m (Expr Ann)) -> Expr Ann -> m (Expr Ann)
forall a b. (a -> b) -> a -> b
$ Ann -> Expr Ann -> Expr Ann
forall a. a -> Expr a -> Expr a
EAnnotated (InputAnn -> Type -> Ann
Ann InputAnn
ann Type
typ) (Expr Ann -> Expr Ann) -> Expr Ann -> Expr Ann
forall a b. (a -> b) -> a -> b
$
      Text -> Expr Ann
forall a. Text -> Expr a
EVar Text
var

  -- Generate type variables for function arguments, and annotate
  -- the body with the arguments in the environment.
  -- The result type should be a function from the arguments types to the type of the body
  EFun [Maybe Text]
args Expr InputAnn
body -> do
    [(Maybe Text, Text)]
targsEnv <- (Maybe Text -> m (Maybe Text, Text))
-> [Maybe Text] -> m [(Maybe Text, Text)]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse (\Maybe Text
arg -> (,) Maybe Text
arg (Text -> (Maybe Text, Text)) -> m Text -> m (Maybe Text, Text)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Text -> m Text
forall (m :: * -> *). MonadState ElabState m => Text -> m Text
genTypeVar Text
"t") [Maybe Text]
args
    Expr Ann
body' <- [(Text, Typer)] -> m (Expr Ann) -> m (Expr Ann)
forall (b :: * -> *) (m :: * -> *) a.
Elaborate b m =>
[(Text, Typer)] -> m a -> m a
withEnv
      ( ((Maybe Text, Text) -> Maybe (Text, Typer))
-> [(Maybe Text, Text)] -> [(Text, Typer)]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe (\(Maybe Text
var, Text
t) -> (Text -> Typer -> (Text, Typer)) -> Typer -> Text -> (Text, Typer)
forall a b c. (a -> b -> c) -> b -> a -> c
flip (,) (Type -> Typer
Monomorphic (Type -> Typer) -> Type -> Typer
forall a b. (a -> b) -> a -> b
$ Text -> Type
TypeVar Text
t) (Text -> (Text, Typer)) -> Maybe Text -> Maybe (Text, Typer)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe Text
var)
        [(Maybe Text, Text)]
targsEnv
      )
      (InputAnn -> Expr InputAnn -> m (Expr Ann)
forall (b :: * -> *) (m :: * -> *).
Elaborate b m =>
InputAnn -> Expr InputAnn -> m (Expr Ann)
elaborateExpr InputAnn
ann Expr InputAnn
body)

    let tret :: Type
tret = Expr Ann -> Type
getType Expr Ann
body'

    let tfun :: Type
tfun = [Type] -> Type -> Type
typeFun (((Maybe Text, Text) -> Type) -> [(Maybe Text, Text)] -> [Type]
forall a b. (a -> b) -> [a] -> [b]
map (Text -> Type
TypeVar (Text -> Type)
-> ((Maybe Text, Text) -> Text) -> (Maybe Text, Text) -> Type
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Maybe Text, Text) -> Text
forall a b. (a, b) -> b
snd) [(Maybe Text, Text)]
targsEnv) Type
tret

    Expr Ann -> m (Expr Ann)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Expr Ann -> m (Expr Ann)) -> Expr Ann -> m (Expr Ann)
forall a b. (a -> b) -> a -> b
$ Ann -> Expr Ann -> Expr Ann
forall a. a -> Expr a -> Expr a
EAnnotated (InputAnn -> Type -> Ann
Ann InputAnn
ann Type
tfun) (Expr Ann -> Expr Ann) -> Expr Ann -> Expr Ann
forall a b. (a -> b) -> a -> b
$
      [Maybe Text] -> Expr Ann -> Expr Ann
forall a. [Maybe Text] -> Expr a -> Expr a
EFun [Maybe Text]
args Expr Ann
body'

  -- Generate a return type and constrain the type of the function as
  -- a function from the arguments types to the generated return type
  EFunCall Expr InputAnn
f [Expr InputAnn]
args -> do
    Expr Ann
f' <- InputAnn -> Expr InputAnn -> m (Expr Ann)
forall (b :: * -> *) (m :: * -> *).
Elaborate b m =>
InputAnn -> Expr InputAnn -> m (Expr Ann)
elaborateExpr InputAnn
ann Expr InputAnn
f
    [Expr Ann]
args' <- (Expr InputAnn -> m (Expr Ann)) -> [Expr InputAnn] -> m [Expr Ann]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse (InputAnn -> Expr InputAnn -> m (Expr Ann)
forall (b :: * -> *) (m :: * -> *).
Elaborate b m =>
InputAnn -> Expr InputAnn -> m (Expr Ann)
elaborateExpr InputAnn
ann) [Expr InputAnn]
args
    Type
tret <- Text -> Type
TypeVar (Text -> Type) -> m Text -> m Type
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Text -> m Text
forall (m :: * -> *). MonadState ElabState m => Text -> m Text
genTypeVar Text
"t"
    InputAnn -> Constraint -> m ()
forall (b :: * -> *) (m :: * -> *).
Elaborate b m =>
InputAnn -> Constraint -> m ()
constrain InputAnn
ann (Constraint -> m ()) -> Constraint -> m ()
forall a b. (a -> b) -> a -> b
$ Type -> Type -> Constraint
Equality
      (Expr Ann -> Type
getType Expr Ann
f')
      ([Type] -> Type -> Type
typeFun ((Expr Ann -> Type) -> [Expr Ann] -> [Type]
forall a b. (a -> b) -> [a] -> [b]
map Expr Ann -> Type
getType [Expr Ann]
args') Type
tret)
    Expr Ann -> m (Expr Ann)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Expr Ann -> m (Expr Ann)) -> Expr Ann -> m (Expr Ann)
forall a b. (a -> b) -> a -> b
$ Ann -> Expr Ann -> Expr Ann
forall a. a -> Expr a -> Expr a
EAnnotated (InputAnn -> Type -> Ann
Ann InputAnn
ann Type
tret) (Expr Ann -> Expr Ann) -> Expr Ann -> Expr Ann
forall a b. (a -> b) -> a -> b
$
      Expr Ann -> [Expr Ann] -> Expr Ann
forall a. Expr a -> [Expr a] -> Expr a
EFunCall Expr Ann
f' [Expr Ann]
args'

  -- If we have a type for an ffi call supplied by the user, we'll use it for type inference.
  -- otherwise we'll take any amount and any type of arguments and return IO {}.
  EFfi Text
f Maybe Type
mtype [Expr InputAnn]
args -> do
    [Expr Ann]
args' <- (Expr InputAnn -> m (Expr Ann)) -> [Expr InputAnn] -> m [Expr Ann]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse (InputAnn -> Expr InputAnn -> m (Expr Ann)
forall (b :: * -> *) (m :: * -> *).
Elaborate b m =>
InputAnn -> Expr InputAnn -> m (Expr Ann)
elaborateExpr InputAnn
ann) [Expr InputAnn]
args
    case Maybe Type
mtype of
      Maybe Type
Nothing -> do
        Expr Ann -> m (Expr Ann)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Expr Ann -> m (Expr Ann)) -> Expr Ann -> m (Expr Ann)
forall a b. (a -> b) -> a -> b
$ Ann -> Expr Ann -> Expr Ann
forall a. a -> Expr a -> Expr a
EAnnotated (InputAnn -> Type -> Ann
Ann InputAnn
ann (Type -> Type
tIO Type
tUnit)) (Expr Ann -> Expr Ann) -> Expr Ann -> Expr Ann
forall a b. (a -> b) -> a -> b
$
          Text -> Maybe Type -> [Expr Ann] -> Expr Ann
forall a. Text -> Maybe Type -> [Expr a] -> Expr a
EFfi Text
f Maybe Type
forall a. Maybe a
Nothing [Expr Ann]
args'
      Just Type
t -> do
        let ([Type]
targs, Type
tret) = Type -> ([Type], Type)
toTypeFun Type
t

        Bool -> m () -> m ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless ([Expr Ann] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Expr Ann]
args' Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== [Type] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Type]
targs) (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$ do
          Type
tmp <- Text -> Type
TypeVar (Text -> Type) -> m Text -> m Type
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Text -> m Text
forall (m :: * -> *). MonadState ElabState m => Text -> m Text
genTypeVar Text
"t"
          [InputAnn] -> TypeError -> m ()
forall (m :: * -> *) a.
MonadError TypeErrorA m =>
[InputAnn] -> TypeError -> m a
throwErr [InputAnn
ann] (TypeError -> m ()) -> TypeError -> m ()
forall a b. (a -> b) -> a -> b
$ Type -> Type -> TypeError
ArityMismatch Type
t ([Type] -> Type -> Type
typeFun ((Expr Ann -> Type) -> [Expr Ann] -> [Type]
forall a b. (a -> b) -> [a] -> [b]
map Expr Ann -> Type
getType [Expr Ann]
args') Type
tmp)

        (Type -> Type -> m ()) -> [Type] -> [Type] -> m ()
forall (m :: * -> *) a b c.
Applicative m =>
(a -> b -> m c) -> [a] -> [b] -> m ()
zipWithM_ ((Constraint -> m ()) -> (Type -> Constraint) -> Type -> m ()
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (InputAnn -> Constraint -> m ()
forall (b :: * -> *) (m :: * -> *).
Elaborate b m =>
InputAnn -> Constraint -> m ()
constrain InputAnn
ann) ((Type -> Constraint) -> Type -> m ())
-> (Type -> Type -> Constraint) -> Type -> Type -> m ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Type -> Type -> Constraint
Equality) [Type]
targs ((Expr Ann -> Type) -> [Expr Ann] -> [Type]
forall a b. (a -> b) -> [a] -> [b]
map Expr Ann -> Type
getType [Expr Ann]
args')

        Expr Ann -> m (Expr Ann)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Expr Ann -> m (Expr Ann)) -> Expr Ann -> m (Expr Ann)
forall a b. (a -> b) -> a -> b
$ Ann -> Expr Ann -> Expr Ann
forall a. a -> Expr a -> Expr a
EAnnotated (InputAnn -> Type -> Ann
Ann InputAnn
ann Type
tret) (Expr Ann -> Expr Ann) -> Expr Ann -> Expr Ann
forall a b. (a -> b) -> a -> b
$
          Text -> Maybe Type -> [Expr Ann] -> Expr Ann
forall a. Text -> Maybe Type -> [Expr a] -> Expr a
EFfi Text
f (Type -> Maybe Type
forall a. a -> Maybe a
Just Type
t) [Expr Ann]
args'

  EBlock Block InputAnn
block -> do
    (Type
t, Block Ann
block') <- Block InputAnn -> m (Type, Block Ann)
forall (b :: * -> *) (m :: * -> *).
Elaborate b m =>
Block InputAnn -> m (Type, Block Ann)
elaborateBlock Block InputAnn
block
    Expr Ann -> m (Expr Ann)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Expr Ann -> m (Expr Ann)) -> Expr Ann -> m (Expr Ann)
forall a b. (a -> b) -> a -> b
$ Ann -> Expr Ann -> Expr Ann
forall a. a -> Expr a -> Expr a
EAnnotated (InputAnn -> Type -> Ann
Ann InputAnn
ann Type
t) (Expr Ann -> Expr Ann) -> Expr Ann -> Expr Ann
forall a b. (a -> b) -> a -> b
$
      Block Ann -> Expr Ann
forall a. Block a -> Expr a
EBlock Block Ann
block'

  ELet TermDef InputAnn
termdef Expr InputAnn
expr -> do
    ElabInfo{TermDef Ann
eiResult :: TermDef Ann
eiResult :: forall a. ElabInfo a -> a
eiResult, Type
eiType :: Type
eiType :: forall a. ElabInfo a -> Type
eiType} <- TermDef InputAnn -> m (ElabInfo (TermDef Ann))
forall (b :: * -> *) (m :: * -> *).
Elaborate b m =>
TermDef InputAnn -> m (ElabInfo (TermDef Ann))
elaborateTermDef TermDef InputAnn
termdef
    Expr Ann
expr' <- [(Text, Typer)] -> m (Expr Ann) -> m (Expr Ann)
forall (b :: * -> *) (m :: * -> *) a.
Elaborate b m =>
[(Text, Typer)] -> m a -> m a
withEnv [(TermDef InputAnn -> Text
forall a. TermDef a -> Text
getTermName TermDef InputAnn
termdef, Type -> Typer
Monomorphic Type
eiType)] (m (Expr Ann) -> m (Expr Ann)) -> m (Expr Ann) -> m (Expr Ann)
forall a b. (a -> b) -> a -> b
$ InputAnn -> Expr InputAnn -> m (Expr Ann)
forall (b :: * -> *) (m :: * -> *).
Elaborate b m =>
InputAnn -> Expr InputAnn -> m (Expr Ann)
elaborateExpr InputAnn
ann Expr InputAnn
expr
    Expr Ann -> m (Expr Ann)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Expr Ann -> m (Expr Ann)) -> Expr Ann -> m (Expr Ann)
forall a b. (a -> b) -> a -> b
$ Ann -> Expr Ann -> Expr Ann
forall a. a -> Expr a -> Expr a
EAnnotated (InputAnn -> Type -> Ann
Ann InputAnn
ann (Expr Ann -> Type
getType Expr Ann
expr')) (Expr Ann -> Expr Ann) -> Expr Ann -> Expr Ann
forall a b. (a -> b) -> a -> b
$
      TermDef Ann -> Expr Ann -> Expr Ann
forall a. TermDef a -> Expr a -> Expr a
ELet TermDef Ann
eiResult Expr Ann
expr'

  -- lookup variant in the environment
  EVariant Text
constr -> do
    vs :: VariantSig InputAnn
vs@VariantSig{ Type
vsDatatype :: Type
vsDatatype :: forall a. VariantSig a -> Type
vsDatatype, Maybe Type
vsPayloadTemplate :: Maybe Type
vsPayloadTemplate :: forall a. VariantSig a -> Maybe Type
vsPayloadTemplate } <- InputAnn -> Text -> m (VariantSig InputAnn)
forall (b :: * -> *) (m :: * -> *).
Elaborate b m =>
InputAnn -> Text -> m (VariantSig InputAnn)
lookupVariant InputAnn
ann Text
constr
    (Env Text
dtvars, Type
dt) <- Text -> Type -> m (Env Text, Type)
forall (b :: * -> *) (m :: * -> *).
Solve b m =>
Text -> Type -> m (Env Text, Type)
instantiate Text
"ti" Type
vsDatatype
    let
      mspecialized :: Maybe Type
mspecialized = (Type -> Type) -> Type -> Type
forall on. Uniplate on => (on -> on) -> on -> on
U.transform
        ( \case
          TypeVar Text
t ->
            -- we already checked this
            Type -> (Text -> Type) -> Maybe Text -> Type
forall b a. b -> (a -> b) -> Maybe a -> b
maybe
              (String -> Type
forall a. HasCallStack => String -> a
error (String -> Type) -> String -> Type
forall a b. (a -> b) -> a -> b
$ Text -> String
toString (Text -> String) -> Text -> String
forall a b. (a -> b) -> a -> b
$ Text
"Found unbound type variable " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> VariantSig InputAnn -> Text
forall a. Show a => a -> Text
pShow VariantSig InputAnn
vs)
              Text -> Type
TypeVar
              (Text -> Env Text -> Maybe Text
forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup Text
t Env Text
dtvars)
          Type
t -> Type
t
        )
        (Type -> Type) -> Maybe Type -> Maybe Type
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe Type
vsPayloadTemplate

    let t :: Type
t = Type -> (Type -> Type) -> Maybe Type -> Type
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Type
dt (\Type
specialized -> [Type] -> Type -> Type
typeFun [Type
specialized] Type
dt) Maybe Type
mspecialized

    Expr Ann -> m (Expr Ann)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Expr Ann -> m (Expr Ann)) -> Expr Ann -> m (Expr Ann)
forall a b. (a -> b) -> a -> b
$ Ann -> Expr Ann -> Expr Ann
forall a. a -> Expr a -> Expr a
EAnnotated (InputAnn -> Type -> Ann
Ann InputAnn
ann Type
t) (Expr Ann -> Expr Ann) -> Expr Ann -> Expr Ann
forall a b. (a -> b) -> a -> b
$
      Text -> Expr Ann
forall a. Text -> Expr a
EVariant Text
constr

  -- An open variant has a specific type according to the constructor and value,
  -- but may be plugged in any place that can handle it.
  -- Must take exactly one value as input.
  EOpenVariant Text
constr -> do
    Text
tv <- Text -> m Text
forall (m :: * -> *). MonadState ElabState m => Text -> m Text
genTypeVar Text
"t"
    Type
t <- Text -> Type
TypeVar (Text -> Type) -> m Text -> m Type
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Text -> m Text
forall (m :: * -> *). MonadState ElabState m => Text -> m Text
genTypeVar Text
"t"
    Expr Ann -> m (Expr Ann)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Expr Ann -> m (Expr Ann)) -> Expr Ann -> m (Expr Ann)
forall a b. (a -> b) -> a -> b
$ Ann -> Expr Ann -> Expr Ann
forall a. a -> Expr a -> Expr a
EAnnotated (InputAnn -> Type -> Ann
Ann InputAnn
ann ([Type] -> Type -> Type
typeFun [Type
t] (Type -> Type) -> Type -> Type
forall a b. (a -> b) -> a -> b
$ [(Text, Type)] -> Text -> Type
TypePolyVariantLB [(Text
constr, Type
t)] Text
tv)) (Expr Ann -> Expr Ann) -> Expr Ann -> Expr Ann
forall a b. (a -> b) -> a -> b
$
      Text -> Expr Ann
forall a. Text -> Expr a
EOpenVariant Text
constr

  -- For if expressions, the condition should be of type Bool,
  -- and the two branches should match.
  EIf Expr InputAnn
cond Expr InputAnn
trueBranch Expr InputAnn
falseBranch -> do
    Expr Ann
cond' <- InputAnn -> Expr InputAnn -> m (Expr Ann)
forall (b :: * -> *) (m :: * -> *).
Elaborate b m =>
InputAnn -> Expr InputAnn -> m (Expr Ann)
elaborateExpr InputAnn
ann Expr InputAnn
cond
    Expr Ann
trueBranch' <- InputAnn -> Expr InputAnn -> m (Expr Ann)
forall (b :: * -> *) (m :: * -> *).
Elaborate b m =>
InputAnn -> Expr InputAnn -> m (Expr Ann)
elaborateExpr InputAnn
ann Expr InputAnn
trueBranch
    Expr Ann
falseBranch' <- InputAnn -> Expr InputAnn -> m (Expr Ann)
forall (b :: * -> *) (m :: * -> *).
Elaborate b m =>
InputAnn -> Expr InputAnn -> m (Expr Ann)
elaborateExpr InputAnn
ann Expr InputAnn
falseBranch
    InputAnn -> Constraint -> m ()
forall (b :: * -> *) (m :: * -> *).
Elaborate b m =>
InputAnn -> Constraint -> m ()
constrain InputAnn
ann (Constraint -> m ()) -> Constraint -> m ()
forall a b. (a -> b) -> a -> b
$ Type -> Type -> Constraint
Equality Type
tBool (Expr Ann -> Type
getType Expr Ann
cond')
    InputAnn -> Constraint -> m ()
forall (b :: * -> *) (m :: * -> *).
Elaborate b m =>
InputAnn -> Constraint -> m ()
constrain InputAnn
ann (Constraint -> m ()) -> Constraint -> m ()
forall a b. (a -> b) -> a -> b
$ Type -> Type -> Constraint
Equality (Expr Ann -> Type
getType Expr Ann
trueBranch') (Expr Ann -> Type
getType Expr Ann
falseBranch')
    Expr Ann -> m (Expr Ann)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Expr Ann -> m (Expr Ann)) -> Expr Ann -> m (Expr Ann)
forall a b. (a -> b) -> a -> b
$ Ann -> Expr Ann -> Expr Ann
forall a. a -> Expr a -> Expr a
EAnnotated (InputAnn -> Type -> Ann
Ann InputAnn
ann (Expr Ann -> Type
getType Expr Ann
trueBranch')) (Expr Ann -> Expr Ann) -> Expr Ann -> Expr Ann
forall a b. (a -> b) -> a -> b
$
      Expr Ann -> Expr Ann -> Expr Ann -> Expr Ann
forall a. Expr a -> Expr a -> Expr a -> Expr a
EIf Expr Ann
cond' Expr Ann
trueBranch' Expr Ann
falseBranch'

  ECase Expr InputAnn
expr [(Pattern, Expr InputAnn)]
patterns -> do
    Expr Ann
expr' <- InputAnn -> Expr InputAnn -> m (Expr Ann)
forall (b :: * -> *) (m :: * -> *).
Elaborate b m =>
InputAnn -> Expr InputAnn -> m (Expr Ann)
elaborateExpr InputAnn
ann Expr InputAnn
expr
    Type
patT <- Text -> Type
TypeVar (Text -> Type) -> m Text -> m Type
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Text -> m Text
forall (m :: * -> *). MonadState ElabState m => Text -> m Text
genTypeVar Text
"t"
    [(Pattern, Expr Ann)]
patterns' <- InputAnn
-> Type
-> Type
-> [(Pattern, Expr InputAnn)]
-> m [(Pattern, Expr Ann)]
forall (b :: * -> *) (m :: * -> *).
Elaborate b m =>
InputAnn
-> Type
-> Type
-> [(Pattern, Expr InputAnn)]
-> m [(Pattern, Expr Ann)]
elaboratePatterns InputAnn
ann (Expr Ann -> Type
getType Expr Ann
expr') Type
patT [(Pattern, Expr InputAnn)]
patterns
    Expr Ann -> m (Expr Ann)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Expr Ann -> m (Expr Ann)) -> Expr Ann -> m (Expr Ann)
forall a b. (a -> b) -> a -> b
$ Ann -> Expr Ann -> Expr Ann
forall a. a -> Expr a -> Expr a
EAnnotated (InputAnn -> Type -> Ann
Ann InputAnn
ann Type
patT) (Expr Ann -> Expr Ann) -> Expr Ann -> Expr Ann
forall a b. (a -> b) -> a -> b
$
      Expr Ann -> [(Pattern, Expr Ann)] -> Expr Ann
forall a. Expr a -> [(Pattern, Expr a)] -> Expr a
ECase Expr Ann
expr' [(Pattern, Expr Ann)]
patterns'

  ERecord Record (Expr InputAnn)
record -> do
    Map Text (Expr Ann)
record' <- (Expr InputAnn -> m (Expr Ann))
-> Record (Expr InputAnn) -> m (Map Text (Expr Ann))
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse (InputAnn -> Expr InputAnn -> m (Expr Ann)
forall (b :: * -> *) (m :: * -> *).
Elaborate b m =>
InputAnn -> Expr InputAnn -> m (Expr Ann)
elaborateExpr InputAnn
ann) Record (Expr InputAnn)
record
    let
      recordT :: Type
recordT = [(Text, Type)] -> Type
TypeRec ([(Text, Type)] -> Type) -> [(Text, Type)] -> Type
forall a b. (a -> b) -> a -> b
$ Env Type -> [(Text, Type)]
forall k a. Map k a -> [(k, a)]
M.toList (Env Type -> [(Text, Type)]) -> Env Type -> [(Text, Type)]
forall a b. (a -> b) -> a -> b
$ (Expr Ann -> Type) -> Map Text (Expr Ann) -> Env Type
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Expr Ann -> Type
getType Map Text (Expr Ann)
record'

    Expr Ann -> m (Expr Ann)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Expr Ann -> m (Expr Ann)) -> Expr Ann -> m (Expr Ann)
forall a b. (a -> b) -> a -> b
$ Ann -> Expr Ann -> Expr Ann
forall a. a -> Expr a -> Expr a
EAnnotated (InputAnn -> Type -> Ann
Ann InputAnn
ann Type
recordT) (Expr Ann -> Expr Ann) -> Expr Ann -> Expr Ann
forall a b. (a -> b) -> a -> b
$
      Map Text (Expr Ann) -> Expr Ann
forall a. Record (Expr a) -> Expr a
ERecord Map Text (Expr Ann)
record'

  -- the "expr" should be a record with at least the "label" label
  ERecordAccess Expr InputAnn
expr Text
label -> do
    Type
labelT <- Text -> Type
TypeVar (Text -> Type) -> m Text -> m Type
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Text -> m Text
forall (m :: * -> *). MonadState ElabState m => Text -> m Text
genTypeVar Text
"t"
    Text
ext <- Text -> m Text
forall (m :: * -> *). MonadState ElabState m => Text -> m Text
genTypeVar Text
"t"
    Expr Ann
expr' <- InputAnn -> Expr InputAnn -> m (Expr Ann)
forall (b :: * -> *) (m :: * -> *).
Elaborate b m =>
InputAnn -> Expr InputAnn -> m (Expr Ann)
elaborateExpr InputAnn
ann Expr InputAnn
expr
    InputAnn -> Constraint -> m ()
forall (b :: * -> *) (m :: * -> *).
Elaborate b m =>
InputAnn -> Constraint -> m ()
constrain InputAnn
ann (Constraint -> m ()) -> Constraint -> m ()
forall a b. (a -> b) -> a -> b
$ Type -> Type -> Constraint
Equality
      (Expr Ann -> Type
getType Expr Ann
expr')
      ([(Text, Type)] -> Text -> Type
TypeRecExt [(Text
label, Type
labelT)] Text
ext)
    Expr Ann -> m (Expr Ann)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Expr Ann -> m (Expr Ann)) -> Expr Ann -> m (Expr Ann)
forall a b. (a -> b) -> a -> b
$ Ann -> Expr Ann -> Expr Ann
forall a. a -> Expr a -> Expr a
EAnnotated (InputAnn -> Type -> Ann
Ann InputAnn
ann Type
labelT) (Expr Ann -> Expr Ann) -> Expr Ann -> Expr Ann
forall a b. (a -> b) -> a -> b
$
      Expr Ann -> Text -> Expr Ann
forall a. Expr a -> Text -> Expr a
ERecordAccess Expr Ann
expr' Text
label

  ERecordExtension Record (Expr InputAnn)
record Expr InputAnn
expr -> do
    Expr Ann
expr' <- InputAnn -> Expr InputAnn -> m (Expr Ann)
forall (b :: * -> *) (m :: * -> *).
Elaborate b m =>
InputAnn -> Expr InputAnn -> m (Expr Ann)
elaborateExpr InputAnn
ann Expr InputAnn
expr
    Map Text (Expr Ann)
record' <- (Expr InputAnn -> m (Expr Ann))
-> Record (Expr InputAnn) -> m (Map Text (Expr Ann))
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse (InputAnn -> Expr InputAnn -> m (Expr Ann)
forall (b :: * -> *) (m :: * -> *).
Elaborate b m =>
InputAnn -> Expr InputAnn -> m (Expr Ann)
elaborateExpr InputAnn
ann) Record (Expr InputAnn)
record
    Text
et <- Text -> m Text
forall (m :: * -> *). MonadState ElabState m => Text -> m Text
genTypeVar Text
"t"
    InputAnn -> Constraint -> m ()
forall (b :: * -> *) (m :: * -> *).
Elaborate b m =>
InputAnn -> Constraint -> m ()
constrain InputAnn
ann (Constraint -> m ()) -> Constraint -> m ()
forall a b. (a -> b) -> a -> b
$ Type -> Type -> Constraint
Equality ([(Text, Type)] -> Text -> Type
TypeRecExt [] Text
et) (Expr Ann -> Type
getType Expr Ann
expr')
    let
      recordTypes :: [(Text, Type)]
recordTypes = Env Type -> [(Text, Type)]
forall k a. Map k a -> [(k, a)]
M.toList (Env Type -> [(Text, Type)]) -> Env Type -> [(Text, Type)]
forall a b. (a -> b) -> a -> b
$ (Expr Ann -> Type) -> Map Text (Expr Ann) -> Env Type
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Expr Ann -> Type
getType Map Text (Expr Ann)
record'
      t :: Type
t = [(Text, Type)] -> Text -> Type
TypeRecExt [(Text, Type)]
recordTypes Text
et
    Expr Ann -> m (Expr Ann)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Expr Ann -> m (Expr Ann)) -> Expr Ann -> m (Expr Ann)
forall a b. (a -> b) -> a -> b
$ Ann -> Expr Ann -> Expr Ann
forall a. a -> Expr a -> Expr a
EAnnotated (InputAnn -> Type -> Ann
Ann InputAnn
ann Type
t) (Expr Ann -> Expr Ann) -> Expr Ann -> Expr Ann
forall a b. (a -> b) -> a -> b
$
      Map Text (Expr Ann) -> Expr Ann -> Expr Ann
forall a. Record (Expr a) -> Expr a -> Expr a
ERecordExtension Map Text (Expr Ann)
record' Expr Ann
expr'

-- | Elaborate patterns in case expressions
elaboratePatterns
  :: Elaborate b m
  => InputAnn -> Type -> Type -> [(Pattern, Expr InputAnn)] -> m [(Pattern, Expr Ann)]
elaboratePatterns :: InputAnn
-> Type
-> Type
-> [(Pattern, Expr InputAnn)]
-> m [(Pattern, Expr Ann)]
elaboratePatterns InputAnn
ann Type
exprT Type
bodyT [(Pattern, Expr InputAnn)]
pats = do
  Text
exprTV <- Text -> m Text
forall (m :: * -> *). MonadState ElabState m => Text -> m Text
genTypeVar Text
"t"
  InputAnn -> Constraint -> m ()
forall (b :: * -> *) (m :: * -> *).
Elaborate b m =>
InputAnn -> Constraint -> m ()
constrain InputAnn
ann (Constraint -> m ()) -> Constraint -> m ()
forall a b. (a -> b) -> a -> b
$ Type -> Type -> Constraint
Equality Type
exprT (Text -> Type
TypeVar Text
exprTV)
  [(Pattern, Expr InputAnn)]
-> ((Pattern, Expr InputAnn) -> m (Pattern, Expr Ann))
-> m [(Pattern, Expr Ann)]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
t a -> (a -> f b) -> f (t b)
for [(Pattern, Expr InputAnn)]
pats (((Pattern, Expr InputAnn) -> m (Pattern, Expr Ann))
 -> m [(Pattern, Expr Ann)])
-> ((Pattern, Expr InputAnn) -> m (Pattern, Expr Ann))
-> m [(Pattern, Expr Ann)]
forall a b. (a -> b) -> a -> b
$ \(Pattern
pat, Expr InputAnn
body) -> do
    [(Text, Typer)]
env <- InputAnn -> Text -> Pattern -> m [(Text, Typer)]
forall (b :: * -> *) (m :: * -> *).
Elaborate b m =>
InputAnn -> Text -> Pattern -> m [(Text, Typer)]
elaboratePattern InputAnn
ann Text
exprTV Pattern
pat
    Expr Ann
body' <- [(Text, Typer)] -> m (Expr Ann) -> m (Expr Ann)
forall (b :: * -> *) (m :: * -> *) a.
Elaborate b m =>
[(Text, Typer)] -> m a -> m a
withEnv [(Text, Typer)]
env (m (Expr Ann) -> m (Expr Ann)) -> m (Expr Ann) -> m (Expr Ann)
forall a b. (a -> b) -> a -> b
$ InputAnn -> Expr InputAnn -> m (Expr Ann)
forall (b :: * -> *) (m :: * -> *).
Elaborate b m =>
InputAnn -> Expr InputAnn -> m (Expr Ann)
elaborateExpr InputAnn
ann Expr InputAnn
body
    let t :: Type
t = Expr Ann -> Type
getType Expr Ann
body'
    InputAnn -> Constraint -> m ()
forall (b :: * -> *) (m :: * -> *).
Elaborate b m =>
InputAnn -> Constraint -> m ()
constrain InputAnn
ann (Constraint -> m ()) -> Constraint -> m ()
forall a b. (a -> b) -> a -> b
$ Type -> Type -> Constraint
Equality Type
bodyT Type
t
    (Pattern, Expr Ann) -> m (Pattern, Expr Ann)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Pattern
pat, Expr Ann
body')
  

-- | Elaborate a single pattern match
elaboratePattern
  :: Elaborate b m
  => InputAnn -> TypeVar -> Pattern -> m [(Var, Typer)]
elaboratePattern :: InputAnn -> Text -> Pattern -> m [(Text, Typer)]
elaboratePattern InputAnn
ann Text
exprTV Pattern
outerPat = do
  case Pattern
outerPat of
    Pattern
PWildcard -> do
      Text
tv <- Text -> m Text
forall (m :: * -> *). MonadState ElabState m => Text -> m Text
genTypeVar Text
"t"
      InputAnn -> Constraint -> m ()
forall (b :: * -> *) (m :: * -> *).
Elaborate b m =>
InputAnn -> Constraint -> m ()
constrain InputAnn
ann (Constraint -> m ()) -> Constraint -> m ()
forall a b. (a -> b) -> a -> b
$ Type -> Type -> Constraint
Equality
        (Text -> Type
TypeVar Text
exprTV)
        ([(Text, Type)] -> Text -> Type
TypePolyVariantLB [] Text
tv)
      [(Text, Typer)] -> m [(Text, Typer)]
forall (f :: * -> *) a. Applicative f => a -> f a
pure [(Text, Typer)]
forall a. Monoid a => a
mempty

    -- variable capture does different things depending if it matches with variants
    -- or other types.
    -- For variants, it matches any variant, but for the specified variants it must
    -- match their type.
    -- Otherwise it will match the expression type.
    PVar Text
v -> do
      Text
tv <- Text -> m Text
forall (m :: * -> *). MonadState ElabState m => Text -> m Text
genTypeVar Text
"t"
      InputAnn -> Constraint -> m ()
forall (b :: * -> *) (m :: * -> *).
Elaborate b m =>
InputAnn -> Constraint -> m ()
constrain InputAnn
ann (Constraint -> m ()) -> Constraint -> m ()
forall a b. (a -> b) -> a -> b
$ Type -> Type -> Constraint
Equality
        (Text -> Type
TypeVar Text
exprTV)
        ([(Text, Type)] -> Text -> Type
TypePolyVariantLB [] Text
tv)
      [(Text, Typer)] -> m [(Text, Typer)]
forall (f :: * -> *) a. Applicative f => a -> f a
pure [(Text
v, Type -> Typer
Monomorphic (Type -> Typer) -> Type -> Typer
forall a b. (a -> b) -> a -> b
$ Text -> Type
TypeVar Text
exprTV)]

    PLit Lit
lit -> do
      InputAnn -> Constraint -> m ()
forall (b :: * -> *) (m :: * -> *).
Elaborate b m =>
InputAnn -> Constraint -> m ()
constrain InputAnn
ann (Constraint -> m ()) -> Constraint -> m ()
forall a b. (a -> b) -> a -> b
$ Type -> Type -> Constraint
Equality (Lit -> Type
getLitType Lit
lit) (Text -> Type
TypeVar Text
exprTV)
      [(Text, Typer)] -> m [(Text, Typer)]
forall (f :: * -> *) a. Applicative f => a -> f a
pure [(Text, Typer)]
forall a. Monoid a => a
mempty

    -- open variants constrain the type of expr to be able to handle their variant
    POpenVariant (Variant Text
constr Pattern
innerPat) -> do
      Text
innerPatT <- Text -> m Text
forall (m :: * -> *). MonadState ElabState m => Text -> m Text
genTypeVar Text
"t"
      InputAnn -> Constraint -> m ()
forall (b :: * -> *) (m :: * -> *).
Elaborate b m =>
InputAnn -> Constraint -> m ()
constrain InputAnn
ann (Constraint -> m ()) -> Constraint -> m ()
forall a b. (a -> b) -> a -> b
$ Type -> Type -> Constraint
Equality
        (Text -> Type
TypeVar Text
exprTV)
        (Text -> [(Text, Type)] -> Type
TypePolyVariantUB Text
exprTV [(Text
constr, Text -> Type
TypeVar Text
innerPatT)])
      InputAnn -> Text -> Pattern -> m [(Text, Typer)]
forall (b :: * -> *) (m :: * -> *).
Elaborate b m =>
InputAnn -> Text -> Pattern -> m [(Text, Typer)]
elaboratePattern InputAnn
ann Text
innerPatT Pattern
innerPat

    PVariant (Variant Text
constr Maybe Pattern
minnerPat) -> do
      vs :: VariantSig InputAnn
vs@VariantSig{ Type
vsDatatype :: Type
vsDatatype :: forall a. VariantSig a -> Type
vsDatatype, Maybe Type
vsPayloadTemplate :: Maybe Type
vsPayloadTemplate :: forall a. VariantSig a -> Maybe Type
vsPayloadTemplate } <- InputAnn -> Text -> m (VariantSig InputAnn)
forall (b :: * -> *) (m :: * -> *).
Elaborate b m =>
InputAnn -> Text -> m (VariantSig InputAnn)
lookupVariant InputAnn
ann Text
constr
      (Env Text
dtvars, Type
dt) <- Text -> Type -> m (Env Text, Type)
forall (b :: * -> *) (m :: * -> *).
Solve b m =>
Text -> Type -> m (Env Text, Type)
instantiate Text
"ti" Type
vsDatatype
      let
        minnerPatT :: Maybe Type
minnerPatT = (Type -> Type) -> Type -> Type
forall on. Uniplate on => (on -> on) -> on -> on
U.transform
          ( \case
            TypeVar Text
t ->
              -- we already checked this
              Type -> (Text -> Type) -> Maybe Text -> Type
forall b a. b -> (a -> b) -> Maybe a -> b
maybe
                (String -> Type
forall a. HasCallStack => String -> a
error (String -> Type) -> String -> Type
forall a b. (a -> b) -> a -> b
$ Text -> String
toString (Text -> String) -> Text -> String
forall a b. (a -> b) -> a -> b
$ Text
"Found unbound type variable " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> VariantSig InputAnn -> Text
forall a. Show a => a -> Text
pShow VariantSig InputAnn
vs)
                Text -> Type
TypeVar
                (Text -> Env Text -> Maybe Text
forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup Text
t Env Text
dtvars)
            Type
t -> Type
t
          )
          (Type -> Type) -> Maybe Type -> Maybe Type
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe Type
vsPayloadTemplate

      InputAnn -> Constraint -> m ()
forall (b :: * -> *) (m :: * -> *).
Elaborate b m =>
InputAnn -> Constraint -> m ()
constrain InputAnn
ann (Constraint -> m ()) -> Constraint -> m ()
forall a b. (a -> b) -> a -> b
$ Type -> Type -> Constraint
Equality (Text -> Type
TypeVar Text
exprTV) Type
dt
      Maybe [(Text, Typer)]
mpayload <- case (Maybe Type
minnerPatT, Maybe Pattern
minnerPat) of
        (Maybe Type
Nothing, Maybe Pattern
Nothing) ->
          Maybe [(Text, Typer)] -> m (Maybe [(Text, Typer)])
forall (f :: * -> *) a. Applicative f => a -> f a
pure Maybe [(Text, Typer)]
forall a. Maybe a
Nothing
        (Just Type
innerPatT, Just Pattern
innerPat) -> do
          Text
tv <- Text -> m Text
forall (m :: * -> *). MonadState ElabState m => Text -> m Text
genTypeVar Text
"t"
          InputAnn -> Constraint -> m ()
forall (b :: * -> *) (m :: * -> *).
Elaborate b m =>
InputAnn -> Constraint -> m ()
constrain InputAnn
ann (Constraint -> m ()) -> Constraint -> m ()
forall a b. (a -> b) -> a -> b
$ Type -> Type -> Constraint
Equality Type
innerPatT (Text -> Type
TypeVar Text
tv)
          [(Text, Typer)] -> Maybe [(Text, Typer)]
forall a. a -> Maybe a
Just ([(Text, Typer)] -> Maybe [(Text, Typer)])
-> m [(Text, Typer)] -> m (Maybe [(Text, Typer)])
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> InputAnn -> Text -> Pattern -> m [(Text, Typer)]
forall (b :: * -> *) (m :: * -> *).
Elaborate b m =>
InputAnn -> Text -> Pattern -> m [(Text, Typer)]
elaboratePattern InputAnn
ann Text
tv Pattern
innerPat
        (Maybe Type, Maybe Pattern)
_ ->
          [InputAnn] -> TypeError -> m (Maybe [(Text, Typer)])
forall (m :: * -> *) a.
MonadError TypeErrorA m =>
[InputAnn] -> TypeError -> m a
throwErr [InputAnn
ann] (TypeError -> m (Maybe [(Text, Typer)]))
-> TypeError -> m (Maybe [(Text, Typer)])
forall a b. (a -> b) -> a -> b
$ Type -> Type -> TypeError
ArityMismatch
            Type
vsDatatype
            ([Type] -> Type -> Type
typeFun [Type -> Maybe Type -> Type
forall a. a -> Maybe a -> a
fromMaybe (Text -> Type
TypeVar Text
"t") Maybe Type
minnerPatT] Type
vsDatatype)
      [(Text, Typer)] -> m [(Text, Typer)]
forall (f :: * -> *) a. Applicative f => a -> f a
pure ([(Text, Typer)] -> m [(Text, Typer)])
-> [(Text, Typer)] -> m [(Text, Typer)]
forall a b. (a -> b) -> a -> b
$ [(Text, Typer)] -> Maybe [(Text, Typer)] -> [(Text, Typer)]
forall a. a -> Maybe a -> a
fromMaybe [(Text, Typer)]
forall a. Monoid a => a
mempty Maybe [(Text, Typer)]
mpayload

    PRecord Record Pattern
record -> do
      Map Text (Type, [(Text, Typer)])
record' <- Record Pattern
-> (Pattern -> m (Type, [(Text, Typer)]))
-> m (Map Text (Type, [(Text, Typer)]))
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
t a -> (a -> f b) -> f (t b)
for Record Pattern
record ((Pattern -> m (Type, [(Text, Typer)]))
 -> m (Map Text (Type, [(Text, Typer)])))
-> (Pattern -> m (Type, [(Text, Typer)]))
-> m (Map Text (Type, [(Text, Typer)]))
forall a b. (a -> b) -> a -> b
$ \Pattern
pat -> do
        Text
t <- Text -> m Text
forall (m :: * -> *). MonadState ElabState m => Text -> m Text
genTypeVar Text
"t"
        (,) (Text -> Type
TypeVar Text
t) ([(Text, Typer)] -> (Type, [(Text, Typer)]))
-> m [(Text, Typer)] -> m (Type, [(Text, Typer)])
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> InputAnn -> Text -> Pattern -> m [(Text, Typer)]
forall (b :: * -> *) (m :: * -> *).
Elaborate b m =>
InputAnn -> Text -> Pattern -> m [(Text, Typer)]
elaboratePattern InputAnn
ann Text
t Pattern
pat

      Text
ext <- Text -> m Text
forall (m :: * -> *). MonadState ElabState m => Text -> m Text
genTypeVar Text
"t"
      InputAnn -> Constraint -> m ()
forall (b :: * -> *) (m :: * -> *).
Elaborate b m =>
InputAnn -> Constraint -> m ()
constrain InputAnn
ann (Constraint -> m ()) -> Constraint -> m ()
forall a b. (a -> b) -> a -> b
$ Type -> Type -> Constraint
Equality
        (Text -> Type
TypeVar Text
exprTV)
        ([(Text, Type)] -> Text -> Type
TypeRecExt (Env Type -> [(Text, Type)]
forall k a. Map k a -> [(k, a)]
M.toList (Env Type -> [(Text, Type)]) -> Env Type -> [(Text, Type)]
forall a b. (a -> b) -> a -> b
$ ((Type, [(Text, Typer)]) -> Type)
-> Map Text (Type, [(Text, Typer)]) -> Env Type
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Type, [(Text, Typer)]) -> Type
forall a b. (a, b) -> a
fst Map Text (Type, [(Text, Typer)])
record') Text
ext)

      -- check if we have duplicate names in the environment
      let
        envs :: [Env Typer]
envs = ((Type, [(Text, Typer)]) -> Env Typer)
-> [(Type, [(Text, Typer)])] -> [Env Typer]
forall a b. (a -> b) -> [a] -> [b]
map ([(Text, Typer)] -> Env Typer
forall k a. Ord k => [(k, a)] -> Map k a
M.fromList ([(Text, Typer)] -> Env Typer)
-> ((Type, [(Text, Typer)]) -> [(Text, Typer)])
-> (Type, [(Text, Typer)])
-> Env Typer
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Type, [(Text, Typer)]) -> [(Text, Typer)]
forall a b. (a, b) -> b
snd) ([(Type, [(Text, Typer)])] -> [Env Typer])
-> [(Type, [(Text, Typer)])] -> [Env Typer]
forall a b. (a -> b) -> a -> b
$ Map Text (Type, [(Text, Typer)]) -> [(Type, [(Text, Typer)])]
forall k a. Map k a -> [a]
M.elems Map Text (Type, [(Text, Typer)])
record'
        env :: Env Typer
env = [Env Typer] -> Env Typer
forall (f :: * -> *) k a.
(Foldable f, Ord k) =>
f (Map k a) -> Map k a
M.unions ([Env Typer] -> Env Typer) -> [Env Typer] -> Env Typer
forall a b. (a -> b) -> a -> b
$ ((Type, [(Text, Typer)]) -> Env Typer)
-> [(Type, [(Text, Typer)])] -> [Env Typer]
forall a b. (a -> b) -> [a] -> [b]
map ([(Text, Typer)] -> Env Typer
forall k a. Ord k => [(k, a)] -> Map k a
M.fromList ([(Text, Typer)] -> Env Typer)
-> ((Type, [(Text, Typer)]) -> [(Text, Typer)])
-> (Type, [(Text, Typer)])
-> Env Typer
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Type, [(Text, Typer)]) -> [(Text, Typer)]
forall a b. (a, b) -> b
snd) ([(Type, [(Text, Typer)])] -> [Env Typer])
-> [(Type, [(Text, Typer)])] -> [Env Typer]
forall a b. (a -> b) -> a -> b
$ Map Text (Type, [(Text, Typer)]) -> [(Type, [(Text, Typer)])]
forall k a. Map k a -> [a]
M.elems Map Text (Type, [(Text, Typer)])
record'
      
      Bool -> m () -> m ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless ([Int] -> Int
forall (t :: * -> *) a. (Foldable t, Num a) => t a -> a
sum ((Env Typer -> Int) -> [Env Typer] -> [Int]
forall a b. (a -> b) -> [a] -> [b]
map Env Typer -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Env Typer]
envs) Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Env Typer -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length Env Typer
env) (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$ do
        [InputAnn] -> TypeError -> m ()
forall (m :: * -> *) a.
MonadError TypeErrorA m =>
[InputAnn] -> TypeError -> m a
throwErr [InputAnn
ann] (TypeError -> m ()) -> TypeError -> m ()
forall a b. (a -> b) -> a -> b
$ Pattern -> TypeError
DuplicateVarsInPattern Pattern
outerPat
      [(Text, Typer)] -> m [(Text, Typer)]
forall (f :: * -> *) a. Applicative f => a -> f a
pure ([(Text, Typer)] -> m [(Text, Typer)])
-> [(Text, Typer)] -> m [(Text, Typer)]
forall a b. (a -> b) -> a -> b
$ Env Typer -> [(Text, Typer)]
forall k a. Map k a -> [(k, a)]
M.toList Env Typer
env

-- | The type of a literal
getLitType :: Lit -> Type
getLitType :: Lit -> Type
getLitType = \case
  LInt{} -> Type
tInt
  LString{} -> Type
tString
  LFloat{} -> Type
tFloat

----------------------------------------

-- * Solve constraints

{- |
In this phase we go over the constraints one by one and try to __unify__ them.

For example, if we see @Equality (TypeVar "t1") (TypeCon "Int")@, we create
a mapping from @t1@ to @Int@ (called a __substitution__) and
we go over the rest of the constraints and replace @t1@ with @Int@ (__apply the substitution__).

We also keep all the substitutions we created from the constraints (and merge them to one substitution
but applying new substitution to the accumulated substitution).

If we see @Equality (TypeCon "Int") (TypeCon "String")@, we throw a type error,
because the two types do not match.

We keep going until there are no more constraints or until we encountered an error.

The result of the algorithm is the accumulated substitution.

-}

solve
  :: MonadBase b b
  => LogAction b LogMsg -> Int -> Constraints -> ExceptT TypeErrorA b (Substitution, Int)
solve :: LogAction b LogMsg
-> Int
-> Set ConstraintA
-> ExceptT TypeErrorA b (Map Text (InputAnn, Type), Int)
solve = LogAction b LogMsg
-> Int
-> Set ConstraintA
-> ExceptT TypeErrorA b (Map Text (InputAnn, Type), Int)
forall (b :: * -> *).
MonadBase b b =>
LogAction b LogMsg
-> Int
-> Set ConstraintA
-> ExceptT TypeErrorA b (Map Text (InputAnn, Type), Int)
runSolve

-- ** Types

-- | Monadic capabilities for the Solve algorithm
type Solve b m
  = ( MonadBase b m
    , MonadError TypeErrorA m
    , MonadState ElabState m -- We highjack the ElabState type for the genTypeVar function.
    , MonadReader (ElabEnv b) m
    )

-- ** Algorithm

runSolve
  :: MonadBase b b
  => LogAction b LogMsg -> Int -> Constraints -> ExceptT TypeErrorA b (Substitution, Int)
runSolve :: LogAction b LogMsg
-> Int
-> Set ConstraintA
-> ExceptT TypeErrorA b (Map Text (InputAnn, Type), Int)
runSolve LogAction b LogMsg
logact Int
seed =
  ( ((Map Text (InputAnn, Type), ElabState)
 -> (Map Text (InputAnn, Type), Int))
-> ExceptT TypeErrorA b (Map Text (InputAnn, Type), ElabState)
-> ExceptT TypeErrorA b (Map Text (InputAnn, Type), Int)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((ElabState -> Int)
-> (Map Text (InputAnn, Type), ElabState)
-> (Map Text (InputAnn, Type), Int)
forall (p :: * -> * -> *) b c a.
Bifunctor p =>
(b -> c) -> p a b -> p a c
second ElabState -> Int
esTypeVarCounter)
  (ExceptT TypeErrorA b (Map Text (InputAnn, Type), ElabState)
 -> ExceptT TypeErrorA b (Map Text (InputAnn, Type), Int))
-> (Set ConstraintA
    -> ExceptT TypeErrorA b (Map Text (InputAnn, Type), ElabState))
-> Set ConstraintA
-> ExceptT TypeErrorA b (Map Text (InputAnn, Type), Int)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (StateT
   ElabState (ExceptT TypeErrorA b) (Map Text (InputAnn, Type))
 -> ElabState
 -> ExceptT TypeErrorA b (Map Text (InputAnn, Type), ElabState))
-> ElabState
-> StateT
     ElabState (ExceptT TypeErrorA b) (Map Text (InputAnn, Type))
-> ExceptT TypeErrorA b (Map Text (InputAnn, Type), ElabState)
forall a b c. (a -> b -> c) -> b -> a -> c
flip StateT ElabState (ExceptT TypeErrorA b) (Map Text (InputAnn, Type))
-> ElabState
-> ExceptT TypeErrorA b (Map Text (InputAnn, Type), ElabState)
forall s (m :: * -> *) a. StateT s m a -> s -> m (a, s)
runStateT (Int -> [Set ConstraintA] -> VariantEnv InputAnn -> ElabState
ElabState Int
seed [Set ConstraintA]
forall a. Monoid a => a
mempty VariantEnv InputAnn
forall a. Monoid a => a
mempty)
  (StateT
   ElabState (ExceptT TypeErrorA b) (Map Text (InputAnn, Type))
 -> ExceptT TypeErrorA b (Map Text (InputAnn, Type), ElabState))
-> (Set ConstraintA
    -> StateT
         ElabState (ExceptT TypeErrorA b) (Map Text (InputAnn, Type)))
-> Set ConstraintA
-> ExceptT TypeErrorA b (Map Text (InputAnn, Type), ElabState)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (ReaderT
   (ElabEnv b)
   (StateT ElabState (ExceptT TypeErrorA b))
   (Map Text (InputAnn, Type))
 -> ElabEnv b
 -> StateT
      ElabState (ExceptT TypeErrorA b) (Map Text (InputAnn, Type)))
-> ElabEnv b
-> ReaderT
     (ElabEnv b)
     (StateT ElabState (ExceptT TypeErrorA b))
     (Map Text (InputAnn, Type))
-> StateT
     ElabState (ExceptT TypeErrorA b) (Map Text (InputAnn, Type))
forall a b c. (a -> b -> c) -> b -> a -> c
flip ReaderT
  (ElabEnv b)
  (StateT ElabState (ExceptT TypeErrorA b))
  (Map Text (InputAnn, Type))
-> ElabEnv b
-> StateT
     ElabState (ExceptT TypeErrorA b) (Map Text (InputAnn, Type))
forall r (m :: * -> *) a. ReaderT r m a -> r -> m a
runReaderT (Env Typer -> Env Type -> LogAction b LogMsg -> ElabEnv b
forall (b :: * -> *).
Env Typer -> Env Type -> LogAction b LogMsg -> ElabEnv b
ElabEnv Env Typer
forall a. Monoid a => a
mempty Env Type
forall a. Monoid a => a
mempty LogAction b LogMsg
logact)
  (ReaderT
   (ElabEnv b)
   (StateT ElabState (ExceptT TypeErrorA b))
   (Map Text (InputAnn, Type))
 -> StateT
      ElabState (ExceptT TypeErrorA b) (Map Text (InputAnn, Type)))
-> (Set ConstraintA
    -> ReaderT
         (ElabEnv b)
         (StateT ElabState (ExceptT TypeErrorA b))
         (Map Text (InputAnn, Type)))
-> Set ConstraintA
-> StateT
     ElabState (ExceptT TypeErrorA b) (Map Text (InputAnn, Type))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ( \[ConstraintA]
cs -> do
      Text
-> ReaderT (ElabEnv b) (StateT ElabState (ExceptT TypeErrorA b)) ()
forall env (b :: * -> *) (m :: * -> *).
HasLog' LogMsg env b m =>
Text -> m ()
logDetailed (Text
"Solving constraints: " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> [ConstraintA] -> Text
forall (f :: * -> *).
(Show (f Text), Functor f) =>
f ConstraintA -> Text
ppShowCAs [ConstraintA]
cs)
      Map Text (InputAnn, Type)
-> [ConstraintA]
-> ReaderT
     (ElabEnv b)
     (StateT ElabState (ExceptT TypeErrorA b))
     (Map Text (InputAnn, Type))
forall (b :: * -> *) (m :: * -> *).
Solve b m =>
Map Text (InputAnn, Type)
-> [ConstraintA] -> m (Map Text (InputAnn, Type))
solveConstraints Map Text (InputAnn, Type)
forall a. Monoid a => a
mempty [ConstraintA]
cs
    )
  ([ConstraintA]
 -> ReaderT
      (ElabEnv b)
      (StateT ElabState (ExceptT TypeErrorA b))
      (Map Text (InputAnn, Type)))
-> (Set ConstraintA -> [ConstraintA])
-> Set ConstraintA
-> ReaderT
     (ElabEnv b)
     (StateT ElabState (ExceptT TypeErrorA b))
     (Map Text (InputAnn, Type))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Set ConstraintA -> [ConstraintA]
forall a. Set a -> [a]
S.toList
  )

-- | Recursively the constraints in order, passing the accumulated substitution.
solveConstraints :: Solve b m => Substitution -> [ConstraintA] -> m Substitution
solveConstraints :: Map Text (InputAnn, Type)
-> [ConstraintA] -> m (Map Text (InputAnn, Type))
solveConstraints Map Text (InputAnn, Type)
sub = \case
  [] -> Map Text (InputAnn, Type) -> m (Map Text (InputAnn, Type))
forall (f :: * -> *) a. Applicative f => a -> f a
pure Map Text (InputAnn, Type)
sub
  ConstraintA
c : [ConstraintA]
cs -> do
    ([ConstraintA]
newCons, Map Text (InputAnn, Type)
newSub) <- ConstraintA -> m ([ConstraintA], Map Text (InputAnn, Type))
forall (b :: * -> *) (m :: * -> *).
Solve b m =>
ConstraintA -> m ([ConstraintA], Map Text (InputAnn, Type))
solveConstraint ConstraintA
c
    -- apply the new substitution on the rest of the constraints
    [ConstraintA]
cs' <- Map Text (InputAnn, Type) -> [ConstraintA] -> m [ConstraintA]
forall (m :: * -> *).
Substitute m =>
Map Text (InputAnn, Type) -> [ConstraintA] -> m [ConstraintA]
substituteConstraints Map Text (InputAnn, Type)
newSub ([ConstraintA]
newCons [ConstraintA] -> [ConstraintA] -> [ConstraintA]
forall a. Semigroup a => a -> a -> a
<> [ConstraintA]
cs)
    -- apply the new substitution to the accumulative substitution
    Map Text (InputAnn, Type)
sub' <- Map Text (InputAnn, Type)
-> Map Text (InputAnn, Type) -> m (Map Text (InputAnn, Type))
forall (m :: * -> *).
Substitute m =>
Map Text (InputAnn, Type)
-> Map Text (InputAnn, Type) -> m (Map Text (InputAnn, Type))
substituteSubs Map Text (InputAnn, Type)
newSub Map Text (InputAnn, Type)
sub
    Map Text (InputAnn, Type)
-> [ConstraintA] -> m (Map Text (InputAnn, Type))
forall (b :: * -> *) (m :: * -> *).
Solve b m =>
Map Text (InputAnn, Type)
-> [ConstraintA] -> m (Map Text (InputAnn, Type))
solveConstraints (Map Text (InputAnn, Type)
-> Map Text (InputAnn, Type) -> Map Text (InputAnn, Type)
forall k a. Ord k => Map k a -> Map k a -> Map k a
M.union Map Text (InputAnn, Type)
newSub Map Text (InputAnn, Type)
sub') [ConstraintA]
cs'

-- | Solve a constraint.
--   Returns new constraints that may arise from this constraint and a substitution
solveConstraint :: Solve b m => ConstraintA -> m ([ConstraintA], Substitution)
solveConstraint :: ConstraintA -> m ([ConstraintA], Map Text (InputAnn, Type))
solveConstraint (Constraint
constraint, InputAnn
ann) = do
  Text -> m ()
forall env (b :: * -> *) (m :: * -> *).
HasLog' LogMsg env b m =>
Text -> m ()
logDetailed (Text
"constraint: " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Constraint -> Text
ppShowC Constraint
constraint)
  case Constraint
constraint of
    -- For let polymorphism. Instantiate a type.
    -- See the comment on @instantiate@ for more information.
    InstanceOf Type
t1 Type
t2 -> do
      (Env Text
_, Type
t2') <- Text -> Type -> m (Env Text, Type)
forall (b :: * -> *) (m :: * -> *).
Solve b m =>
Text -> Type -> m (Env Text, Type)
instantiate Text
"ti" Type
t2
      ([ConstraintA], Map Text (InputAnn, Type))
-> m ([ConstraintA], Map Text (InputAnn, Type))
forall (f :: * -> *) a. Applicative f => a -> f a
pure ([(Type -> Type -> Constraint
Equality Type
t1 Type
t2', InputAnn
ann)], Map Text (InputAnn, Type)
forall a. Monoid a => a
mempty)

    -- When the two types are equals, there's nothing to do.
    Equality Type
t1 Type
t2
      | Type
t1 Type -> Type -> Bool
forall a. Eq a => a -> a -> Bool
== Type
t2 ->
        ([ConstraintA], Map Text (InputAnn, Type))
-> m ([ConstraintA], Map Text (InputAnn, Type))
forall (f :: * -> *) a. Applicative f => a -> f a
pure ([ConstraintA]
forall a. Monoid a => a
mempty, Map Text (InputAnn, Type)
forall a. Monoid a => a
mempty)

    Equality (TypeApp Type
f1 Type
a1) (TypeApp Type
f2 Type
a2) ->
      ([ConstraintA], Map Text (InputAnn, Type))
-> m ([ConstraintA], Map Text (InputAnn, Type))
forall (f :: * -> *) a. Applicative f => a -> f a
pure
        ( (Constraint -> ConstraintA) -> [Constraint] -> [ConstraintA]
forall a b. (a -> b) -> [a] -> [b]
map ((Constraint -> InputAnn -> ConstraintA)
-> InputAnn -> Constraint -> ConstraintA
forall a b c. (a -> b -> c) -> b -> a -> c
flip (,) InputAnn
ann) ([Constraint] -> [ConstraintA]) -> [Constraint] -> [ConstraintA]
forall a b. (a -> b) -> a -> b
$ [Type -> Type -> Constraint
Equality Type
f1 Type
f2, Type -> Type -> Constraint
Equality Type
a1 Type
a2]
        , Map Text (InputAnn, Type)
forall a. Monoid a => a
mempty
        )

    -- all record labels and type should match
    Equality t1 :: Type
t1@(TypeRec ([(Text, Type)] -> Env Type
forall k a. Ord k => [(k, a)] -> Map k a
M.fromList -> Env Type
rec1)) t2 :: Type
t2@(TypeRec ([(Text, Type)] -> Env Type
forall k a. Ord k => [(k, a)] -> Map k a
M.fromList -> Env Type
rec2)) -> do
      let
        ([Text]
lefts, [Text]
rights, [Constraint]
matches) =
          [Matches Text Constraint] -> ([Text], [Text], [Constraint])
forall a b. [Matches a b] -> ([a], [a], [b])
unzipMatches ([Matches Text Constraint] -> ([Text], [Text], [Constraint]))
-> [Matches Text Constraint] -> ([Text], [Text], [Constraint])
forall a b. (a -> b) -> a -> b
$ Map Text (Matches Text Constraint) -> [Matches Text Constraint]
forall k a. Map k a -> [a]
M.elems (Map Text (Matches Text Constraint) -> [Matches Text Constraint])
-> Map Text (Matches Text Constraint) -> [Matches Text Constraint]
forall a b. (a -> b) -> a -> b
$ SimpleWhenMissing Text Type (Matches Text Constraint)
-> SimpleWhenMissing Text Type (Matches Text Constraint)
-> SimpleWhenMatched Text Type Type (Matches Text Constraint)
-> Env Type
-> Env Type
-> Map Text (Matches Text Constraint)
forall k a c b.
Ord k =>
SimpleWhenMissing k a c
-> SimpleWhenMissing k b c
-> SimpleWhenMatched k a b c
-> Map k a
-> Map k b
-> Map k c
M.merge
            ((Text -> Type -> Matches Text Constraint)
-> SimpleWhenMissing Text Type (Matches Text Constraint)
forall (f :: * -> *) k x y.
Applicative f =>
(k -> x -> y) -> WhenMissing f k x y
M.mapMissing ((Text -> Type -> Matches Text Constraint)
 -> SimpleWhenMissing Text Type (Matches Text Constraint))
-> (Text -> Type -> Matches Text Constraint)
-> SimpleWhenMissing Text Type (Matches Text Constraint)
forall a b. (a -> b) -> a -> b
$ Matches Text Constraint -> Type -> Matches Text Constraint
forall a b. a -> b -> a
const (Matches Text Constraint -> Type -> Matches Text Constraint)
-> (Text -> Matches Text Constraint)
-> Text
-> Type
-> Matches Text Constraint
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Text -> Matches Text Constraint
forall a b. a -> Matches a b
OnlyLeft)
            ((Text -> Type -> Matches Text Constraint)
-> SimpleWhenMissing Text Type (Matches Text Constraint)
forall (f :: * -> *) k x y.
Applicative f =>
(k -> x -> y) -> WhenMissing f k x y
M.mapMissing ((Text -> Type -> Matches Text Constraint)
 -> SimpleWhenMissing Text Type (Matches Text Constraint))
-> (Text -> Type -> Matches Text Constraint)
-> SimpleWhenMissing Text Type (Matches Text Constraint)
forall a b. (a -> b) -> a -> b
$ Matches Text Constraint -> Type -> Matches Text Constraint
forall a b. a -> b -> a
const (Matches Text Constraint -> Type -> Matches Text Constraint)
-> (Text -> Matches Text Constraint)
-> Text
-> Type
-> Matches Text Constraint
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Text -> Matches Text Constraint
forall a b. a -> Matches a b
OnlyRight)
            ((Text -> Type -> Type -> Matches Text Constraint)
-> SimpleWhenMatched Text Type Type (Matches Text Constraint)
forall (f :: * -> *) k x y z.
Applicative f =>
(k -> x -> y -> z) -> WhenMatched f k x y z
M.zipWithMatched ((Text -> Type -> Type -> Matches Text Constraint)
 -> SimpleWhenMatched Text Type Type (Matches Text Constraint))
-> (Text -> Type -> Type -> Matches Text Constraint)
-> SimpleWhenMatched Text Type Type (Matches Text Constraint)
forall a b. (a -> b) -> a -> b
$ \Text
_ Type
l Type
r -> Constraint -> Matches Text Constraint
forall a b. b -> Matches a b
BothSides (Type -> Type -> Constraint
Equality Type
l Type
r))
            Env Type
rec1
            Env Type
rec2
      Bool -> m () -> m ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless ([Text] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Text]
lefts Bool -> Bool -> Bool
&& [Text] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Text]
rights) (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$
        [InputAnn] -> TypeError -> m ()
forall (m :: * -> *) a.
MonadError TypeErrorA m =>
[InputAnn] -> TypeError -> m a
throwErr [InputAnn
ann] (TypeError -> m ()) -> TypeError -> m ()
forall a b. (a -> b) -> a -> b
$ Type -> Type -> [Text] -> [Text] -> TypeError
RecordDiff Type
t1 Type
t2 [Text]
lefts [Text]
rights
      ([ConstraintA], Map Text (InputAnn, Type))
-> m ([ConstraintA], Map Text (InputAnn, Type))
forall (f :: * -> *) a. Applicative f => a -> f a
pure
        ( (Constraint -> ConstraintA) -> [Constraint] -> [ConstraintA]
forall a b. (a -> b) -> [a] -> [b]
map ((Constraint -> InputAnn -> ConstraintA)
-> InputAnn -> Constraint -> ConstraintA
forall a b c. (a -> b -> c) -> b -> a -> c
flip (,) InputAnn
ann) [Constraint]
matches
        , Map Text (InputAnn, Type)
forall a. Monoid a => a
mempty
        )

    -- we want to make sure rec1 and rec2 do not contain matching labels with non matching types
    -- we want to match the labels from rec1 that do not exist in rec2 to match "ext"
    Equality t1 :: Type
t1@(TypeRec ([(Text, Type)] -> Env Type
forall k a. Ord k => [(k, a)] -> Map k a
M.fromList -> Env Type
rec1)) t2 :: Type
t2@(TypeRecExt ([(Text, Type)] -> Env Type
forall k a. Ord k => [(k, a)] -> Map k a
M.fromList -> Env Type
rec2) Text
ext) -> do
      let
        ([(Text, Type)]
lefts, [(Text, Type)]
rights, [Constraint]
matches) =
          [Matches (Text, Type) Constraint]
-> ([(Text, Type)], [(Text, Type)], [Constraint])
forall a b. [Matches a b] -> ([a], [a], [b])
unzipMatches ([Matches (Text, Type) Constraint]
 -> ([(Text, Type)], [(Text, Type)], [Constraint]))
-> [Matches (Text, Type) Constraint]
-> ([(Text, Type)], [(Text, Type)], [Constraint])
forall a b. (a -> b) -> a -> b
$ Map Text (Matches (Text, Type) Constraint)
-> [Matches (Text, Type) Constraint]
forall k a. Map k a -> [a]
M.elems (Map Text (Matches (Text, Type) Constraint)
 -> [Matches (Text, Type) Constraint])
-> Map Text (Matches (Text, Type) Constraint)
-> [Matches (Text, Type) Constraint]
forall a b. (a -> b) -> a -> b
$ SimpleWhenMissing Text Type (Matches (Text, Type) Constraint)
-> SimpleWhenMissing Text Type (Matches (Text, Type) Constraint)
-> SimpleWhenMatched
     Text Type Type (Matches (Text, Type) Constraint)
-> Env Type
-> Env Type
-> Map Text (Matches (Text, Type) Constraint)
forall k a c b.
Ord k =>
SimpleWhenMissing k a c
-> SimpleWhenMissing k b c
-> SimpleWhenMatched k a b c
-> Map k a
-> Map k b
-> Map k c
M.merge
            ((Text -> Type -> Matches (Text, Type) Constraint)
-> SimpleWhenMissing Text Type (Matches (Text, Type) Constraint)
forall (f :: * -> *) k x y.
Applicative f =>
(k -> x -> y) -> WhenMissing f k x y
M.mapMissing ((Text -> Type -> Matches (Text, Type) Constraint)
 -> SimpleWhenMissing Text Type (Matches (Text, Type) Constraint))
-> (Text -> Type -> Matches (Text, Type) Constraint)
-> SimpleWhenMissing Text Type (Matches (Text, Type) Constraint)
forall a b. (a -> b) -> a -> b
$ ((Text, Type) -> Matches (Text, Type) Constraint)
-> (Type -> (Text, Type))
-> Type
-> Matches (Text, Type) Constraint
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Text, Type) -> Matches (Text, Type) Constraint
forall a b. a -> Matches a b
OnlyLeft ((Type -> (Text, Type)) -> Type -> Matches (Text, Type) Constraint)
-> (Text -> Type -> (Text, Type))
-> Text
-> Type
-> Matches (Text, Type) Constraint
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (,))
            ((Text -> Type -> Matches (Text, Type) Constraint)
-> SimpleWhenMissing Text Type (Matches (Text, Type) Constraint)
forall (f :: * -> *) k x y.
Applicative f =>
(k -> x -> y) -> WhenMissing f k x y
M.mapMissing ((Text -> Type -> Matches (Text, Type) Constraint)
 -> SimpleWhenMissing Text Type (Matches (Text, Type) Constraint))
-> (Text -> Type -> Matches (Text, Type) Constraint)
-> SimpleWhenMissing Text Type (Matches (Text, Type) Constraint)
forall a b. (a -> b) -> a -> b
$ ((Text, Type) -> Matches (Text, Type) Constraint)
-> (Type -> (Text, Type))
-> Type
-> Matches (Text, Type) Constraint
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Text, Type) -> Matches (Text, Type) Constraint
forall a b. a -> Matches a b
OnlyRight ((Type -> (Text, Type)) -> Type -> Matches (Text, Type) Constraint)
-> (Text -> Type -> (Text, Type))
-> Text
-> Type
-> Matches (Text, Type) Constraint
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (,))
            ((Text -> Type -> Type -> Matches (Text, Type) Constraint)
-> SimpleWhenMatched
     Text Type Type (Matches (Text, Type) Constraint)
forall (f :: * -> *) k x y z.
Applicative f =>
(k -> x -> y -> z) -> WhenMatched f k x y z
M.zipWithMatched ((Text -> Type -> Type -> Matches (Text, Type) Constraint)
 -> SimpleWhenMatched
      Text Type Type (Matches (Text, Type) Constraint))
-> (Text -> Type -> Type -> Matches (Text, Type) Constraint)
-> SimpleWhenMatched
     Text Type Type (Matches (Text, Type) Constraint)
forall a b. (a -> b) -> a -> b
$ \Text
_ Type
l Type
r -> Constraint -> Matches (Text, Type) Constraint
forall a b. b -> Matches a b
BothSides (Type -> Type -> Constraint
Equality Type
l Type
r))
            Env Type
rec1
            Env Type
rec2
      Bool -> m () -> m ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless ([(Text, Type)] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [(Text, Type)]
rights) (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$
        [InputAnn] -> TypeError -> m ()
forall (m :: * -> *) a.
MonadError TypeErrorA m =>
[InputAnn] -> TypeError -> m a
throwErr [InputAnn
ann] (TypeError -> m ()) -> TypeError -> m ()
forall a b. (a -> b) -> a -> b
$ Type -> Type -> [Text] -> [Text] -> TypeError
RecordDiff Type
t1 Type
t2 [] (((Text, Type) -> Text) -> [(Text, Type)] -> [Text]
forall a b. (a -> b) -> [a] -> [b]
map (Text, Type) -> Text
forall a b. (a, b) -> a
fst [(Text, Type)]
rights)
      ([ConstraintA], Map Text (InputAnn, Type))
-> m ([ConstraintA], Map Text (InputAnn, Type))
forall (f :: * -> *) a. Applicative f => a -> f a
pure
        ( (Constraint -> ConstraintA) -> [Constraint] -> [ConstraintA]
forall a b. (a -> b) -> [a] -> [b]
map ((Constraint -> InputAnn -> ConstraintA)
-> InputAnn -> Constraint -> ConstraintA
forall a b c. (a -> b -> c) -> b -> a -> c
flip (,) InputAnn
ann) ([Constraint] -> [ConstraintA]) -> [Constraint] -> [ConstraintA]
forall a b. (a -> b) -> a -> b
$ Type -> Type -> Constraint
Equality ([(Text, Type)] -> Type
TypeRec [(Text, Type)]
lefts) (Text -> Type
TypeVar Text
ext) Constraint -> [Constraint] -> [Constraint]
forall a. a -> [a] -> [a]
: [Constraint]
matches
        , Map Text (InputAnn, Type)
forall a. Monoid a => a
mempty
        )
    Equality t1 :: Type
t1@TypeRecExt{} t2 :: Type
t2@TypeRec{} -> do
      ConstraintA -> m ([ConstraintA], Map Text (InputAnn, Type))
forall (b :: * -> *) (m :: * -> *).
Solve b m =>
ConstraintA -> m ([ConstraintA], Map Text (InputAnn, Type))
solveConstraint (Type -> Type -> Constraint
Equality Type
t2 Type
t1, InputAnn
ann)

    Equality (TypeRecExt ([(Text, Type)] -> Env Type
forall k a. Ord k => [(k, a)] -> Map k a
M.fromList -> Env Type
rec1) Text
ext1) (TypeRecExt ([(Text, Type)] -> Env Type
forall k a. Ord k => [(k, a)] -> Map k a
M.fromList -> Env Type
rec2) Text
ext2) -> do
      let
        matches :: [Constraint]
matches = Map Text Constraint -> [Constraint]
forall k a. Map k a -> [a]
M.elems (Map Text Constraint -> [Constraint])
-> Map Text Constraint -> [Constraint]
forall a b. (a -> b) -> a -> b
$ (Type -> Type -> Constraint)
-> Env Type -> Env Type -> Map Text Constraint
forall k a b c.
Ord k =>
(a -> b -> c) -> Map k a -> Map k b -> Map k c
M.intersectionWith Type -> Type -> Constraint
Equality Env Type
rec1 Env Type
rec2
        onlyLeft :: Env Type
onlyLeft = Env Type -> Env Type -> Env Type
forall k a b. Ord k => Map k a -> Map k b -> Map k a
M.difference Env Type
rec1 Env Type
rec2
        onlyRight :: Env Type
onlyRight = Env Type -> Env Type -> Env Type
forall k a b. Ord k => Map k a -> Map k b -> Map k a
M.difference Env Type
rec2 Env Type
rec1
      Text
ext' <- Text -> m Text
forall (m :: * -> *). MonadState ElabState m => Text -> m Text
genTypeVar Text
"ext"
      ([ConstraintA], Map Text (InputAnn, Type))
-> m ([ConstraintA], Map Text (InputAnn, Type))
forall (f :: * -> *) a. Applicative f => a -> f a
pure
        ( (Constraint -> ConstraintA) -> [Constraint] -> [ConstraintA]
forall a b. (a -> b) -> [a] -> [b]
map ((Constraint -> InputAnn -> ConstraintA)
-> InputAnn -> Constraint -> ConstraintA
forall a b c. (a -> b -> c) -> b -> a -> c
flip (,) InputAnn
ann)
          ([Constraint] -> [ConstraintA]) -> [Constraint] -> [ConstraintA]
forall a b. (a -> b) -> a -> b
$ Type -> Type -> Constraint
Equality ([(Text, Type)] -> Text -> Type
TypeRecExt (Env Type -> [(Text, Type)]
forall k a. Map k a -> [(k, a)]
M.toList Env Type
onlyLeft) Text
ext') (Text -> Type
TypeVar Text
ext2)
          Constraint -> [Constraint] -> [Constraint]
forall a. a -> [a] -> [a]
: Type -> Type -> Constraint
Equality ([(Text, Type)] -> Text -> Type
TypeRecExt (Env Type -> [(Text, Type)]
forall k a. Map k a -> [(k, a)]
M.toList Env Type
onlyRight) Text
ext') (Text -> Type
TypeVar Text
ext1)
          Constraint -> [Constraint] -> [Constraint]
forall a. a -> [a] -> [a]
: [Constraint]
matches
        , Map Text (InputAnn, Type)
forall a. Monoid a => a
mempty
        )

    -- Polymorphic Variants --

    -- all variants constructors and types should match
    Equality t1 :: Type
t1@(TypeVariant ([(Text, Type)] -> Env Type
forall k a. Ord k => [(k, a)] -> Map k a
M.fromList -> Env Type
var1)) t2 :: Type
t2@(TypeVariant ([(Text, Type)] -> Env Type
forall k a. Ord k => [(k, a)] -> Map k a
M.fromList -> Env Type
var2)) -> do
      let
        ([Text]
lefts, [Text]
rights, [Constraint]
matches) =
          [Matches Text Constraint] -> ([Text], [Text], [Constraint])
forall a b. [Matches a b] -> ([a], [a], [b])
unzipMatches ([Matches Text Constraint] -> ([Text], [Text], [Constraint]))
-> [Matches Text Constraint] -> ([Text], [Text], [Constraint])
forall a b. (a -> b) -> a -> b
$ Map Text (Matches Text Constraint) -> [Matches Text Constraint]
forall k a. Map k a -> [a]
M.elems (Map Text (Matches Text Constraint) -> [Matches Text Constraint])
-> Map Text (Matches Text Constraint) -> [Matches Text Constraint]
forall a b. (a -> b) -> a -> b
$ SimpleWhenMissing Text Type (Matches Text Constraint)
-> SimpleWhenMissing Text Type (Matches Text Constraint)
-> SimpleWhenMatched Text Type Type (Matches Text Constraint)
-> Env Type
-> Env Type
-> Map Text (Matches Text Constraint)
forall k a c b.
Ord k =>
SimpleWhenMissing k a c
-> SimpleWhenMissing k b c
-> SimpleWhenMatched k a b c
-> Map k a
-> Map k b
-> Map k c
M.merge
            ((Text -> Type -> Matches Text Constraint)
-> SimpleWhenMissing Text Type (Matches Text Constraint)
forall (f :: * -> *) k x y.
Applicative f =>
(k -> x -> y) -> WhenMissing f k x y
M.mapMissing ((Text -> Type -> Matches Text Constraint)
 -> SimpleWhenMissing Text Type (Matches Text Constraint))
-> (Text -> Type -> Matches Text Constraint)
-> SimpleWhenMissing Text Type (Matches Text Constraint)
forall a b. (a -> b) -> a -> b
$ Matches Text Constraint -> Type -> Matches Text Constraint
forall a b. a -> b -> a
const (Matches Text Constraint -> Type -> Matches Text Constraint)
-> (Text -> Matches Text Constraint)
-> Text
-> Type
-> Matches Text Constraint
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Text -> Matches Text Constraint
forall a b. a -> Matches a b
OnlyLeft)
            ((Text -> Type -> Matches Text Constraint)
-> SimpleWhenMissing Text Type (Matches Text Constraint)
forall (f :: * -> *) k x y.
Applicative f =>
(k -> x -> y) -> WhenMissing f k x y
M.mapMissing ((Text -> Type -> Matches Text Constraint)
 -> SimpleWhenMissing Text Type (Matches Text Constraint))
-> (Text -> Type -> Matches Text Constraint)
-> SimpleWhenMissing Text Type (Matches Text Constraint)
forall a b. (a -> b) -> a -> b
$ Matches Text Constraint -> Type -> Matches Text Constraint
forall a b. a -> b -> a
const (Matches Text Constraint -> Type -> Matches Text Constraint)
-> (Text -> Matches Text Constraint)
-> Text
-> Type
-> Matches Text Constraint
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Text -> Matches Text Constraint
forall a b. a -> Matches a b
OnlyRight)
            ((Text -> Type -> Type -> Matches Text Constraint)
-> SimpleWhenMatched Text Type Type (Matches Text Constraint)
forall (f :: * -> *) k x y z.
Applicative f =>
(k -> x -> y -> z) -> WhenMatched f k x y z
M.zipWithMatched ((Text -> Type -> Type -> Matches Text Constraint)
 -> SimpleWhenMatched Text Type Type (Matches Text Constraint))
-> (Text -> Type -> Type -> Matches Text Constraint)
-> SimpleWhenMatched Text Type Type (Matches Text Constraint)
forall a b. (a -> b) -> a -> b
$ \Text
_ Type
l Type
r -> Constraint -> Matches Text Constraint
forall a b. b -> Matches a b
BothSides (Type -> Type -> Constraint
Equality Type
l Type
r))
            Env Type
var1
            Env Type
var2
      Bool -> m () -> m ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless ([Text] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Text]
lefts Bool -> Bool -> Bool
&& [Text] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Text]
rights) (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$
        [InputAnn] -> TypeError -> m ()
forall (m :: * -> *) a.
MonadError TypeErrorA m =>
[InputAnn] -> TypeError -> m a
throwErr [InputAnn
ann] (TypeError -> m ()) -> TypeError -> m ()
forall a b. (a -> b) -> a -> b
$ Type -> Type -> [Text] -> [Text] -> TypeError
VariantDiff Type
t1 Type
t2 [Text]
lefts [Text]
rights
      ([ConstraintA], Map Text (InputAnn, Type))
-> m ([ConstraintA], Map Text (InputAnn, Type))
forall (f :: * -> *) a. Applicative f => a -> f a
pure
        ( (Constraint -> ConstraintA) -> [Constraint] -> [ConstraintA]
forall a b. (a -> b) -> [a] -> [b]
map ((Constraint -> InputAnn -> ConstraintA)
-> InputAnn -> Constraint -> ConstraintA
forall a b c. (a -> b -> c) -> b -> a -> c
flip (,) InputAnn
ann) [Constraint]
matches
        , Map Text (InputAnn, Type)
forall a. Monoid a => a
mempty
        )

    -- all relevant variants should match.
    -- When we have matching constructors from both sides, we match their type.
    Equality (TypePolyVariantLB ([(Text, Type)] -> Env Type
forall k a. Ord k => [(k, a)] -> Map k a
M.fromList -> Env Type
var1) Text
ext1) (TypePolyVariantLB ([(Text, Type)] -> Env Type
forall k a. Ord k => [(k, a)] -> Map k a
M.fromList -> Env Type
var2) Text
ext2) -> do
      let
        ([(Text, Type)]
lefts, [(Text, Type)]
rights, [Constraint]
matches) =
          [Matches (Text, Type) Constraint]
-> ([(Text, Type)], [(Text, Type)], [Constraint])
forall a b. [Matches a b] -> ([a], [a], [b])
unzipMatches ([Matches (Text, Type) Constraint]
 -> ([(Text, Type)], [(Text, Type)], [Constraint]))
-> [Matches (Text, Type) Constraint]
-> ([(Text, Type)], [(Text, Type)], [Constraint])
forall a b. (a -> b) -> a -> b
$ Map Text (Matches (Text, Type) Constraint)
-> [Matches (Text, Type) Constraint]
forall k a. Map k a -> [a]
M.elems (Map Text (Matches (Text, Type) Constraint)
 -> [Matches (Text, Type) Constraint])
-> Map Text (Matches (Text, Type) Constraint)
-> [Matches (Text, Type) Constraint]
forall a b. (a -> b) -> a -> b
$ SimpleWhenMissing Text Type (Matches (Text, Type) Constraint)
-> SimpleWhenMissing Text Type (Matches (Text, Type) Constraint)
-> SimpleWhenMatched
     Text Type Type (Matches (Text, Type) Constraint)
-> Env Type
-> Env Type
-> Map Text (Matches (Text, Type) Constraint)
forall k a c b.
Ord k =>
SimpleWhenMissing k a c
-> SimpleWhenMissing k b c
-> SimpleWhenMatched k a b c
-> Map k a
-> Map k b
-> Map k c
M.merge
            ((Text -> Type -> Matches (Text, Type) Constraint)
-> SimpleWhenMissing Text Type (Matches (Text, Type) Constraint)
forall (f :: * -> *) k x y.
Applicative f =>
(k -> x -> y) -> WhenMissing f k x y
M.mapMissing ((Text -> Type -> Matches (Text, Type) Constraint)
 -> SimpleWhenMissing Text Type (Matches (Text, Type) Constraint))
-> (Text -> Type -> Matches (Text, Type) Constraint)
-> SimpleWhenMissing Text Type (Matches (Text, Type) Constraint)
forall a b. (a -> b) -> a -> b
$ ((Text, Type) -> Matches (Text, Type) Constraint)
-> (Type -> (Text, Type))
-> Type
-> Matches (Text, Type) Constraint
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Text, Type) -> Matches (Text, Type) Constraint
forall a b. a -> Matches a b
OnlyLeft ((Type -> (Text, Type)) -> Type -> Matches (Text, Type) Constraint)
-> (Text -> Type -> (Text, Type))
-> Text
-> Type
-> Matches (Text, Type) Constraint
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (,))
            ((Text -> Type -> Matches (Text, Type) Constraint)
-> SimpleWhenMissing Text Type (Matches (Text, Type) Constraint)
forall (f :: * -> *) k x y.
Applicative f =>
(k -> x -> y) -> WhenMissing f k x y
M.mapMissing ((Text -> Type -> Matches (Text, Type) Constraint)
 -> SimpleWhenMissing Text Type (Matches (Text, Type) Constraint))
-> (Text -> Type -> Matches (Text, Type) Constraint)
-> SimpleWhenMissing Text Type (Matches (Text, Type) Constraint)
forall a b. (a -> b) -> a -> b
$ ((Text, Type) -> Matches (Text, Type) Constraint)
-> (Type -> (Text, Type))
-> Type
-> Matches (Text, Type) Constraint
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Text, Type) -> Matches (Text, Type) Constraint
forall a b. a -> Matches a b
OnlyRight ((Type -> (Text, Type)) -> Type -> Matches (Text, Type) Constraint)
-> (Text -> Type -> (Text, Type))
-> Text
-> Type
-> Matches (Text, Type) Constraint
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (,))
            ((Text -> Type -> Type -> Matches (Text, Type) Constraint)
-> SimpleWhenMatched
     Text Type Type (Matches (Text, Type) Constraint)
forall (f :: * -> *) k x y z.
Applicative f =>
(k -> x -> y -> z) -> WhenMatched f k x y z
M.zipWithMatched ((Text -> Type -> Type -> Matches (Text, Type) Constraint)
 -> SimpleWhenMatched
      Text Type Type (Matches (Text, Type) Constraint))
-> (Text -> Type -> Type -> Matches (Text, Type) Constraint)
-> SimpleWhenMatched
     Text Type Type (Matches (Text, Type) Constraint)
forall a b. (a -> b) -> a -> b
$ \Text
_ Type
l Type
r -> Constraint -> Matches (Text, Type) Constraint
forall a b. b -> Matches a b
BothSides (Type -> Type -> Constraint
Equality Type
l Type
r))
            Env Type
var1
            Env Type
var2
      Text
ext' <- Text -> m Text
forall (m :: * -> *). MonadState ElabState m => Text -> m Text
genTypeVar Text
"tv"
      ([ConstraintA], Map Text (InputAnn, Type))
-> m ([ConstraintA], Map Text (InputAnn, Type))
forall (f :: * -> *) a. Applicative f => a -> f a
pure
        ( (Constraint -> ConstraintA) -> [Constraint] -> [ConstraintA]
forall a b. (a -> b) -> [a] -> [b]
map ((Constraint -> InputAnn -> ConstraintA)
-> InputAnn -> Constraint -> ConstraintA
forall a b c. (a -> b -> c) -> b -> a -> c
flip (,) InputAnn
ann)
          ([Constraint] -> [ConstraintA]) -> [Constraint] -> [ConstraintA]
forall a b. (a -> b) -> a -> b
$ Type -> Type -> Constraint
Equality ([(Text, Type)] -> Text -> Type
TypePolyVariantLB ([(Text, Type)] -> [(Text, Type)]
forall a. Ord a => [a] -> [a]
sort ([(Text, Type)] -> [(Text, Type)])
-> [(Text, Type)] -> [(Text, Type)]
forall a b. (a -> b) -> a -> b
$ [(Text, Type)]
lefts [(Text, Type)] -> [(Text, Type)] -> [(Text, Type)]
forall a. Semigroup a => a -> a -> a
<> [(Text, Type)]
rights) Text
ext') (Text -> Type
TypeVar Text
ext1)
          Constraint -> [Constraint] -> [Constraint]
forall a. a -> [a] -> [a]
: Type -> Type -> Constraint
Equality ([(Text, Type)] -> Text -> Type
TypePolyVariantLB ([(Text, Type)] -> [(Text, Type)]
forall a. Ord a => [a] -> [a]
sort ([(Text, Type)] -> [(Text, Type)])
-> [(Text, Type)] -> [(Text, Type)]
forall a b. (a -> b) -> a -> b
$ [(Text, Type)]
lefts [(Text, Type)] -> [(Text, Type)] -> [(Text, Type)]
forall a. Semigroup a => a -> a -> a
<> [(Text, Type)]
rights) Text
ext') (Text -> Type
TypeVar Text
ext2)
          Constraint -> [Constraint] -> [Constraint]
forall a. a -> [a] -> [a]
: [Constraint]
matches
        , Map Text (InputAnn, Type)
forall a. Monoid a => a
mempty
        )

    -- to unify two upper bounded polymorphic variants with the same hidden type variant, we:
    -- 1. match the types of the known fields, and
    -- 2. merge all of the fields together into a UB that represents the merge, and
    -- 3. match it with the hidden type variable.
    -- This process keeps track of the variants we ran into for a specific type variable during constraint solving.
    Equality (TypePolyVariantUB Text
tv1 ([(Text, Type)] -> Env Type
forall k a. Ord k => [(k, a)] -> Map k a
M.fromList -> Env Type
var1)) (TypePolyVariantUB Text
tv2 ([(Text, Type)] -> Env Type
forall k a. Ord k => [(k, a)] -> Map k a
M.fromList -> Env Type
var2))
      | Text
tv1 Text -> Text -> Bool
forall a. Eq a => a -> a -> Bool
== Text
tv2 -> do
        let
          ([(Text, Type)]
lefts, [(Text, Type)]
rights, [((Text, Type), Constraint)]
matches) =
            [Matches (Text, Type) ((Text, Type), Constraint)]
-> ([(Text, Type)], [(Text, Type)], [((Text, Type), Constraint)])
forall a b. [Matches a b] -> ([a], [a], [b])
unzipMatches ([Matches (Text, Type) ((Text, Type), Constraint)]
 -> ([(Text, Type)], [(Text, Type)], [((Text, Type), Constraint)]))
-> [Matches (Text, Type) ((Text, Type), Constraint)]
-> ([(Text, Type)], [(Text, Type)], [((Text, Type), Constraint)])
forall a b. (a -> b) -> a -> b
$ Map Text (Matches (Text, Type) ((Text, Type), Constraint))
-> [Matches (Text, Type) ((Text, Type), Constraint)]
forall k a. Map k a -> [a]
M.elems (Map Text (Matches (Text, Type) ((Text, Type), Constraint))
 -> [Matches (Text, Type) ((Text, Type), Constraint)])
-> Map Text (Matches (Text, Type) ((Text, Type), Constraint))
-> [Matches (Text, Type) ((Text, Type), Constraint)]
forall a b. (a -> b) -> a -> b
$ SimpleWhenMissing
  Text Type (Matches (Text, Type) ((Text, Type), Constraint))
-> SimpleWhenMissing
     Text Type (Matches (Text, Type) ((Text, Type), Constraint))
-> SimpleWhenMatched
     Text Type Type (Matches (Text, Type) ((Text, Type), Constraint))
-> Env Type
-> Env Type
-> Map Text (Matches (Text, Type) ((Text, Type), Constraint))
forall k a c b.
Ord k =>
SimpleWhenMissing k a c
-> SimpleWhenMissing k b c
-> SimpleWhenMatched k a b c
-> Map k a
-> Map k b
-> Map k c
M.merge
              ((Text -> Type -> Matches (Text, Type) ((Text, Type), Constraint))
-> SimpleWhenMissing
     Text Type (Matches (Text, Type) ((Text, Type), Constraint))
forall (f :: * -> *) k x y.
Applicative f =>
(k -> x -> y) -> WhenMissing f k x y
M.mapMissing ((Text -> Type -> Matches (Text, Type) ((Text, Type), Constraint))
 -> SimpleWhenMissing
      Text Type (Matches (Text, Type) ((Text, Type), Constraint)))
-> (Text
    -> Type -> Matches (Text, Type) ((Text, Type), Constraint))
-> SimpleWhenMissing
     Text Type (Matches (Text, Type) ((Text, Type), Constraint))
forall a b. (a -> b) -> a -> b
$ ((Text, Type) -> Matches (Text, Type) ((Text, Type), Constraint))
-> (Type -> (Text, Type))
-> Type
-> Matches (Text, Type) ((Text, Type), Constraint)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Text, Type) -> Matches (Text, Type) ((Text, Type), Constraint)
forall a b. a -> Matches a b
OnlyLeft ((Type -> (Text, Type))
 -> Type -> Matches (Text, Type) ((Text, Type), Constraint))
-> (Text -> Type -> (Text, Type))
-> Text
-> Type
-> Matches (Text, Type) ((Text, Type), Constraint)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (,))
              ((Text -> Type -> Matches (Text, Type) ((Text, Type), Constraint))
-> SimpleWhenMissing
     Text Type (Matches (Text, Type) ((Text, Type), Constraint))
forall (f :: * -> *) k x y.
Applicative f =>
(k -> x -> y) -> WhenMissing f k x y
M.mapMissing ((Text -> Type -> Matches (Text, Type) ((Text, Type), Constraint))
 -> SimpleWhenMissing
      Text Type (Matches (Text, Type) ((Text, Type), Constraint)))
-> (Text
    -> Type -> Matches (Text, Type) ((Text, Type), Constraint))
-> SimpleWhenMissing
     Text Type (Matches (Text, Type) ((Text, Type), Constraint))
forall a b. (a -> b) -> a -> b
$ ((Text, Type) -> Matches (Text, Type) ((Text, Type), Constraint))
-> (Type -> (Text, Type))
-> Type
-> Matches (Text, Type) ((Text, Type), Constraint)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Text, Type) -> Matches (Text, Type) ((Text, Type), Constraint)
forall a b. a -> Matches a b
OnlyRight ((Type -> (Text, Type))
 -> Type -> Matches (Text, Type) ((Text, Type), Constraint))
-> (Text -> Type -> (Text, Type))
-> Text
-> Type
-> Matches (Text, Type) ((Text, Type), Constraint)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (,))
              ((Text
 -> Type -> Type -> Matches (Text, Type) ((Text, Type), Constraint))
-> SimpleWhenMatched
     Text Type Type (Matches (Text, Type) ((Text, Type), Constraint))
forall (f :: * -> *) k x y z.
Applicative f =>
(k -> x -> y -> z) -> WhenMatched f k x y z
M.zipWithMatched ((Text
  -> Type -> Type -> Matches (Text, Type) ((Text, Type), Constraint))
 -> SimpleWhenMatched
      Text Type Type (Matches (Text, Type) ((Text, Type), Constraint)))
-> (Text
    -> Type -> Type -> Matches (Text, Type) ((Text, Type), Constraint))
-> SimpleWhenMatched
     Text Type Type (Matches (Text, Type) ((Text, Type), Constraint))
forall a b. (a -> b) -> a -> b
$ \Text
k Type
l Type
r -> ((Text, Type), Constraint)
-> Matches (Text, Type) ((Text, Type), Constraint)
forall a b. b -> Matches a b
BothSides ((Text
k, Type
l), Type -> Type -> Constraint
Equality Type
l Type
r))
              Env Type
var1
              Env Type
var2
        ([ConstraintA], Map Text (InputAnn, Type))
-> m ([ConstraintA], Map Text (InputAnn, Type))
forall (f :: * -> *) a. Applicative f => a -> f a
pure
          ( (Constraint -> ConstraintA) -> [Constraint] -> [ConstraintA]
forall a b. (a -> b) -> [a] -> [b]
map ((Constraint -> InputAnn -> ConstraintA)
-> InputAnn -> Constraint -> ConstraintA
forall a b c. (a -> b -> c) -> b -> a -> c
flip (,) InputAnn
ann)
            ([Constraint] -> [ConstraintA]) -> [Constraint] -> [ConstraintA]
forall a b. (a -> b) -> a -> b
$ Type -> Type -> Constraint
Equality (Text -> [(Text, Type)] -> Type
TypePolyVariantUB Text
tv1 ([(Text, Type)] -> [(Text, Type)]
forall a. Ord a => [a] -> [a]
sort ([(Text, Type)] -> [(Text, Type)])
-> [(Text, Type)] -> [(Text, Type)]
forall a b. (a -> b) -> a -> b
$ [(Text, Type)]
lefts [(Text, Type)] -> [(Text, Type)] -> [(Text, Type)]
forall a. Semigroup a => a -> a -> a
<> [(Text, Type)]
rights [(Text, Type)] -> [(Text, Type)] -> [(Text, Type)]
forall a. Semigroup a => a -> a -> a
<> (((Text, Type), Constraint) -> (Text, Type))
-> [((Text, Type), Constraint)] -> [(Text, Type)]
forall a b. (a -> b) -> [a] -> [b]
map ((Text, Type), Constraint) -> (Text, Type)
forall a b. (a, b) -> a
fst [((Text, Type), Constraint)]
matches)) (Text -> Type
TypeVar Text
tv1)
            Constraint -> [Constraint] -> [Constraint]
forall a. a -> [a] -> [a]
: (((Text, Type), Constraint) -> Constraint)
-> [((Text, Type), Constraint)] -> [Constraint]
forall a b. (a -> b) -> [a] -> [b]
map ((Text, Type), Constraint) -> Constraint
forall a b. (a, b) -> b
snd [((Text, Type), Constraint)]
matches
          , Map Text (InputAnn, Type)
forall a. Monoid a => a
mempty
          )
    -- but if the type variables don't match, we treat them as regular variants that should match.
    Equality (TypePolyVariantUB Text
_ [(Text, Type)]
vars1) (TypePolyVariantUB Text
_ [(Text, Type)]
vars2) ->
      ConstraintA -> m ([ConstraintA], Map Text (InputAnn, Type))
forall (b :: * -> *) (m :: * -> *).
Solve b m =>
ConstraintA -> m ([ConstraintA], Map Text (InputAnn, Type))
solveConstraint (Type -> Type -> Constraint
Equality ([(Text, Type)] -> Type
TypeVariant [(Text, Type)]
vars1) ([(Text, Type)] -> Type
TypeVariant [(Text, Type)]
vars2), InputAnn
ann)

    -- similar to TypeRecordExt, there shouldn't be variants in LB that we don't know of in the regular variant.
    Equality t1 :: Type
t1@(TypeVariant ([(Text, Type)] -> Env Type
forall k a. Ord k => [(k, a)] -> Map k a
M.fromList -> Env Type
var1)) t2 :: Type
t2@(TypePolyVariantLB ([(Text, Type)] -> Env Type
forall k a. Ord k => [(k, a)] -> Map k a
M.fromList -> Env Type
var2) Text
ext) -> do
      let
        ([(Text, Type)]
lefts, [(Text, Type)]
rights, [Constraint]
matches) =
          [Matches (Text, Type) Constraint]
-> ([(Text, Type)], [(Text, Type)], [Constraint])
forall a b. [Matches a b] -> ([a], [a], [b])
unzipMatches ([Matches (Text, Type) Constraint]
 -> ([(Text, Type)], [(Text, Type)], [Constraint]))
-> [Matches (Text, Type) Constraint]
-> ([(Text, Type)], [(Text, Type)], [Constraint])
forall a b. (a -> b) -> a -> b
$ Map Text (Matches (Text, Type) Constraint)
-> [Matches (Text, Type) Constraint]
forall k a. Map k a -> [a]
M.elems (Map Text (Matches (Text, Type) Constraint)
 -> [Matches (Text, Type) Constraint])
-> Map Text (Matches (Text, Type) Constraint)
-> [Matches (Text, Type) Constraint]
forall a b. (a -> b) -> a -> b
$ SimpleWhenMissing Text Type (Matches (Text, Type) Constraint)
-> SimpleWhenMissing Text Type (Matches (Text, Type) Constraint)
-> SimpleWhenMatched
     Text Type Type (Matches (Text, Type) Constraint)
-> Env Type
-> Env Type
-> Map Text (Matches (Text, Type) Constraint)
forall k a c b.
Ord k =>
SimpleWhenMissing k a c
-> SimpleWhenMissing k b c
-> SimpleWhenMatched k a b c
-> Map k a
-> Map k b
-> Map k c
M.merge
            ((Text -> Type -> Matches (Text, Type) Constraint)
-> SimpleWhenMissing Text Type (Matches (Text, Type) Constraint)
forall (f :: * -> *) k x y.
Applicative f =>
(k -> x -> y) -> WhenMissing f k x y
M.mapMissing ((Text -> Type -> Matches (Text, Type) Constraint)
 -> SimpleWhenMissing Text Type (Matches (Text, Type) Constraint))
-> (Text -> Type -> Matches (Text, Type) Constraint)
-> SimpleWhenMissing Text Type (Matches (Text, Type) Constraint)
forall a b. (a -> b) -> a -> b
$ ((Text, Type) -> Matches (Text, Type) Constraint)
-> (Type -> (Text, Type))
-> Type
-> Matches (Text, Type) Constraint
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Text, Type) -> Matches (Text, Type) Constraint
forall a b. a -> Matches a b
OnlyLeft ((Type -> (Text, Type)) -> Type -> Matches (Text, Type) Constraint)
-> (Text -> Type -> (Text, Type))
-> Text
-> Type
-> Matches (Text, Type) Constraint
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (,))
            ((Text -> Type -> Matches (Text, Type) Constraint)
-> SimpleWhenMissing Text Type (Matches (Text, Type) Constraint)
forall (f :: * -> *) k x y.
Applicative f =>
(k -> x -> y) -> WhenMissing f k x y
M.mapMissing ((Text -> Type -> Matches (Text, Type) Constraint)
 -> SimpleWhenMissing Text Type (Matches (Text, Type) Constraint))
-> (Text -> Type -> Matches (Text, Type) Constraint)
-> SimpleWhenMissing Text Type (Matches (Text, Type) Constraint)
forall a b. (a -> b) -> a -> b
$ ((Text, Type) -> Matches (Text, Type) Constraint)
-> (Type -> (Text, Type))
-> Type
-> Matches (Text, Type) Constraint
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Text, Type) -> Matches (Text, Type) Constraint
forall a b. a -> Matches a b
OnlyRight ((Type -> (Text, Type)) -> Type -> Matches (Text, Type) Constraint)
-> (Text -> Type -> (Text, Type))
-> Text
-> Type
-> Matches (Text, Type) Constraint
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (,))
            ((Text -> Type -> Type -> Matches (Text, Type) Constraint)
-> SimpleWhenMatched
     Text Type Type (Matches (Text, Type) Constraint)
forall (f :: * -> *) k x y z.
Applicative f =>
(k -> x -> y -> z) -> WhenMatched f k x y z
M.zipWithMatched ((Text -> Type -> Type -> Matches (Text, Type) Constraint)
 -> SimpleWhenMatched
      Text Type Type (Matches (Text, Type) Constraint))
-> (Text -> Type -> Type -> Matches (Text, Type) Constraint)
-> SimpleWhenMatched
     Text Type Type (Matches (Text, Type) Constraint)
forall a b. (a -> b) -> a -> b
$ \Text
_ Type
l Type
r -> Constraint -> Matches (Text, Type) Constraint
forall a b. b -> Matches a b
BothSides (Type -> Type -> Constraint
Equality Type
l Type
r))
            Env Type
var1
            Env Type
var2
      Bool -> m () -> m ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless ([(Text, Type)] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [(Text, Type)]
rights) (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$
        [InputAnn] -> TypeError -> m ()
forall (m :: * -> *) a.
MonadError TypeErrorA m =>
[InputAnn] -> TypeError -> m a
throwErr [InputAnn
ann] (TypeError -> m ()) -> TypeError -> m ()
forall a b. (a -> b) -> a -> b
$ Type -> Type -> [Text] -> [Text] -> TypeError
VariantDiff Type
t1 Type
t2 [] (((Text, Type) -> Text) -> [(Text, Type)] -> [Text]
forall a b. (a -> b) -> [a] -> [b]
map (Text, Type) -> Text
forall a b. (a, b) -> a
fst [(Text, Type)]
rights)
      ([ConstraintA], Map Text (InputAnn, Type))
-> m ([ConstraintA], Map Text (InputAnn, Type))
forall (f :: * -> *) a. Applicative f => a -> f a
pure
        ( (Constraint -> ConstraintA) -> [Constraint] -> [ConstraintA]
forall a b. (a -> b) -> [a] -> [b]
map ((Constraint -> InputAnn -> ConstraintA)
-> InputAnn -> Constraint -> ConstraintA
forall a b c. (a -> b -> c) -> b -> a -> c
flip (,) InputAnn
ann) ([Constraint] -> [ConstraintA]) -> [Constraint] -> [ConstraintA]
forall a b. (a -> b) -> a -> b
$ Type -> Type -> Constraint
Equality ([(Text, Type)] -> Type
TypeVariant [(Text, Type)]
lefts) (Text -> Type
TypeVar Text
ext) Constraint -> [Constraint] -> [Constraint]
forall a. a -> [a] -> [a]
: [Constraint]
matches
        , Map Text (InputAnn, Type)
forall a. Monoid a => a
mempty
        )

    -- to unify LB and UB, we treat the UB as a normal variant.

    Equality t1 :: Type
t1@TypePolyVariantLB{} (TypePolyVariantUB Text
_ [(Text, Type)]
vars2) -> do
      ConstraintA -> m ([ConstraintA], Map Text (InputAnn, Type))
forall (b :: * -> *) (m :: * -> *).
Solve b m =>
ConstraintA -> m ([ConstraintA], Map Text (InputAnn, Type))
solveConstraint (Type -> Type -> Constraint
Equality Type
t1 ([(Text, Type)] -> Type
TypeVariant [(Text, Type)]
vars2), InputAnn
ann)

    Equality (TypePolyVariantUB Text
_ [(Text, Type)]
vars1) t2 :: Type
t2@TypePolyVariantLB{} -> do
      ConstraintA -> m ([ConstraintA], Map Text (InputAnn, Type))
forall (b :: * -> *) (m :: * -> *).
Solve b m =>
ConstraintA -> m ([ConstraintA], Map Text (InputAnn, Type))
solveConstraint (Type -> Type -> Constraint
Equality ([(Text, Type)] -> Type
TypeVariant [(Text, Type)]
vars1) Type
t2, InputAnn
ann)

    -- all other cases match like regular variants

    Equality t1 :: Type
t1@TypePolyVariantLB{} t2 :: Type
t2@TypeVariant{} -> do
      ConstraintA -> m ([ConstraintA], Map Text (InputAnn, Type))
forall (b :: * -> *) (m :: * -> *).
Solve b m =>
ConstraintA -> m ([ConstraintA], Map Text (InputAnn, Type))
solveConstraint (Type -> Type -> Constraint
Equality Type
t2 Type
t1, InputAnn
ann)

    Equality (TypePolyVariantUB Text
_ [(Text, Type)]
vars) t2 :: Type
t2@TypeVariant{} -> do
      ConstraintA -> m ([ConstraintA], Map Text (InputAnn, Type))
forall (b :: * -> *) (m :: * -> *).
Solve b m =>
ConstraintA -> m ([ConstraintA], Map Text (InputAnn, Type))
solveConstraint (Type -> Type -> Constraint
Equality ([(Text, Type)] -> Type
TypeVariant [(Text, Type)]
vars) Type
t2, InputAnn
ann)

    Equality t1 :: Type
t1@TypeVariant{} (TypePolyVariantUB Text
_ [(Text, Type)]
vars) -> do
      ConstraintA -> m ([ConstraintA], Map Text (InputAnn, Type))
forall (b :: * -> *) (m :: * -> *).
Solve b m =>
ConstraintA -> m ([ConstraintA], Map Text (InputAnn, Type))
solveConstraint (Type -> Type -> Constraint
Equality Type
t1 ([(Text, Type)] -> Type
TypeVariant [(Text, Type)]
vars), InputAnn
ann)

    --------------------------

    -- Map a type variable to the other type
    Equality (TypeVar Text
tv) Type
t2 ->
      ([ConstraintA], Map Text (InputAnn, Type))
-> m ([ConstraintA], Map Text (InputAnn, Type))
forall (f :: * -> *) a. Applicative f => a -> f a
pure
        ( [ConstraintA]
forall a. Monoid a => a
mempty
        , Text -> (InputAnn, Type) -> Map Text (InputAnn, Type)
forall k a. k -> a -> Map k a
M.singleton Text
tv (InputAnn
ann, Type
t2)
        )

    Equality Type
t1 (TypeVar Text
tv) ->
      ConstraintA -> m ([ConstraintA], Map Text (InputAnn, Type))
forall (b :: * -> *) (m :: * -> *).
Solve b m =>
ConstraintA -> m ([ConstraintA], Map Text (InputAnn, Type))
solveConstraint (Type -> Type -> Constraint
Equality (Text -> Type
TypeVar Text
tv) Type
t1, InputAnn
ann)

    -- finally, if non of the above cases matched with this empty open variant,
    -- treat it as a type variable.
    Equality (TypePolyVariantLB [] Text
tv) Type
t2 ->
      ConstraintA -> m ([ConstraintA], Map Text (InputAnn, Type))
forall (b :: * -> *) (m :: * -> *).
Solve b m =>
ConstraintA -> m ([ConstraintA], Map Text (InputAnn, Type))
solveConstraint (Type -> Type -> Constraint
Equality (Text -> Type
TypeVar Text
tv) Type
t2, InputAnn
ann)

    Equality Type
t1 (TypePolyVariantLB [] Text
tv) ->
      ConstraintA -> m ([ConstraintA], Map Text (InputAnn, Type))
forall (b :: * -> *) (m :: * -> *).
Solve b m =>
ConstraintA -> m ([ConstraintA], Map Text (InputAnn, Type))
solveConstraint (Type -> Type -> Constraint
Equality (Text -> Type
TypeVar Text
tv) Type
t1, InputAnn
ann)


    -- When all else fails, throw an error.
    Equality Type
t1 Type
t2 ->
      [InputAnn]
-> TypeError -> m ([ConstraintA], Map Text (InputAnn, Type))
forall (m :: * -> *) a.
MonadError TypeErrorA m =>
[InputAnn] -> TypeError -> m a
throwErr [InputAnn
ann] (TypeError -> m ([ConstraintA], Map Text (InputAnn, Type)))
-> TypeError -> m ([ConstraintA], Map Text (InputAnn, Type))
forall a b. (a -> b) -> a -> b
$ Type -> Type -> TypeError
TypeMismatch Type
t1 Type
t2

{- | Create an instance of a type. (The type serves as a template for specialized types)

Let polymorphism gives us the ability to use a generic function in more contexts.

For example, @id@ is a function that can work for @x@ of any type. But our algorithm
collects constraints globally, including that:

@
id = \x -> x

one = id 1          -- constrain that the type of id __is equal to__ the type [Int] -> tN

hello = id "hello"  -- constrain that the type of id __is equal to__ the type [String] -> tM
@

We need to invent a new constraint that will define the relationship between the type of id
and the arguments passing to it as an __Instance of__ relationship.

@InstanceOf t1 t2@ relationship means that @t1@ is an @instantiation@ of @t2@
(or a special case if you will).
What we'll do is copy the type of @t2@, generate new type variables in place of all type variables
inside of it, and then say that this new type @t3@ has an equality relationship with @t1@.

It's important to solve the equality constraints for each function before solving the InstanceOf
constraints, so that when we instantiate we already have the final type of the function.

We will highjack the @Ord@ instance deriving (constructors defined later are bigger)
and the fact that @Set@ is ordered to accomplish that.


-}
instantiate :: Solve b m => Text -> Type -> m (Env TypeVar, Type)
instantiate :: Text -> Type -> m (Env Text, Type)
instantiate Text
prefix Type
typ = do
  -- collect all type variables, generate a new type variable for each one
  -- replace old type variables with new ones
  Env Text
env1 <- ([(Text, Text)] -> Env Text) -> m [(Text, Text)] -> m (Env Text)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap [(Text, Text)] -> Env Text
forall k a. Ord k => [(k, a)] -> Map k a
M.fromList (m [(Text, Text)] -> m (Env Text))
-> m [(Text, Text)] -> m (Env Text)
forall a b. (a -> b) -> a -> b
$ [m (Text, Text)] -> m [(Text, Text)]
forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
sequence
    [ (,) Text
tv (Text -> (Text, Text)) -> m Text -> m (Text, Text)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Text -> m Text
forall (m :: * -> *). MonadState ElabState m => Text -> m Text
genTypeVar Text
prefix
    | TypeVar Text
tv <- Type -> [Type]
forall on. Uniplate on => on -> [on]
U.universe Type
typ
    ]
  Env Text
env2 <- ([(Text, Text)] -> Env Text) -> m [(Text, Text)] -> m (Env Text)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap [(Text, Text)] -> Env Text
forall k a. Ord k => [(k, a)] -> Map k a
M.fromList (m [(Text, Text)] -> m (Env Text))
-> m [(Text, Text)] -> m (Env Text)
forall a b. (a -> b) -> a -> b
$ [m (Text, Text)] -> m [(Text, Text)]
forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
sequence
    [ (,) Text
tv (Text -> (Text, Text)) -> m Text -> m (Text, Text)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Text -> m Text
forall (m :: * -> *). MonadState ElabState m => Text -> m Text
genTypeVar Text
prefix
    | TypeRecExt [(Text, Type)]
_ Text
tv <- Type -> [Type]
forall on. Uniplate on => on -> [on]
U.universe Type
typ
    ]
  Env Text
env3 <- ([(Text, Text)] -> Env Text) -> m [(Text, Text)] -> m (Env Text)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap [(Text, Text)] -> Env Text
forall k a. Ord k => [(k, a)] -> Map k a
M.fromList (m [(Text, Text)] -> m (Env Text))
-> m [(Text, Text)] -> m (Env Text)
forall a b. (a -> b) -> a -> b
$ [m (Text, Text)] -> m [(Text, Text)]
forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
sequence
    [ (,) Text
tv (Text -> (Text, Text)) -> m Text -> m (Text, Text)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Text -> m Text
forall (m :: * -> *). MonadState ElabState m => Text -> m Text
genTypeVar Text
prefix
    | TypePolyVariantLB [(Text, Type)]
_ Text
tv <- Type -> [Type]
forall on. Uniplate on => on -> [on]
U.universe Type
typ
    ]
  Env Text
env4 <- ([(Text, Text)] -> Env Text) -> m [(Text, Text)] -> m (Env Text)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap [(Text, Text)] -> Env Text
forall k a. Ord k => [(k, a)] -> Map k a
M.fromList (m [(Text, Text)] -> m (Env Text))
-> m [(Text, Text)] -> m (Env Text)
forall a b. (a -> b) -> a -> b
$ [m (Text, Text)] -> m [(Text, Text)]
forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
sequence
    [ (,) Text
tv (Text -> (Text, Text)) -> m Text -> m (Text, Text)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Text -> m Text
forall (m :: * -> *). MonadState ElabState m => Text -> m Text
genTypeVar Text
prefix
    | TypePolyVariantUB Text
tv [(Text, Type)]
_ <- Type -> [Type]
forall on. Uniplate on => on -> [on]
U.universe Type
typ
    ]
  let
    env :: Env Text
env = Env Text
env1 Env Text -> Env Text -> Env Text
forall a. Semigroup a => a -> a -> a
<> Env Text
env2 Env Text -> Env Text -> Env Text
forall a. Semigroup a => a -> a -> a
<> Env Text
env3 Env Text -> Env Text -> Env Text
forall a. Semigroup a => a -> a -> a
<> Env Text
env4
  (Env Text, Type) -> m (Env Text, Type)
forall (f :: * -> *) a. Applicative f => a -> f a
pure ((Env Text, Type) -> m (Env Text, Type))
-> (Env Text, Type) -> m (Env Text, Type)
forall a b. (a -> b) -> a -> b
$ (,) Env Text
env (Type -> (Env Text, Type)) -> Type -> (Env Text, Type)
forall a b. (a -> b) -> a -> b
$ ((Type -> Type) -> Type -> Type) -> Type -> (Type -> Type) -> Type
forall a b c. (a -> b -> c) -> b -> a -> c
flip (Type -> Type) -> Type -> Type
forall on. Uniplate on => (on -> on) -> on -> on
U.transform Type
typ ((Type -> Type) -> Type) -> (Type -> Type) -> Type
forall a b. (a -> b) -> a -> b
$ \case
    TypeVar Text
tv
      | Just Text
tv' <- Text -> Env Text -> Maybe Text
forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup Text
tv Env Text
env ->
        Text -> Type
TypeVar Text
tv'
    TypeRecExt [(Text, Type)]
r Text
tv
      | Just Text
tv' <- Text -> Env Text -> Maybe Text
forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup Text
tv Env Text
env ->
        [(Text, Type)] -> Text -> Type
TypeRecExt [(Text, Type)]
r Text
tv'
    TypePolyVariantLB [(Text, Type)]
variants Text
tv
      | Just Text
tv' <- Text -> Env Text -> Maybe Text
forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup Text
tv Env Text
env ->
        [(Text, Type)] -> Text -> Type
TypePolyVariantLB [(Text, Type)]
variants Text
tv'
    TypePolyVariantUB Text
tv [(Text, Type)]
variants
      | Just Text
tv' <- Text -> Env Text -> Maybe Text
forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup Text
tv Env Text
env ->
        Text -> [(Text, Type)] -> Type
TypePolyVariantUB Text
tv' [(Text, Type)]
variants
    t :: Type
t@TypeVar{} -> Type
t
    t :: Type
t@TypeCon{} -> Type
t
    t :: Type
t@TypeApp{} -> Type
t
    t :: Type
t@TypeRec{} -> Type
t
    t :: Type
t@TypeRecExt{} -> Type
t
    t :: Type
t@TypeVariant{} -> Type
t
    t :: Type
t@TypePolyVariantLB{} -> Type
t
    t :: Type
t@TypePolyVariantUB{} -> Type
t


--------------------------
-- * Substitute

{- | Apply a substitution.

-}

-- ** API

-- | Replaces all type variables for any data type that
--   has an instance of Data using uniplate magic.
--
--   Note: uniplate magic = slow.
substitute :: Substitute m => Data f => Substitution -> f -> m f
substitute :: Map Text (InputAnn, Type) -> f -> m f
substitute Map Text (InputAnn, Type)
sub
  | Map Text (InputAnn, Type) -> Bool
forall k a. Map k a -> Bool
M.null Map Text (InputAnn, Type)
sub = f -> m f
forall (f :: * -> *) a. Applicative f => a -> f a
pure
  | Bool
otherwise = (Type -> m Type) -> f -> m f
forall (m :: * -> *) from to.
(Monad m, Applicative m, Biplate from to) =>
(to -> m to) -> from -> m from
U.transformBiM (Map Text (InputAnn, Type) -> Type -> m Type
forall (m :: * -> *).
Substitute m =>
Map Text (InputAnn, Type) -> Type -> m Type
replaceTypeVar Map Text (InputAnn, Type)
sub)


-- | Replaces all type variables for constraints.
substituteConstraints :: Substitute m => Substitution -> [ConstraintA] -> m [ConstraintA]
substituteConstraints :: Map Text (InputAnn, Type) -> [ConstraintA] -> m [ConstraintA]
substituteConstraints Map Text (InputAnn, Type)
sub
  | Map Text (InputAnn, Type) -> Bool
forall k a. Map k a -> Bool
M.null Map Text (InputAnn, Type)
sub = [ConstraintA] -> m [ConstraintA]
forall (f :: * -> *) a. Applicative f => a -> f a
pure
  | Bool
otherwise =
  (ConstraintA -> m ConstraintA) -> [ConstraintA] -> m [ConstraintA]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse ((ConstraintA -> m ConstraintA)
 -> [ConstraintA] -> m [ConstraintA])
-> (ConstraintA -> m ConstraintA)
-> [ConstraintA]
-> m [ConstraintA]
forall a b. (a -> b) -> a -> b
$ \case
    (Constraint
c, InputAnn
ann) ->
      let
        onConstraint :: (Type -> Type -> Constraint) -> Type -> Type -> m ConstraintA
onConstraint Type -> Type -> Constraint
constr Type
t1 Type
t2 =
          (Constraint -> ConstraintA) -> m Constraint -> m ConstraintA
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((Constraint -> InputAnn -> ConstraintA)
-> InputAnn -> Constraint -> ConstraintA
forall a b c. (a -> b -> c) -> b -> a -> c
flip (,) InputAnn
ann) (m Constraint -> m ConstraintA) -> m Constraint -> m ConstraintA
forall a b. (a -> b) -> a -> b
$ Type -> Type -> Constraint
constr
            (Type -> Type -> Constraint) -> m Type -> m (Type -> Constraint)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Type -> m Type) -> Type -> m Type
forall (m :: * -> *) on.
(Monad m, Applicative m, Uniplate on) =>
(on -> m on) -> on -> m on
U.transformM (Map Text (InputAnn, Type) -> Type -> m Type
forall (m :: * -> *).
Substitute m =>
Map Text (InputAnn, Type) -> Type -> m Type
replaceTypeVar Map Text (InputAnn, Type)
sub) Type
t1
            m (Type -> Constraint) -> m Type -> m Constraint
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (Type -> m Type) -> Type -> m Type
forall (m :: * -> *) on.
(Monad m, Applicative m, Uniplate on) =>
(on -> m on) -> on -> m on
U.transformM (Map Text (InputAnn, Type) -> Type -> m Type
forall (m :: * -> *).
Substitute m =>
Map Text (InputAnn, Type) -> Type -> m Type
replaceTypeVar Map Text (InputAnn, Type)
sub) Type
t2
      in case Constraint
c of
        Equality Type
t1 Type
t2 ->
          (Type -> Type -> Constraint) -> Type -> Type -> m ConstraintA
onConstraint Type -> Type -> Constraint
Equality Type
t1 Type
t2
        InstanceOf Type
t1 Type
t2 ->
          (Type -> Type -> Constraint) -> Type -> Type -> m ConstraintA
onConstraint Type -> Type -> Constraint
InstanceOf Type
t1 Type
t2

-- | Replaces all type variables for substitutions.
substituteSubs :: Substitute m => Substitution -> Substitution -> m Substitution
substituteSubs :: Map Text (InputAnn, Type)
-> Map Text (InputAnn, Type) -> m (Map Text (InputAnn, Type))
substituteSubs Map Text (InputAnn, Type)
sub
  | Map Text (InputAnn, Type) -> Bool
forall k a. Map k a -> Bool
M.null Map Text (InputAnn, Type)
sub = Map Text (InputAnn, Type) -> m (Map Text (InputAnn, Type))
forall (f :: * -> *) a. Applicative f => a -> f a
pure
  | Bool
otherwise = ((InputAnn, Type) -> m (InputAnn, Type))
-> Map Text (InputAnn, Type) -> m (Map Text (InputAnn, Type))
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse (((InputAnn, Type) -> m (InputAnn, Type))
 -> Map Text (InputAnn, Type) -> m (Map Text (InputAnn, Type)))
-> ((InputAnn, Type) -> m (InputAnn, Type))
-> Map Text (InputAnn, Type)
-> m (Map Text (InputAnn, Type))
forall a b. (a -> b) -> a -> b
$ (Type -> m Type) -> (InputAnn, Type) -> m (InputAnn, Type)
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse ((Type -> m Type) -> (InputAnn, Type) -> m (InputAnn, Type))
-> (Type -> m Type) -> (InputAnn, Type) -> m (InputAnn, Type)
forall a b. (a -> b) -> a -> b
$ (Type -> m Type) -> Type -> m Type
forall (m :: * -> *) on.
(Monad m, Applicative m, Uniplate on) =>
(on -> m on) -> on -> m on
U.transformM ((Type -> m Type) -> Type -> m Type)
-> (Type -> m Type) -> Type -> m Type
forall a b. (a -> b) -> a -> b
$ Map Text (InputAnn, Type) -> Type -> m Type
forall (m :: * -> *).
Substitute m =>
Map Text (InputAnn, Type) -> Type -> m Type
replaceTypeVar Map Text (InputAnn, Type)
sub


-- ** Types

-- | Monadic capabilities of Substitute
type Substitute m
  = ( MonadError TypeErrorA m
    )

-- ** Algorithm

-- | Find type variables that appear in the substitution and replace them.
replaceTypeVar :: Substitute m => Substitution -> Type -> m Type
replaceTypeVar :: Map Text (InputAnn, Type) -> Type -> m Type
replaceTypeVar Map Text (InputAnn, Type)
sub = \case
  TypeVar Text
v ->
    m Type
-> ((InputAnn, Type) -> m Type) -> Maybe (InputAnn, Type) -> m Type
forall b a. b -> (a -> b) -> Maybe a -> b
maybe
      (Type -> m Type
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Type -> m Type) -> Type -> m Type
forall a b. (a -> b) -> a -> b
$ Text -> Type
TypeVar Text
v)
      ((InputAnn -> Type -> m Type) -> (InputAnn, Type) -> m Type
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry ((InputAnn -> Type -> m Type) -> (InputAnn, Type) -> m Type)
-> (InputAnn -> Type -> m Type) -> (InputAnn, Type) -> m Type
forall a b. (a -> b) -> a -> b
$ Text -> InputAnn -> Type -> m Type
forall (m :: * -> *).
Substitute m =>
Text -> InputAnn -> Type -> m Type
occursCheck Text
v) -- Make sure we don't have an infinite type
      (Text -> Map Text (InputAnn, Type) -> Maybe (InputAnn, Type)
forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup Text
v Map Text (InputAnn, Type)
sub)

  TypeRecExt [(Text, Type)]
r1 Text
ext
    | Just (InputAnn
ann, Type
r2) <- Text -> Map Text (InputAnn, Type) -> Maybe (InputAnn, Type)
forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup Text
ext Map Text (InputAnn, Type)
sub -> do
      m Type -> m ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void (m Type -> m ()) -> m Type -> m ()
forall a b. (a -> b) -> a -> b
$ Text -> InputAnn -> Type -> m Type
forall (m :: * -> *).
Substitute m =>
Text -> InputAnn -> Type -> m Type
occursCheck Text
ext InputAnn
ann Type
r2
      InputAnn -> [(Text, Type)] -> Type -> m Type
forall (m :: * -> *).
Substitute m =>
InputAnn -> [(Text, Type)] -> Type -> m Type
mergeRecords InputAnn
ann [(Text, Type)]
r1 Type
r2

  -- if the hidden type variable name is change we change it here as well
  TypePolyVariantUB Text
tv [(Text, Type)]
vars
    | Just (InputAnn
_, TypeVar Text
tv') <- Text -> Map Text (InputAnn, Type) -> Maybe (InputAnn, Type)
forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup Text
tv Map Text (InputAnn, Type)
sub -> do
      Type -> m Type
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Type -> m Type) -> Type -> m Type
forall a b. (a -> b) -> a -> b
$ Text -> [(Text, Type)] -> Type
TypePolyVariantUB Text
tv' [(Text, Type)]
vars

  TypePolyVariantUB Text
tv [(Text, Type)]
vars1
    | Just (InputAnn
ann, Type
vars2) <- Text -> Map Text (InputAnn, Type) -> Maybe (InputAnn, Type)
forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup Text
tv Map Text (InputAnn, Type)
sub -> do
       -- @TODO occursCheck ?
      InputAnn -> [(Text, Type)] -> Type -> m Type
forall (m :: * -> *).
Substitute m =>
InputAnn -> [(Text, Type)] -> Type -> m Type
mergeVariants InputAnn
ann [(Text, Type)]
vars1 Type
vars2

  -- this case represents a normal TypeVar
  TypePolyVariantLB [] Text
tv
    | Just (InputAnn
_, Type
t) <- Text -> Map Text (InputAnn, Type) -> Maybe (InputAnn, Type)
forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup Text
tv Map Text (InputAnn, Type)
sub -> do
      Type -> m Type
forall (f :: * -> *) a. Applicative f => a -> f a
pure Type
t

  TypePolyVariantLB [(Text, Type)]
vars1 Text
tv
    | Just (InputAnn
ann, Type
vars2) <- Text -> Map Text (InputAnn, Type) -> Maybe (InputAnn, Type)
forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup Text
tv Map Text (InputAnn, Type)
sub -> do
       -- @TODO occursCheck ?
      InputAnn -> [(Text, Type)] -> Type -> m Type
forall (m :: * -> *).
Substitute m =>
InputAnn -> [(Text, Type)] -> Type -> m Type
mergeVariants InputAnn
ann [(Text, Type)]
vars1 Type
vars2

  t :: Type
t@TypeCon{} -> Type -> m Type
forall (f :: * -> *) a. Applicative f => a -> f a
pure Type
t
  t :: Type
t@TypeApp{} -> Type -> m Type
forall (f :: * -> *) a. Applicative f => a -> f a
pure Type
t
  t :: Type
t@TypeRec{} -> Type -> m Type
forall (f :: * -> *) a. Applicative f => a -> f a
pure Type
t
  t :: Type
t@TypeRecExt{} -> Type -> m Type
forall (f :: * -> *) a. Applicative f => a -> f a
pure Type
t
  t :: Type
t@TypeVariant{} -> Type -> m Type
forall (f :: * -> *) a. Applicative f => a -> f a
pure Type
t
  t :: Type
t@TypePolyVariantLB{} -> Type -> m Type
forall (f :: * -> *) a. Applicative f => a -> f a
pure Type
t
  t :: Type
t@TypePolyVariantUB{} -> Type -> m Type
forall (f :: * -> *) a. Applicative f => a -> f a
pure Type
t

-- Merging two open variants
mergeVariants :: Substitute m => InputAnn -> [(Label, Type)] -> Type -> m Type
mergeVariants :: InputAnn -> [(Text, Type)] -> Type -> m Type
mergeVariants InputAnn
ann [(Text, Type)]
vars1 = \case
  TypePolyVariantLB [(Text, Type)]
vars2 Text
tv ->
    Type -> m Type
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Type -> m Type) -> (Env Type -> Type) -> Env Type -> m Type
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ([(Text, Type)] -> Text -> Type) -> Text -> [(Text, Type)] -> Type
forall a b c. (a -> b -> c) -> b -> a -> c
flip [(Text, Type)] -> Text -> Type
TypePolyVariantLB Text
tv ([(Text, Type)] -> Type)
-> (Env Type -> [(Text, Type)]) -> Env Type -> Type
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Env Type -> [(Text, Type)]
forall k a. Map k a -> [(k, a)]
M.toList (Env Type -> m Type) -> Env Type -> m Type
forall a b. (a -> b) -> a -> b
$ (Type -> Type -> Type) -> [(Text, Type)] -> Env Type
forall k a. Ord k => (a -> a -> a) -> [(k, a)] -> Map k a
M.fromListWith ((Type -> Type -> Type) -> Type -> Type -> Type
forall a b c. (a -> b -> c) -> b -> a -> c
flip Type -> Type -> Type
forall a b. a -> b -> a
const) ([(Text, Type)]
vars1 [(Text, Type)] -> [(Text, Type)] -> [(Text, Type)]
forall a. Semigroup a => a -> a -> a
<> [(Text, Type)]
vars2)
  TypePolyVariantUB Text
tv [(Text, Type)]
vars2 ->
    Type -> m Type
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Type -> m Type) -> (Env Type -> Type) -> Env Type -> m Type
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Text -> [(Text, Type)] -> Type
TypePolyVariantUB Text
tv ([(Text, Type)] -> Type)
-> (Env Type -> [(Text, Type)]) -> Env Type -> Type
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Env Type -> [(Text, Type)]
forall k a. Map k a -> [(k, a)]
M.toList (Env Type -> m Type) -> Env Type -> m Type
forall a b. (a -> b) -> a -> b
$ (Type -> Type -> Type) -> [(Text, Type)] -> Env Type
forall k a. Ord k => (a -> a -> a) -> [(k, a)] -> Map k a
M.fromListWith ((Type -> Type -> Type) -> Type -> Type -> Type
forall a b c. (a -> b -> c) -> b -> a -> c
flip Type -> Type -> Type
forall a b. a -> b -> a
const) ([(Text, Type)]
vars1 [(Text, Type)] -> [(Text, Type)] -> [(Text, Type)]
forall a. Semigroup a => a -> a -> a
<> [(Text, Type)]
vars2)
  TypeVariant [(Text, Type)]
vars2 ->
    Type -> m Type
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Type -> m Type) -> (Env Type -> Type) -> Env Type -> m Type
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [(Text, Type)] -> Type
TypeVariant ([(Text, Type)] -> Type)
-> (Env Type -> [(Text, Type)]) -> Env Type -> Type
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Env Type -> [(Text, Type)]
forall k a. Map k a -> [(k, a)]
M.toList (Env Type -> m Type) -> Env Type -> m Type
forall a b. (a -> b) -> a -> b
$ (Type -> Type -> Type) -> [(Text, Type)] -> Env Type
forall k a. Ord k => (a -> a -> a) -> [(k, a)] -> Map k a
M.fromListWith ((Type -> Type -> Type) -> Type -> Type -> Type
forall a b c. (a -> b -> c) -> b -> a -> c
flip Type -> Type -> Type
forall a b. a -> b -> a
const) ([(Text, Type)]
vars1 [(Text, Type)] -> [(Text, Type)] -> [(Text, Type)]
forall a. Semigroup a => a -> a -> a
<> [(Text, Type)]
vars2)
  Type
t ->
    [InputAnn] -> TypeError -> m Type
forall (m :: * -> *) a.
MonadError TypeErrorA m =>
[InputAnn] -> TypeError -> m a
throwErr [InputAnn
ann] (TypeError -> m Type) -> TypeError -> m Type
forall a b. (a -> b) -> a -> b
$ Type -> TypeError
NotAVariant Type
t


mergeRecords :: Substitute m => InputAnn -> [(Label, Type)] -> Type -> m Type
mergeRecords :: InputAnn -> [(Text, Type)] -> Type -> m Type
mergeRecords InputAnn
ann [(Text, Type)]
r1 = \case
  TypeRec [(Text, Type)]
r2 ->
    Type -> m Type
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Type -> m Type) -> (Env Type -> Type) -> Env Type -> m Type
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [(Text, Type)] -> Type
TypeRec ([(Text, Type)] -> Type)
-> (Env Type -> [(Text, Type)]) -> Env Type -> Type
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Env Type -> [(Text, Type)]
forall k a. Map k a -> [(k, a)]
M.toList (Env Type -> m Type) -> Env Type -> m Type
forall a b. (a -> b) -> a -> b
$ (Type -> Type -> Type) -> [(Text, Type)] -> Env Type
forall k a. Ord k => (a -> a -> a) -> [(k, a)] -> Map k a
M.fromListWith ((Type -> Type -> Type) -> Type -> Type -> Type
forall a b c. (a -> b -> c) -> b -> a -> c
flip Type -> Type -> Type
forall a b. a -> b -> a
const) ([(Text, Type)]
r1 [(Text, Type)] -> [(Text, Type)] -> [(Text, Type)]
forall a. Semigroup a => a -> a -> a
<> [(Text, Type)]
r2)
  TypeVar Text
ext' ->
    Type -> m Type
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Type -> m Type) -> Type -> m Type
forall a b. (a -> b) -> a -> b
$ [(Text, Type)] -> Text -> Type
TypeRecExt [(Text, Type)]
r1 Text
ext'
  TypeRecExt [(Text, Type)]
r2 Text
ext ->
    Type -> m Type
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Type -> m Type) -> (Env Type -> Type) -> Env Type -> m Type
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ([(Text, Type)] -> Text -> Type) -> Text -> [(Text, Type)] -> Type
forall a b c. (a -> b -> c) -> b -> a -> c
flip [(Text, Type)] -> Text -> Type
TypeRecExt Text
ext ([(Text, Type)] -> Type)
-> (Env Type -> [(Text, Type)]) -> Env Type -> Type
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Env Type -> [(Text, Type)]
forall k a. Map k a -> [(k, a)]
M.toList (Env Type -> m Type) -> Env Type -> m Type
forall a b. (a -> b) -> a -> b
$ (Type -> Type -> Type) -> [(Text, Type)] -> Env Type
forall k a. Ord k => (a -> a -> a) -> [(k, a)] -> Map k a
M.fromListWith ((Type -> Type -> Type) -> Type -> Type -> Type
forall a b c. (a -> b -> c) -> b -> a -> c
flip Type -> Type -> Type
forall a b. a -> b -> a
const) ([(Text, Type)]
r1 [(Text, Type)] -> [(Text, Type)] -> [(Text, Type)]
forall a. Semigroup a => a -> a -> a
<> [(Text, Type)]
r2)
  Type
t ->
    [InputAnn] -> TypeError -> m Type
forall (m :: * -> *) a.
MonadError TypeErrorA m =>
[InputAnn] -> TypeError -> m a
throwErr [InputAnn
ann] (TypeError -> m Type) -> TypeError -> m Type
forall a b. (a -> b) -> a -> b
$ Type -> TypeError
NotARecord Type
t

-- | protect against infinite types
occursCheck :: Substitute m => TypeVar -> InputAnn -> Type -> m Type
occursCheck :: Text -> InputAnn -> Type -> m Type
occursCheck Text
v InputAnn
ann = \case
  TypeVar Text
v'
    | Text
v Text -> Text -> Bool
forall a. Eq a => a -> a -> Bool
== Text
v' ->
      Type -> m Type
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Type -> m Type) -> Type -> m Type
forall a b. (a -> b) -> a -> b
$ Text -> Type
TypeVar Text
v'
  -- types that contain the type variable we are trying to replace
  -- are forbidden
  Type
t -> do
    let
      tvars :: [()]
tvars = [ () | TypeVar Text
tv <- Type -> [Type]
forall on. Uniplate on => on -> [on]
U.universe Type
t, Text
tv Text -> Text -> Bool
forall a. Eq a => a -> a -> Bool
== Text
v ]
    Bool -> m () -> m ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless ([()] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [()]
tvars) (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$ [InputAnn] -> TypeError -> m ()
forall (m :: * -> *) a.
MonadError TypeErrorA m =>
[InputAnn] -> TypeError -> m a
throwErr [InputAnn
ann] (TypeError -> m ()) -> TypeError -> m ()
forall a b. (a -> b) -> a -> b
$ Text -> Type -> TypeError
InfiniteType Text
v Type
t
    Type -> m Type
forall (f :: * -> *) a. Applicative f => a -> f a
pure Type
t

-- * Utils

data Matches a b
  = OnlyLeft a
  | OnlyRight a
  | BothSides b

unzipMatches :: [Matches a b] -> ([a], [a], [b])
unzipMatches :: [Matches a b] -> ([a], [a], [b])
unzipMatches = \case
  [] -> ([], [], [])
  Matches a b
current : [Matches a b]
rest ->
    let
      ([a]
lefts, [a]
rights, [b]
both) = [Matches a b] -> ([a], [a], [b])
forall a b. [Matches a b] -> ([a], [a], [b])
unzipMatches [Matches a b]
rest
    in case Matches a b
current of
      OnlyLeft a
x ->
        (a
x a -> [a] -> [a]
forall a. a -> [a] -> [a]
: [a]
lefts, [a]
rights, [b]
both)
      OnlyRight a
x ->
        ([a]
lefts, a
x a -> [a] -> [a]
forall a. a -> [a] -> [a]
: [a]
rights, [b]
both)
      BothSides b
x ->
        ([a]
lefts, [a]
rights, b
x b -> [b] -> [b]
forall a. a -> [a] -> [a]
: [b]
both)
      
      

-- * Pretty printing

ppShow :: Pretty ann => Functor f => Show (f Text) => f ann -> Text
ppShow :: f ann -> Text
ppShow = f Text -> Text
forall a. Show a => a -> Text
pShow (f Text -> Text) -> (f ann -> f Text) -> f ann -> Text
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (ann -> Text) -> f ann -> f Text
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Doc Any -> Text
forall a. Doc a -> Text
render (Doc Any -> Text) -> (ann -> Doc Any) -> ann -> Text
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ann -> Doc Any
forall a ann. Pretty a => a -> Doc ann
pretty)

ppShowC :: Constraint -> Text
ppShowC :: Constraint -> Text
ppShowC = Doc Any -> Text
forall a. Doc a -> Text
render (Doc Any -> Text) -> (Constraint -> Doc Any) -> Constraint -> Text
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Constraint -> Doc Any
forall ann. Constraint -> Doc ann
ppConstraint

ppShowCs :: Show (f Text) => Functor f => f Constraint -> Text
ppShowCs :: f Constraint -> Text
ppShowCs = f Text -> Text
forall a. Show a => a -> Text
pShow (f Text -> Text)
-> (f Constraint -> f Text) -> f Constraint -> Text
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Constraint -> Text) -> f Constraint -> f Text
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Doc Any -> Text
forall a. Doc a -> Text
render (Doc Any -> Text) -> (Constraint -> Doc Any) -> Constraint -> Text
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Constraint -> Doc Any
forall ann. Constraint -> Doc ann
ppConstraint)

ppShowCAss :: [Set ConstraintA] -> Text
ppShowCAss :: [Set ConstraintA] -> Text
ppShowCAss = [Set Text] -> Text
forall a. Show a => a -> Text
pShow ([Set Text] -> Text)
-> ([Set ConstraintA] -> [Set Text]) -> [Set ConstraintA] -> Text
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Set ConstraintA -> Set Text) -> [Set ConstraintA] -> [Set Text]
forall a b. (a -> b) -> [a] -> [b]
map ((ConstraintA -> Text) -> Set ConstraintA -> Set Text
forall b a. Ord b => (a -> b) -> Set a -> Set b
S.map (Doc Any -> Text
forall a. Doc a -> Text
render (Doc Any -> Text)
-> (ConstraintA -> Doc Any) -> ConstraintA -> Text
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Constraint -> Doc Any
forall ann. Constraint -> Doc ann
ppConstraint (Constraint -> Doc Any)
-> (ConstraintA -> Constraint) -> ConstraintA -> Doc Any
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ConstraintA -> Constraint
forall a b. (a, b) -> a
fst))

ppShowCAs :: Show (f Text) => Functor f => f ConstraintA -> Text
ppShowCAs :: f ConstraintA -> Text
ppShowCAs = f Text -> Text
forall a. Show a => a -> Text
pShow (f Text -> Text)
-> (f ConstraintA -> f Text) -> f ConstraintA -> Text
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (ConstraintA -> Text) -> f ConstraintA -> f Text
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Doc Any -> Text
forall a. Doc a -> Text
render (Doc Any -> Text)
-> (ConstraintA -> Doc Any) -> ConstraintA -> Text
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Constraint -> Doc Any
forall ann. Constraint -> Doc ann
ppConstraint (Constraint -> Doc Any)
-> (ConstraintA -> Constraint) -> ConstraintA -> Doc Any
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ConstraintA -> Constraint
forall a b. (a, b) -> a
fst)

printAnn :: Ann -> Text
printAnn :: Ann -> Text
printAnn = Doc Any -> Text
forall a. Doc a -> Text
render (Doc Any -> Text) -> (Ann -> Doc Any) -> Ann -> Text
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Ann -> Doc Any
forall a ann. Pretty a => a -> Doc ann
pretty

ppAnn :: Ann -> Doc ann
ppAnn :: Ann -> Doc ann
ppAnn (Ann InputAnn
src Type
typ) = [Doc ann] -> Doc ann
forall ann. [Doc ann] -> Doc ann
braced' [InputAnn -> Doc ann
forall ann. InputAnn -> Doc ann
ppSourcePos InputAnn
src, Type -> Doc ann
forall ann. Type -> Doc ann
ppType Type
typ]

ppConstraint :: Constraint -> Doc ann
ppConstraint :: Constraint -> Doc ann
ppConstraint = \case
  Equality Type
t1 Type
t2 -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann
align (Doc ann -> Doc ann) -> Doc ann -> Doc ann
forall a b. (a -> b) -> a -> b
$ Type -> Doc ann
forall ann. Type -> Doc ann
ppType Type
t1 Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ann
"~" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Type -> Doc ann
forall ann. Type -> Doc ann
ppType Type
t2
  InstanceOf Type
t1 Type
t2 -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann
align (Doc ann -> Doc ann) -> Doc ann -> Doc ann
forall a b. (a -> b) -> a -> b
$ Type -> Doc ann
forall ann. Type -> Doc ann
ppType Type
t1 Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ann
":~" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Type -> Doc ann
forall ann. Type -> Doc ann
ppType Type
t2

instance Pretty Parser.SourcePos where
  pretty :: InputAnn -> Doc ann
pretty = InputAnn -> Doc ann
forall ann. InputAnn -> Doc ann
ppSourcePos
instance Pretty Ann where
  pretty :: Ann -> Doc ann
pretty = Ann -> Doc ann
forall ann. Ann -> Doc ann
ppAnn
instance Pretty Type where
  pretty :: Type -> Doc ann
pretty = Type -> Doc ann
forall ann. Type -> Doc ann
ppType
instance Pretty Constraint where
  pretty :: Constraint -> Doc ann
pretty = Constraint -> Doc ann
forall ann. Constraint -> Doc ann
ppConstraint

ppTypeError :: TypeErrorA -> Text
ppTypeError :: TypeErrorA -> Text
ppTypeError ([InputAnn]
srcs, TypeError
typeErr) =
  [Text] -> Text
T.unlines
    [ Text
"*** Error from: " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text -> [Text] -> Text
T.intercalate Text
", and " ((InputAnn -> Text) -> [InputAnn] -> [Text]
forall a b. (a -> b) -> [a] -> [b]
map (Doc Any -> Text
forall a. Doc a -> Text
render (Doc Any -> Text) -> (InputAnn -> Doc Any) -> InputAnn -> Text
forall b c a. (b -> c) -> (a -> b) -> a -> c
. InputAnn -> Doc Any
forall ann. InputAnn -> Doc ann
ppSourcePos) [InputAnn]
srcs)
    , TypeError -> Text
forall a. Show a => a -> Text
pShow TypeError
typeErr
    ]