{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeSynonymInstances #-}
{-# OPTIONS_GHC -fno-warn-orphans #-}

module Inferno.Infer
  ( Constraint,
    TypeError (..),
    Subst (..),
    inferExpr,
    closeOver,
    closeOverType,
    findTypeClassWitnesses,
    inferTypeReps,
    inferPossibleTypes,
  )
where

import Control.Monad (when)
import Control.Monad.Except
  ( Except,
    ExceptT,
    MonadError (catchError, throwError),
    foldM,
    forM,
    forM_,
    runExcept,
    runExceptT,
  )
import Control.Monad.Identity (Identity (runIdentity))
import Control.Monad.Reader
  ( MonadReader (ask, local),
    ReaderT (ReaderT, runReaderT),
  )
import Control.Monad.State
  ( MonadState (get, put, state),
    StateT (StateT, runStateT),
    evalStateT,
    execState,
    modify,
  )
import Data.Bifunctor (bimap)
import qualified Data.Bimap as Bimap
import Data.Either (partitionEithers, rights)
import Data.Generics.Product (HasType, getTyped, setTyped)
import Data.List (find, unzip4) -- intercalate
import qualified Data.List.NonEmpty as NEList
import qualified Data.Map as Map
import qualified Data.Map.Merge.Lazy as Map
import Data.Maybe (catMaybes, fromJust)
import qualified Data.Set as Set
import qualified Data.Text as Text
import Debug.Trace (trace)
import Inferno.Infer.Env (Env (..), TypeMetadata (..), closeOver, closeOverType)
import qualified Inferno.Infer.Env as Env
import Inferno.Infer.Error (TypeError (..), getLocFromErrs, getTypeClassFromErrs)
import Inferno.Infer.Exhaustiveness
  ( Pattern (..),
    cEmpty,
    cEnum,
    cInf,
    cOne,
    cTuple,
    checkUsefullness,
    exhaustive,
    mkEnumText,
  )
import Inferno.Module.Builtin (builtinModule, emptyHash, oneHash)
import Inferno.Types.Module (Module (..), PinnedModule, pinnedModuleHashToTy)
import Inferno.Types.Syntax
  ( BlockUtils (blockPosition, removeComments),
    ElementPosition (elementPosition),
    Expr (..),
    ExtIdent (..),
    Ident (..),
    ImplExpl (Expl, Impl),
    Lit (LDouble, LHex, LInt, LText),
    ModuleName (..),
    Pat (..),
    Scoped (..),
    fromEitherList,
    fromScoped,
    incSourceCol,
    patternToExpr,
    substInternalIdents,
    tListFromList,
    tListToList,
    toEitherList,
  )
import Inferno.Types.Type
  ( BaseType (TEnum),
    ImplType (..),
    InfernoType (..),
    Subst (..),
    Substitutable (..),
    TCScheme (..),
    TV,
    TypeClass (TypeClass),
    typeBool,
    typeDouble,
    typeInt,
    typeText,
    typeWord64,
    var,
    (.->),
  )
import Inferno.Types.VersionControl (Pinned (..), VCObjectHash, pinnedToMaybe, vcHash)
-- import Inferno.Utils.Prettyprinter (renderPretty)
-- import Prettyprinter (pretty)
import qualified Picosat
import System.IO.Unsafe (unsafePerformIO)
import Text.Megaparsec (SourcePos (..), initialPos)

-------------------------------------------------------------------------------
-- Classes
-------------------------------------------------------------------------------

-- | Inference monad
type Infer a =
  ( ReaderT
      Env -- Typing environment
      ( StateT -- Inference state
          InferState
          ( Except -- Inference errors
              [TypeError SourcePos]
          )
      )
      a -- Result
  )

-- | Inference state
data InferState = InferState
  { InferState -> Int
count :: Int,
    InferState
-> Map
     (Location SourcePos) (TypeMetadata (Set TypeClass, ImplType))
typeMap :: Map.Map (Location SourcePos) (TypeMetadata (Set.Set TypeClass, ImplType)),
    InferState -> Map ModuleName (Module ())
modules :: Map.Map ModuleName (Module ()),
    InferState -> Set TypeClass
typeClasses :: Set.Set TypeClass,
    InferState
-> [(Location SourcePos, [Pat (Pinned VCObjectHash) SourcePos])]
patternsToCheck :: [(Location SourcePos, [Pat (Pinned VCObjectHash) SourcePos])]
  }

-- | Initial inference state
initInfer :: InferState
initInfer :: InferState
initInfer = InferState {count :: Int
count = Int
0, typeMap :: Map (Location SourcePos) (TypeMetadata (Set TypeClass, ImplType))
typeMap = forall k a. Map k a
Map.empty, modules :: Map ModuleName (Module ())
modules = forall k a. Map k a
Map.empty, typeClasses :: Set TypeClass
typeClasses = forall a. Set a
Set.empty, patternsToCheck :: [(Location SourcePos, [Pat (Pinned VCObjectHash) SourcePos])]
patternsToCheck = []}

type Constraint = Either (InfernoType, InfernoType, [TypeError SourcePos]) (Location SourcePos, TypeClass)

type Unifier = (Subst, [Constraint])

-- | Constraint solver monad
type Solve a = ReaderT (Set.Set TypeClass) (ExceptT [TypeError SourcePos] Identity) a

type SolveState st a = ReaderT (Set.Set TypeClass) (StateT st (ExceptT [TypeError SourcePos] Identity)) a

type Location a = (a, a)

instance Substitutable Constraint where
  apply :: Subst -> Constraint -> Constraint
apply Subst
s (Left (InfernoType
t1, InfernoType
t2, [TypeError SourcePos]
es)) = forall a b. a -> Either a b
Left (forall a. Substitutable a => Subst -> a -> a
apply Subst
s InfernoType
t1, forall a. Substitutable a => Subst -> a -> a
apply Subst
s InfernoType
t2, [TypeError SourcePos]
es)
  apply Subst
s (Right (Location SourcePos
loc, TypeClass
tc)) = forall a b. b -> Either a b
Right (Location SourcePos
loc, forall a. Substitutable a => Subst -> a -> a
apply Subst
s TypeClass
tc)
  ftv :: Constraint -> Set TV
ftv (Left (InfernoType
t1, InfernoType
t2, [TypeError SourcePos]
_)) = forall a. Substitutable a => a -> Set TV
ftv InfernoType
t1 forall a. Ord a => Set a -> Set a -> Set a
`Set.union` forall a. Substitutable a => a -> Set TV
ftv InfernoType
t2
  ftv (Right (Location SourcePos
_, TypeClass
tc)) = forall a. Substitutable a => a -> Set TV
ftv TypeClass
tc

-------------------------------------------------------------------------------
-- Inference
-------------------------------------------------------------------------------

filterInstantiatedTypeClasses :: Set.Set TypeClass -> Set.Set TypeClass
filterInstantiatedTypeClasses :: Set TypeClass -> Set TypeClass
filterInstantiatedTypeClasses = forall a. (a -> Bool) -> Set a -> Set a
Set.filter forall a b. (a -> b) -> a -> b
$ Bool -> Bool
not forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Set a -> Bool
Set.null forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Substitutable a => a -> Set TV
ftv

mkPattern :: Pat (Pinned VCObjectHash) a -> Pattern
mkPattern :: forall a. Pat (Pinned VCObjectHash) a -> Pattern
mkPattern = \case
  PVar a
_ Maybe Ident
_ -> Pattern
W
  PEnum a
_ Pinned VCObjectHash
Local Scoped ModuleName
_ns Ident
_ident -> forall a. HasCallStack => [Char] -> a
error forall a b. (a -> b) -> a -> b
$ [Char]
"internal error. cannot convert unpinned enum into a pattern"
  PEnum a
_ Pinned VCObjectHash
hash Scoped ModuleName
_ns ident :: Ident
ident@(Ident Text
i) -> VCObjectHash -> Text -> Pattern
cEnum (forall obj. VCHashUpdate obj => obj -> VCObjectHash
vcHash (Ident
ident, forall a. HasCallStack => Maybe a -> a
fromJust forall a b. (a -> b) -> a -> b
$ Pinned VCObjectHash -> Maybe VCObjectHash
pinnedToMaybe Pinned VCObjectHash
hash)) Text
i
  PLit a
_ Lit
l -> case Lit
l of
    LInt Int64
v -> forall a. (Show a, Pretty a, Enum a) => a -> Pattern
cInf Int64
v
    LDouble Double
v -> forall a. (Show a, Pretty a, Enum a) => a -> Pattern
cInf Double
v
    LHex Word64
v -> forall a. (Show a, Pretty a, Enum a) => a -> Pattern
cInf Word64
v
    LText Text
v -> forall a. (Show a, Pretty a, Enum a) => a -> Pattern
cInf forall a b. (a -> b) -> a -> b
$ Text -> EnumText
mkEnumText Text
v
  POne a
_ Pat (Pinned VCObjectHash) a
p -> Pattern -> Pattern
cOne forall a b. (a -> b) -> a -> b
$ forall a. Pat (Pinned VCObjectHash) a -> Pattern
mkPattern Pat (Pinned VCObjectHash) a
p
  PEmpty a
_ -> Pattern
cEmpty
  PTuple a
_ TList (Pat (Pinned VCObjectHash) a, Maybe a)
ps a
_ -> [Pattern] -> Pattern
cTuple forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map (forall a. Pat (Pinned VCObjectHash) a -> Pattern
mkPattern forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> a
fst) forall a b. (a -> b) -> a -> b
$ forall a. TList a -> [a]
tListToList TList (Pat (Pinned VCObjectHash) a, Maybe a)
ps
  PCommentAbove Comment a
_ Pat (Pinned VCObjectHash) a
p -> forall a. Pat (Pinned VCObjectHash) a -> Pattern
mkPattern Pat (Pinned VCObjectHash) a
p
  PCommentAfter Pat (Pinned VCObjectHash) a
p Comment a
_ -> forall a. Pat (Pinned VCObjectHash) a -> Pattern
mkPattern Pat (Pinned VCObjectHash) a
p
  PCommentBelow Pat (Pinned VCObjectHash) a
p Comment a
_ -> forall a. Pat (Pinned VCObjectHash) a -> Pattern
mkPattern Pat (Pinned VCObjectHash) a
p

checkExhaustivenessAndUsefullness :: Map.Map VCObjectHash (Set.Set (VCObjectHash, Text.Text)) -> Location SourcePos -> [Pat (Pinned VCObjectHash) SourcePos] -> [TypeError SourcePos]
checkExhaustivenessAndUsefullness :: Map VCObjectHash (Set (VCObjectHash, Text))
-> Location SourcePos
-> [Pat (Pinned VCObjectHash) SourcePos]
-> [TypeError SourcePos]
checkExhaustivenessAndUsefullness Map VCObjectHash (Set (VCObjectHash, Text))
enum_sigs Location SourcePos
loc [Pat (Pinned VCObjectHash) SourcePos]
patts =
  let patternsOfPatts :: [[Pattern]]
patternsOfPatts = forall a b. (a -> b) -> [a] -> [b]
map ((forall a. a -> [a] -> [a]
: []) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Pat (Pinned VCObjectHash) a -> Pattern
mkPattern) [Pat (Pinned VCObjectHash) SourcePos]
patts
   in case Map VCObjectHash (Set (VCObjectHash, Text))
-> [[Pattern]] -> Maybe [Pattern]
exhaustive Map VCObjectHash (Set (VCObjectHash, Text))
enum_sigs [[Pattern]]
patternsOfPatts of
        Just [Pattern]
ps -> [forall a. Pattern -> Location a -> TypeError a
NonExhaustivePatternMatch Pattern
p Location SourcePos
loc | Pattern
p <- [Pattern]
ps]
        Maybe [Pattern]
Nothing ->
          let uErrs :: [(Int, Int)]
uErrs = Map VCObjectHash (Set (VCObjectHash, Text))
-> [[Pattern]] -> [(Int, Int)]
checkUsefullness Map VCObjectHash (Set (VCObjectHash, Text))
enum_sigs [[Pattern]]
patternsOfPatts
           in forall a b. (a -> b) -> [a] -> [b]
map
                ( \(Int
i, Int
j) ->
                    let loc' :: Location SourcePos
loc' = forall (f :: * -> *).
BlockUtils f =>
f SourcePos -> Location SourcePos
blockPosition forall a b. (a -> b) -> a -> b
$ [Pat (Pinned VCObjectHash) SourcePos]
patts forall a. [a] -> Int -> a
!! Int
i
                     in let pat :: Pat (Pinned VCObjectHash) SourcePos
pat = [Pat (Pinned VCObjectHash) SourcePos]
patts forall a. [a] -> Int -> a
!! Int
j
                         in if Int
i forall a. Eq a => a -> a -> Bool
== Int
j then forall a.
Maybe (Pat (Pinned VCObjectHash) a) -> Location a -> TypeError a
UselessPattern forall a. Maybe a
Nothing Location SourcePos
loc' else forall a.
Maybe (Pat (Pinned VCObjectHash) a) -> Location a -> TypeError a
UselessPattern (forall a. a -> Maybe a
Just Pat (Pinned VCObjectHash) SourcePos
pat) Location SourcePos
loc'
                )
                [(Int, Int)]
uErrs

-- | Run the inference monad
runInfer :: Env -> Set.Set TypeClass -> Map.Map ModuleName (Module m) -> Infer r -> Either [TypeError SourcePos] (r, InferState)
runInfer :: forall m r.
Env
-> Set TypeClass
-> Map ModuleName (Module m)
-> Infer r
-> Either [TypeError SourcePos] (r, InferState)
runInfer Env
env Set TypeClass
allClasses Map ModuleName (Module m)
allModules Infer r
m =
  forall e a. Except e a -> Either e a
runExcept forall a b. (a -> b) -> a -> b
$
    forall s (m :: * -> *) a. StateT s m a -> s -> m (a, s)
runStateT
      (forall r (m :: * -> *) a. ReaderT r m a -> r -> m a
runReaderT Infer r
m Env
env)
      InferState
initInfer
        { modules :: Map ModuleName (Module ())
modules = forall a b k. (a -> b) -> Map k a -> Map k b
Map.map (\Module m
m' -> Module m
m' {moduleObjects :: ()
moduleObjects = ()}) Map ModuleName (Module m)
allModules,
          typeClasses :: Set TypeClass
typeClasses = Set TypeClass
allClasses
        }

-- Given a map of implicit types containing `rep of <ty>` variables, and an expression `e`
-- we want to either substitute any implicit variable `?var$n : rep of <ty>` with a `RuntimeRep <ty>`,
-- provided that `<ty>` contains no free variables
-- otherwise we want to create a closure `fun var$n -> e[var$n/?var$n]`
closeOverTypeReps :: Map.Map ExtIdent InfernoType -> Expr (Pinned VCObjectHash) SourcePos -> (Maybe TypeClass, Map.Map ExtIdent InfernoType, Expr (Pinned VCObjectHash) SourcePos)
closeOverTypeReps :: Map ExtIdent InfernoType
-> Expr (Pinned VCObjectHash) SourcePos
-> (Maybe TypeClass, Map ExtIdent InfernoType,
    Expr (Pinned VCObjectHash) SourcePos)
closeOverTypeReps Map ExtIdent InfernoType
implTys Expr (Pinned VCObjectHash) SourcePos
expr =
  let (Map ExtIdent InfernoType
tReps, Map ExtIdent InfernoType
rest) = forall a b c. (a -> b -> c) -> b -> a -> c
flip forall a k. (a -> Bool) -> Map k a -> (Map k a, Map k a)
Map.partition Map ExtIdent InfernoType
implTys forall a b. (a -> b) -> a -> b
$ \case
        TRep InfernoType
_ -> Bool
True
        InfernoType
_ -> Bool
False
   in if forall k a. Map k a -> Bool
Map.null Map ExtIdent InfernoType
tReps
        then (forall a. Maybe a
Nothing, Map ExtIdent InfernoType
implTys, Expr (Pinned VCObjectHash) SourcePos
expr)
        else
          let -- we partition the types to those that have been fully inferred and ones where we are lacking the type-rep information
              (Map ExtIdent InfernoType
fullyInstantiated, Map ExtIdent InfernoType
withTypeHole) = forall a k. (a -> Bool) -> Map k a -> (Map k a, Map k a)
Map.partition (forall a. Set a -> Bool
Set.null forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Substitutable a => a -> Set TV
ftv) Map ExtIdent InfernoType
tReps
              -- next, we create a Map Int (Either Int InfernoType) where all the fully instantiated `TRep ty`s get mapped to a `Right ty`
              fullyInstantiatedMap :: Map Int (Either a InfernoType)
fullyInstantiatedMap =
                forall k a b. (k -> a -> b -> b) -> b -> Map k a -> b
Map.foldrWithKey
                  ( \ExtIdent
k InfernoType
v Map Int (Either a InfernoType)
m -> case (ExtIdent
k, InfernoType
v) of
                      (ExtIdent (Left Int
i), TRep InfernoType
ty) -> forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert Int
i (forall a b. b -> Either a b
Right InfernoType
ty) Map Int (Either a InfernoType)
m
                      (ExtIdent, InfernoType)
_ -> Map Int (Either a InfernoType)
m
                  )
                  forall a. Monoid a => a
mempty
                  Map ExtIdent InfernoType
fullyInstantiated

              -- we group all the types with holes
              withTypeHoleGrouped :: [NonEmpty (ExtIdent, InfernoType)]
withTypeHoleGrouped = forall (f :: * -> *) a.
Foldable f =>
(a -> a -> Bool) -> f a -> [NonEmpty a]
NEList.groupBy (\(ExtIdent
_, InfernoType
ty1) (ExtIdent
_, InfernoType
ty2) -> InfernoType
ty1 forall a. Eq a => a -> a -> Bool
== InfernoType
ty2) forall a b. (a -> b) -> a -> b
$ forall k a. Map k a -> [(k, a)]
Map.toList Map ExtIdent InfernoType
withTypeHole
              -- each [(var$i_1, _),...,(var$i_n, _)] gets turned into the map {i_1 -> Left i_1, ... i_n -> Left i_1}
              substMap :: Map Int (Either Int InfernoType)
substMap =
                forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr
                  ( \NonEmpty (ExtIdent, InfernoType)
vs Map Int (Either Int InfernoType)
m -> case forall a. NonEmpty a -> a
NEList.head NonEmpty (ExtIdent, InfernoType)
vs of
                      (ExtIdent (Left Int
i), InfernoType
_) ->
                        forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr
                          ( \(ExtIdent
v, InfernoType
_) Map Int (Either Int InfernoType)
m' -> case ExtIdent
v of
                              ExtIdent (Left Int
j) -> forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert Int
j (forall a b. a -> Either a b
Left Int
i) Map Int (Either Int InfernoType)
m'
                              ExtIdent
_ -> Map Int (Either Int InfernoType)
m'
                          )
                          Map Int (Either Int InfernoType)
m
                          NonEmpty (ExtIdent, InfernoType)
vs
                      (ExtIdent, InfernoType)
_ -> Map Int (Either Int InfernoType)
m
                  )
                  forall {a}. Map Int (Either a InfernoType)
fullyInstantiatedMap
                  [NonEmpty (ExtIdent, InfernoType)]
withTypeHoleGrouped

              (SourcePos
pos, SourcePos
_) = forall (f :: * -> *).
BlockUtils f =>
f SourcePos -> Location SourcePos
blockPosition Expr (Pinned VCObjectHash) SourcePos
expr
              expr' :: Expr (Pinned VCObjectHash) SourcePos
expr' = forall hash pos.
Map Int (Either Int InfernoType) -> Expr hash pos -> Expr hash pos
substInternalIdents Map Int (Either Int InfernoType)
substMap Expr (Pinned VCObjectHash) SourcePos
expr
           in case forall k a. Map k a -> [(k, a)]
Map.toList Map ExtIdent InfernoType
withTypeHole of
                [] -> (forall a. Maybe a
Nothing, Map ExtIdent InfernoType
rest, Expr (Pinned VCObjectHash) SourcePos
expr')
                -- if we have any type holes, we need to wrap the expression in a lambda and add a `requires rep on ...` typeclass
                -- capturing all the runtime reps that the expression needs
                (ExtIdent, InfernoType)
_ : [(ExtIdent, InfernoType)]
_ ->
                  let lamList :: NonEmpty (SourcePos, Maybe ExtIdent)
lamList = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\NonEmpty (ExtIdent, InfernoType)
merged -> let (ExtIdent
v, InfernoType
_) = forall a. NonEmpty a -> a
NEList.head NonEmpty (ExtIdent, InfernoType)
merged in (SourcePos
pos, forall a. a -> Maybe a
Just ExtIdent
v)) forall a b. (a -> b) -> a -> b
$ forall a. [a] -> NonEmpty a
NEList.fromList forall a b. (a -> b) -> a -> b
$ [NonEmpty (ExtIdent, InfernoType)]
withTypeHoleGrouped
                   in ( forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$
                          Text -> [InfernoType] -> TypeClass
TypeClass Text
"rep" forall a b. (a -> b) -> a -> b
$
                            forall a b. (a -> b) -> [a] -> [b]
map
                              ( \((ExtIdent
_, InfernoType
ty) NEList.:| [(ExtIdent, InfernoType)]
_) -> case InfernoType
ty of
                                  TRep InfernoType
ty' -> InfernoType
ty'
                                  InfernoType
_ -> InfernoType
ty
                              )
                              [NonEmpty (ExtIdent, InfernoType)]
withTypeHoleGrouped,
                        Map ExtIdent InfernoType
rest,
                        forall hash pos.
pos
-> NonEmpty (pos, Maybe ExtIdent)
-> pos
-> Expr hash pos
-> Expr hash pos
Lam SourcePos
pos NonEmpty (SourcePos, Maybe ExtIdent)
lamList SourcePos
pos Expr (Pinned VCObjectHash) SourcePos
expr'
                      )

-- | Solve for the top level type of an expression in a given environment
inferExpr ::
  Map.Map ModuleName (PinnedModule m) ->
  Expr (Pinned VCObjectHash) SourcePos ->
  Either
    [TypeError SourcePos]
    ( Expr (Pinned VCObjectHash) SourcePos,
      TCScheme,
      Map.Map (Location SourcePos) (TypeMetadata TCScheme)
    )
inferExpr :: forall m.
Map ModuleName (PinnedModule m)
-> Expr (Pinned VCObjectHash) SourcePos
-> Either
     [TypeError SourcePos]
     (Expr (Pinned VCObjectHash) SourcePos, TCScheme,
      Map (Location SourcePos) (TypeMetadata TCScheme))
inferExpr Map ModuleName (PinnedModule m)
allModules Expr (Pinned VCObjectHash) SourcePos
expr =
  let (Env
env, Set TypeClass
inScopeClasses) = forall m. Map ModuleName (PinnedModule m) -> (Env, Set TypeClass)
openBuiltinModuleAndAddPinnedTypes Map ModuleName (PinnedModule m)
allModules
   in case forall m r.
Env
-> Set TypeClass
-> Map ModuleName (Module m)
-> Infer r
-> Either [TypeError SourcePos] (r, InferState)
runInfer Env
env Set TypeClass
inScopeClasses Map ModuleName (PinnedModule m)
allModules (Expr (Pinned VCObjectHash) SourcePos
-> Infer
     (Expr (Pinned VCObjectHash) SourcePos, ImplType, Set Constraint)
infer Expr (Pinned VCObjectHash) SourcePos
expr) of
        -- if we threw errors whilst inferring, rethrow
        Left [TypeError SourcePos]
err -> forall a b. a -> Either a b
Left [TypeError SourcePos]
err
        Right ((Expr (Pinned VCObjectHash) SourcePos
expr', ImplType
ty, Set Constraint
cs), InferState {Int
[(Location SourcePos, [Pat (Pinned VCObjectHash) SourcePos])]
Map (Location SourcePos) (TypeMetadata (Set TypeClass, ImplType))
Map ModuleName (Module ())
Set TypeClass
patternsToCheck :: [(Location SourcePos, [Pat (Pinned VCObjectHash) SourcePos])]
typeClasses :: Set TypeClass
modules :: Map ModuleName (Module ())
typeMap :: Map (Location SourcePos) (TypeMetadata (Set TypeClass, ImplType))
count :: Int
patternsToCheck :: InferState
-> [(Location SourcePos, [Pat (Pinned VCObjectHash) SourcePos])]
typeClasses :: InferState -> Set TypeClass
modules :: InferState -> Map ModuleName (Module ())
typeMap :: InferState
-> Map
     (Location SourcePos) (TypeMetadata (Set TypeClass, ImplType))
count :: InferState -> Int
..}) ->
          -- trace ("new expr: " <> (Text.unpack . renderPretty) expr') $
          --   trace
          --     ( "ty: " <> (Text.unpack . renderPretty) ty
          --         <> "\ncs: "
          --         <> (intercalate "\n" $ map show $ Set.toList cs)
          --     )
          --     $
          -- case runSolve typeClasses $ filter (\case { Right (_, TypeClass "rep" _) -> False; _ -> True }) $ Set.toList cs of
          case Set TypeClass -> [Constraint] -> Either [TypeError SourcePos] Subst
runSolve Set TypeClass
typeClasses forall a b. (a -> b) -> a -> b
$ forall a. Set a -> [a]
Set.toList Set Constraint
cs of
            Left [TypeError SourcePos]
errs -> forall a b. a -> Either a b
Left [TypeError SourcePos]
errs
            Right Subst
subst ->
              -- trace ("substs: " <> show subst) $
              -- trace ("patternsToCheck: " <> show patternsToCheck) $
              case forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry forall a b. (a -> b) -> a -> b
$ Map VCObjectHash (Set (VCObjectHash, Text))
-> Location SourcePos
-> [Pat (Pinned VCObjectHash) SourcePos]
-> [TypeError SourcePos]
checkExhaustivenessAndUsefullness Map VCObjectHash (Set (VCObjectHash, Text))
enumSigs) [(Location SourcePos, [Pat (Pinned VCObjectHash) SourcePos])]
patternsToCheck of
                errs :: [TypeError SourcePos]
errs@(TypeError SourcePos
_ : [TypeError SourcePos]
_) -> forall a b. a -> Either a b
Left [TypeError SourcePos]
errs
                [TypeError SourcePos]
_ -> do
                  -- get type classes and type from solved constraints
                  let cls :: Set TypeClass
cls = Set TypeClass -> Set TypeClass
filterInstantiatedTypeClasses forall a b. (a -> b) -> a -> b
$ forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map (forall a. Substitutable a => Subst -> a -> a
apply Subst
subst forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> b
snd) forall a b. (a -> b) -> a -> b
$ forall a. Ord a => [a] -> Set a
Set.fromList forall a b. (a -> b) -> a -> b
$ forall a b. [Either a b] -> [b]
rights forall a b. (a -> b) -> a -> b
$ forall a. Set a -> [a]
Set.toList Set Constraint
cs
                  let substitutedTy :: ImplType
substitutedTy@(ImplType Map ExtIdent InfernoType
implTys InfernoType
tyBody) = forall a. Substitutable a => Subst -> a -> a
apply Subst
subst ImplType
ty
                  -- get current type variables
                  let tvs :: Set TV
tvs = forall a. Substitutable a => a -> Set TV
ftv ImplType
substitutedTy forall a. Ord a => Set a -> Set a -> Set a
`Set.union` (forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
Set.unions forall a b. (a -> b) -> a -> b
$ forall a. Set a -> [a]
Set.elems forall a b. (a -> b) -> a -> b
$ forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map forall a. Substitutable a => a -> Set TV
ftv Set TypeClass
cls)
                  let res :: Subst
-> (Maybe TypeClass, Map ExtIdent InfernoType, a)
-> Either
     a (a, TCScheme, Map (Location SourcePos) (TypeMetadata TCScheme))
res Subst
substNew (Maybe TypeClass
mRepTyCls, Map ExtIdent InfernoType
implTys', a
expr'') =
                        let finalTy :: TCScheme
finalTy =
                              Set TypeClass -> ImplType -> TCScheme
closeOver
                                ((Set TypeClass -> Set TypeClass
filterInstantiatedTypeClasses forall a b. (a -> b) -> a -> b
$ forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map (forall a. Substitutable a => Subst -> a -> a
apply Subst
substNew) Set TypeClass
cls) forall a. Ord a => Set a -> Set a -> Set a
`Set.union` (forall b a. b -> (a -> b) -> Maybe a -> b
maybe forall a. Monoid a => a
mempty forall a. a -> Set a
Set.singleton Maybe TypeClass
mRepTyCls))
                                forall a b. (a -> b) -> a -> b
$ forall a. Substitutable a => Subst -> a -> a
apply Subst
substNew
                                forall a b. (a -> b) -> a -> b
$ Map ExtIdent InfernoType -> InfernoType -> ImplType
ImplType Map ExtIdent InfernoType
implTys' InfernoType
tyBody
                         in forall a b. b -> Either a b
Right forall a b. (a -> b) -> a -> b
$
                              ( a
expr'',
                                TCScheme
finalTy,
                                forall a b k. (a -> b) -> Map k a -> Map k b
Map.map
                                  (\meta :: TypeMetadata (Set TypeClass, ImplType)
meta@TypeMetadata {ty :: forall ty. TypeMetadata ty -> ty
ty = (Set TypeClass
tcs, ImplType
t)} -> TypeMetadata (Set TypeClass, ImplType)
meta {ty :: TCScheme
ty = Set TypeClass -> ImplType -> TCScheme
closeOver (Set TypeClass -> Set TypeClass
filterInstantiatedTypeClasses forall a b. (a -> b) -> a -> b
$ forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map (forall a. Substitutable a => Subst -> a -> a
apply forall a b. (a -> b) -> a -> b
$ Subst
substNew forall a. Semigroup a => a -> a -> a
<> Subst
subst) Set TypeClass
tcs) forall a b. (a -> b) -> a -> b
$ forall a. Substitutable a => Subst -> a -> a
apply (Subst
substNew forall a. Semigroup a => a -> a -> a
<> Subst
subst) ImplType
t})
                                  Map (Location SourcePos) (TypeMetadata (Set TypeClass, ImplType))
typeMap
                              )

                  if -- trace ("type classes: " <> show cls) $
                  forall a. Set a -> Bool
Set.null Set TypeClass
cls
                    then forall {a} {a}.
Subst
-> (Maybe TypeClass, Map ExtIdent InfernoType, a)
-> Either
     a (a, TCScheme, Map (Location SourcePos) (TypeMetadata TCScheme))
res forall a. Monoid a => a
mempty forall a b. (a -> b) -> a -> b
$ Map ExtIdent InfernoType
-> Expr (Pinned VCObjectHash) SourcePos
-> (Maybe TypeClass, Map ExtIdent InfernoType,
    Expr (Pinned VCObjectHash) SourcePos)
closeOverTypeReps Map ExtIdent InfernoType
implTys Expr (Pinned VCObjectHash) SourcePos
expr'
                    else case Set TypeClass -> Maybe Int -> Set TypeClass -> Set TV -> [Subst]
findTypeClassWitnesses Set TypeClass
typeClasses (forall a. a -> Maybe a
Just Int
2) Set TypeClass
cls Set TV
tvs of
                      [] -> forall a b. a -> Either a b
Left [forall a. Set TypeClass -> Location a -> TypeError a
CouldNotFindTypeclassWitness Set TypeClass
cls forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *).
BlockUtils f =>
f SourcePos -> Location SourcePos
blockPosition Expr (Pinned VCObjectHash) SourcePos
expr]
                      -- we attempt to find two type assignments. If there is only one satisfying assignment for all the type-classes, we automatically substitute the instantiations
                      [Subst
subst'] -> forall {a} {a}.
Subst
-> (Maybe TypeClass, Map ExtIdent InfernoType, a)
-> Either
     a (a, TCScheme, Map (Location SourcePos) (TypeMetadata TCScheme))
res Subst
subst' forall a b. (a -> b) -> a -> b
$ Map ExtIdent InfernoType
-> Expr (Pinned VCObjectHash) SourcePos
-> (Maybe TypeClass, Map ExtIdent InfernoType,
    Expr (Pinned VCObjectHash) SourcePos)
closeOverTypeReps (forall a b k. (a -> b) -> Map k a -> Map k b
Map.map (forall a. Substitutable a => Subst -> a -> a
apply Subst
subst') Map ExtIdent InfernoType
implTys) Expr (Pinned VCObjectHash) SourcePos
expr'
                      -- even if there isn't a unique solution, we can still safely apply the substitutions to any types which do not transitively depend on the input or output type variables
                      -- e.g. for `let x = 3.2 in x + 2` it does not matter whether the type of `2` is an int or a double, because the final type of the whole expression won't change
                      (Subst Map TV InfernoType
s) : [Subst]
_ ->
                        let ftvsDependentOnOuterType :: Set TV
ftvsDependentOnOuterType =
                              forall a b. (a -> b -> a) -> a -> Set b -> a
Set.foldl
                                ( \Set TV
ftvsTransClosure TypeClass
c ->
                                    let ftvCls :: Set TV
ftvCls = forall a. Substitutable a => a -> Set TV
ftv TypeClass
c
                                     in if forall a. Set a -> Bool
Set.null forall a b. (a -> b) -> a -> b
$ Set TV
ftvCls forall a. Ord a => Set a -> Set a -> Set a
`Set.intersection` Set TV
ftvsTransClosure
                                          then Set TV
ftvsTransClosure
                                          else Set TV
ftvCls forall a. Ord a => Set a -> Set a -> Set a
`Set.union` Set TV
ftvsTransClosure
                                )
                                -- start with the body of the type, i.e. in `forall a_1 ... a_n {requires ..., implicit ...} => t` get the type variables in `t`
                                -- as well as any implicit arguments which aren't internal, since those are used for tracking type-reps
                                (forall a. Substitutable a => a -> Set TV
ftv InfernoType
tyBody forall a. Ord a => Set a -> Set a -> Set a
`Set.union` (forall k a b. (k -> a -> b -> b) -> b -> Map k a -> b
Map.foldrWithKey (\(ExtIdent Either Int Text
ident) InfernoType
t Set TV
ftvs -> case Either Int Text
ident of Left Int
_ -> Set TV
ftvs; Right Text
_ -> forall a. Substitutable a => a -> Set TV
ftv InfernoType
t forall a. Ord a => Set a -> Set a -> Set a
`Set.union` Set TV
ftvs) forall a. Monoid a => a
mempty Map ExtIdent InfernoType
implTys))
                                Set TypeClass
cls
                            subst' :: Subst
subst' = Map TV InfernoType -> Subst
Subst forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b -> b) -> b -> Set a -> b
Set.foldr forall k a. Ord k => k -> Map k a -> Map k a
Map.delete Map TV InfernoType
s Set TV
ftvsDependentOnOuterType
                         in -- trace ("type ftvsDependentOnOuterType: " <> show ftvsDependentOnOuterType) $
                            forall {a} {a}.
Subst
-> (Maybe TypeClass, Map ExtIdent InfernoType, a)
-> Either
     a (a, TCScheme, Map (Location SourcePos) (TypeMetadata TCScheme))
res Subst
subst' forall a b. (a -> b) -> a -> b
$ Map ExtIdent InfernoType
-> Expr (Pinned VCObjectHash) SourcePos
-> (Maybe TypeClass, Map ExtIdent InfernoType,
    Expr (Pinned VCObjectHash) SourcePos)
closeOverTypeReps (forall a b k. (a -> b) -> Map k a -> Map k b
Map.map (forall a. Substitutable a => Subst -> a -> a
apply Subst
subst') Map ExtIdent InfernoType
implTys) Expr (Pinned VCObjectHash) SourcePos
expr'
  where
    enumSigs :: Map.Map VCObjectHash (Set.Set (VCObjectHash, Text.Text))
    enumSigs :: Map VCObjectHash (Set (VCObjectHash, Text))
enumSigs =
      forall k a b. (k -> a -> b -> b) -> b -> Map k a -> b
Map.foldrWithKey
        ( \VCObjectHash
h (ForallTC [TV]
_ Set TypeClass
_ (ImplType Map ExtIdent InfernoType
_ InfernoType
ty)) Map VCObjectHash (Set (VCObjectHash, Text))
m -> case InfernoType
ty of
            TBase (TEnum Text
_n Set Ident
cs) ->
              let allConstrHashes :: Set (VCObjectHash, Text)
allConstrHashes = forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map (\c :: Ident
c@(Ident Text
i) -> (forall obj. VCHashUpdate obj => obj -> VCObjectHash
vcHash (Ident
c, VCObjectHash
h), Text
i)) Set Ident
cs
               in forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList [(VCObjectHash
cH, Set (VCObjectHash, Text)
allConstrHashes) | (VCObjectHash
cH, Text
_) <- forall a. Set a -> [a]
Set.toList Set (VCObjectHash, Text)
allConstrHashes] forall k a. Ord k => Map k a -> Map k a -> Map k a
`Map.union` Map VCObjectHash (Set (VCObjectHash, Text))
m
            InfernoType
_ -> Map VCObjectHash (Set (VCObjectHash, Text))
m
        )
        forall a. Monoid a => a
mempty
        forall a b. (a -> b) -> a -> b
$ forall a b k. (a -> b) -> Map k a -> Map k b
Map.map forall ty. TypeMetadata ty -> ty
ty
        forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) k a.
(Foldable f, Ord k) =>
f (Map k a) -> Map k a
Map.unions
        forall a b. (a -> b) -> a -> b
$ forall m.
PinnedModule m -> Map VCObjectHash (TypeMetadata TCScheme)
pinnedModuleHashToTy PinnedModule ()
builtinModule forall a. a -> [a] -> [a]
: (forall a b. (a -> b) -> [a] -> [b]
map forall m.
PinnedModule m -> Map VCObjectHash (TypeMetadata TCScheme)
pinnedModuleHashToTy forall a b. (a -> b) -> a -> b
$ forall k a. Map k a -> [a]
Map.elems Map ModuleName (PinnedModule m)
allModules)
    openBuiltinModuleAndAddPinnedTypes :: Map.Map ModuleName (PinnedModule m) -> (Env, Set.Set TypeClass)
    openBuiltinModuleAndAddPinnedTypes :: forall m. Map ModuleName (PinnedModule m) -> (Env, Set TypeClass)
openBuiltinModuleAndAddPinnedTypes Map ModuleName (PinnedModule m)
modules =
      let Module {moduleTypeClasses :: forall objs. Module objs -> Set TypeClass
moduleTypeClasses = Set TypeClass
tyCls, moduleObjects :: forall objs. Module objs -> objs
moduleObjects = (Map Namespace VCObjectHash
_, Map VCObjectHash (TypeMetadata TCScheme)
tys, ()
_)} = PinnedModule ()
builtinModule
       in ( Env
Env.empty
              { pinnedTypes :: Map VCObjectHash (TypeMetadata TCScheme)
Env.pinnedTypes = forall (f :: * -> *) k a.
(Foldable f, Ord k) =>
f (Map k a) -> Map k a
Map.unions forall a b. (a -> b) -> a -> b
$ Map VCObjectHash (TypeMetadata TCScheme)
tys forall a. a -> [a] -> [a]
: [forall m.
PinnedModule m -> Map VCObjectHash (TypeMetadata TCScheme)
pinnedModuleHashToTy PinnedModule m
m | PinnedModule m
m <- forall k a. Map k a -> [a]
Map.elems Map ModuleName (PinnedModule m)
modules]
              },
            Set TypeClass
tyCls forall a. Ord a => Set a -> Set a -> Set a
`Set.union` forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
Set.unions [Set TypeClass
tc | Module {moduleTypeClasses :: forall objs. Module objs -> Set TypeClass
moduleTypeClasses = Set TypeClass
tc} <- forall k a. Map k a -> [a]
Map.elems Map ModuleName (PinnedModule m)
modules]
          )

-- | Given a type signature and some concrete assignment of types (assumes inputTys and outputTy have no free variables)
-- | this function computes the runtime reps
inferTypeReps :: Set.Set TypeClass -> TCScheme -> [InfernoType] -> InfernoType -> Either [TypeError SourcePos] [InfernoType]
inferTypeReps :: Set TypeClass
-> TCScheme
-> [InfernoType]
-> InfernoType
-> Either [TypeError SourcePos] [InfernoType]
inferTypeReps Set TypeClass
allTypeClasses (ForallTC [TV]
tvs Set TypeClass
tyCls (ImplType Map ExtIdent InfernoType
_impl InfernoType
ty)) [InfernoType]
inputTys InfernoType
outputTy =
  let cs :: [Either
   (InfernoType, InfernoType, [a]) (Location SourcePos, TypeClass)]
cs =
        [forall a b. b -> Either a b
Right (Location SourcePos
dummyPos, TypeClass
c) | c :: TypeClass
c@(TypeClass Text
nm [InfernoType]
_) <- forall a. Set a -> [a]
Set.toList Set TypeClass
tyCls, Text
nm forall a. Eq a => a -> a -> Bool
/= Text
"rep"]
          forall a. [a] -> [a] -> [a]
++ forall {a} {b}.
InfernoType
-> [InfernoType] -> [Either (InfernoType, InfernoType, [a]) b]
mkConstraints InfernoType
ty [InfernoType]
inputTys
   in case Set TypeClass -> [Constraint] -> Either [TypeError SourcePos] Subst
runSolve Set TypeClass
allTypeClasses forall {a}.
[Either
   (InfernoType, InfernoType, [a]) (Location SourcePos, TypeClass)]
cs of
        Left [TypeError SourcePos]
errs -> forall a b. a -> Either a b
Left [TypeError SourcePos]
errs
        Right Subst
subst ->
          let tyClsSubst :: Set TypeClass
tyClsSubst = forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map (forall a. Substitutable a => Subst -> a -> a
apply Subst
subst) Set TypeClass
tyCls
           in case forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Maybe a
find (\(TypeClass Text
nm [InfernoType]
_) -> Text
nm forall a. Eq a => a -> a -> Bool
== Text
"rep") forall a b. (a -> b) -> a -> b
$ forall a. Set a -> [a]
Set.toList Set TypeClass
tyClsSubst of
                Maybe TypeClass
Nothing -> forall (f :: * -> *) a. Applicative f => a -> f a
pure []
                Just rep :: TypeClass
rep@(TypeClass Text
_ [InfernoType]
runtimeRepTys) ->
                  if forall a. Set a -> Bool
Set.null forall a b. (a -> b) -> a -> b
$ forall a. Substitutable a => a -> Set TV
ftv TypeClass
rep
                    then forall (f :: * -> *) a. Applicative f => a -> f a
pure [InfernoType]
runtimeRepTys
                    else case Set TypeClass -> Maybe Int -> Set TypeClass -> Set TV -> [Subst]
findTypeClassWitnesses
                      Set TypeClass
allTypeClasses
                      (forall a. a -> Maybe a
Just Int
1)
                      (forall a. (a -> Bool) -> Set a -> Set a
Set.filter (\case TypeClass Text
"rep" [InfernoType]
_ -> Bool
False; TypeClass
_ -> Bool
True) Set TypeClass
tyClsSubst)
                      (forall a. Ord a => [a] -> Set a
Set.fromList [TV]
tvs) of
                      [] -> forall a b. a -> Either a b
Left [forall a. Set TypeClass -> Location a -> TypeError a
CouldNotFindTypeclassWitness Set TypeClass
tyClsSubst Location SourcePos
dummyPos]
                      Subst
subst' : [Subst]
_ -> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall a. Substitutable a => Subst -> a -> a
apply Subst
subst' [InfernoType]
runtimeRepTys
  where
    mkConstraints :: InfernoType
-> [InfernoType] -> [Either (InfernoType, InfernoType, [a]) b]
mkConstraints (TArr InfernoType
t1 InfernoType
t2) (InfernoType
x : [InfernoType]
xs) = forall a b. a -> Either a b
Left (InfernoType
t1, InfernoType
x, []) forall a. a -> [a] -> [a]
: InfernoType
-> [InfernoType] -> [Either (InfernoType, InfernoType, [a]) b]
mkConstraints InfernoType
t2 [InfernoType]
xs
    mkConstraints InfernoType
t [] = [forall a b. a -> Either a b
Left (InfernoType
t, InfernoType
outputTy, [])]
    mkConstraints InfernoType
_ [InfernoType]
_ = forall a. HasCallStack => [Char] -> a
error [Char]
"mkConstraints: invalid input params length"

    dummyPos :: Location SourcePos
dummyPos = let pos :: SourcePos
pos = [Char] -> SourcePos
initialPos [Char]
"" in (SourcePos
pos, SourcePos
pos)

inferPossibleTypes :: Set.Set TypeClass -> TCScheme -> [Maybe InfernoType] -> Maybe InfernoType -> Either [TypeError SourcePos] ([[InfernoType]], [InfernoType])
inferPossibleTypes :: Set TypeClass
-> TCScheme
-> [Maybe InfernoType]
-> Maybe InfernoType
-> Either [TypeError SourcePos] ([[InfernoType]], [InfernoType])
inferPossibleTypes Set TypeClass
allTypeClasses (ForallTC [TV]
_ Set TypeClass
tyCls (ImplType Map ExtIdent InfernoType
_impl InfernoType
ty)) [Maybe InfernoType]
inputTys Maybe InfernoType
outputTy =
  let cs :: [Either
   (InfernoType, InfernoType, [a]) (Location SourcePos, TypeClass)]
cs =
        [forall a b. b -> Either a b
Right (Location SourcePos
dummyPos, TypeClass
c) | c :: TypeClass
c@(TypeClass Text
nm [InfernoType]
_) <- forall a. Set a -> [a]
Set.toList Set TypeClass
tyCls, Text
nm forall a. Eq a => a -> a -> Bool
/= Text
"rep"]
          forall a. [a] -> [a] -> [a]
++ forall {a} {b}.
InfernoType
-> [Maybe InfernoType]
-> [Either (InfernoType, InfernoType, [a]) b]
mkMaybeConstraints InfernoType
ty [Maybe InfernoType]
inputTys
   in case Set TypeClass -> [Constraint] -> Either [TypeError SourcePos] Subst
runSolve Set TypeClass
allTypeClasses forall {a}.
[Either
   (InfernoType, InfernoType, [a]) (Location SourcePos, TypeClass)]
cs of
        Left [TypeError SourcePos]
errs -> forall a b. a -> Either a b
Left [TypeError SourcePos]
errs
        Right Subst
subst -> do
          let tyClsSubst :: Set TypeClass
tyClsSubst = forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map (forall a. Substitutable a => Subst -> a -> a
apply Subst
subst) forall a b. (a -> b) -> a -> b
$ forall a. (a -> Bool) -> Set a -> Set a
Set.filter (\case TypeClass Text
"rep" [InfernoType]
_ -> Bool
False; TypeClass
_ -> Bool
True) Set TypeClass
tyCls
          let ([InfernoType]
inTysFromSig, InfernoType
outTyFromSig) = InfernoType -> ([InfernoType], InfernoType)
gatherArgs forall a b. (a -> b) -> a -> b
$ forall a. Substitutable a => Subst -> a -> a
apply Subst
subst InfernoType
ty
          let findAllPossibleTypes :: (Maybe a, a) -> Either [TypeError SourcePos] [a]
findAllPossibleTypes (Maybe a
supplied, a
t) = case Maybe a
supplied of
                Just a
t' -> forall (f :: * -> *) a. Applicative f => a -> f a
pure [a
t']
                Maybe a
Nothing ->
                  let tvs :: Set TV
tvs = forall a. Substitutable a => a -> Set TV
ftv a
t
                   in if forall a. Set a -> Bool
Set.null Set TV
tvs
                        then forall (f :: * -> *) a. Applicative f => a -> f a
pure [a
t]
                        else case Set TypeClass -> Maybe Int -> Set TypeClass -> Set TV -> [Subst]
findTypeClassWitnesses Set TypeClass
allTypeClasses (forall a. a -> Maybe a
Just Int
100) Set TypeClass
tyClsSubst Set TV
tvs of
                          [] -> forall a b. a -> Either a b
Left [forall a. Set TypeClass -> Location a -> TypeError a
CouldNotFindTypeclassWitness Set TypeClass
tyClsSubst Location SourcePos
dummyPos]
                          [Subst]
substs -> forall (f :: * -> *) a. Applicative f => a -> f a
pure [forall a. Substitutable a => Subst -> a -> a
apply Subst
sub a
t | Subst
sub <- [Subst]
substs]

          [[InfernoType]]
possibleInTysFromSig <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM (forall a b. [a] -> [b] -> [(a, b)]
zip [Maybe InfernoType]
inputTys [InfernoType]
inTysFromSig) forall {a}.
Substitutable a =>
(Maybe a, a) -> Either [TypeError SourcePos] [a]
findAllPossibleTypes
          ([[InfernoType]]
possibleInTysFromSig,) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall {a}.
Substitutable a =>
(Maybe a, a) -> Either [TypeError SourcePos] [a]
findAllPossibleTypes (Maybe InfernoType
outputTy, InfernoType
outTyFromSig)
  where
    gatherArgs :: InfernoType -> ([InfernoType], InfernoType)
gatherArgs (TArr InfernoType
t1 InfernoType
t2) = forall (p :: * -> * -> *) a b c d.
Bifunctor p =>
(a -> b) -> (c -> d) -> p a c -> p b d
bimap (InfernoType
t1 forall a. a -> [a] -> [a]
:) forall a. a -> a
id forall a b. (a -> b) -> a -> b
$ InfernoType -> ([InfernoType], InfernoType)
gatherArgs InfernoType
t2
    gatherArgs InfernoType
x = ([], InfernoType
x)
    mkMaybeConstraints :: InfernoType
-> [Maybe InfernoType]
-> [Either (InfernoType, InfernoType, [a]) b]
mkMaybeConstraints (TArr InfernoType
t1 InfernoType
t2) (Just InfernoType
x : [Maybe InfernoType]
xs) = forall a b. a -> Either a b
Left (InfernoType
t1, InfernoType
x, []) forall a. a -> [a] -> [a]
: InfernoType
-> [Maybe InfernoType]
-> [Either (InfernoType, InfernoType, [a]) b]
mkMaybeConstraints InfernoType
t2 [Maybe InfernoType]
xs
    mkMaybeConstraints (TArr InfernoType
_ InfernoType
t2) (Maybe InfernoType
Nothing : [Maybe InfernoType]
xs) = InfernoType
-> [Maybe InfernoType]
-> [Either (InfernoType, InfernoType, [a]) b]
mkMaybeConstraints InfernoType
t2 [Maybe InfernoType]
xs
    mkMaybeConstraints InfernoType
t [] = case Maybe InfernoType
outputTy of
      Just InfernoType
t' -> [forall a b. a -> Either a b
Left (InfernoType
t, InfernoType
t', [])]
      Maybe InfernoType
Nothing -> []
    mkMaybeConstraints InfernoType
_ [Maybe InfernoType]
_ = forall a. HasCallStack => [Char] -> a
error [Char]
"mkConstraints: invalid input params length"

    dummyPos :: Location SourcePos
dummyPos = let pos :: SourcePos
pos = [Char] -> SourcePos
initialPos [Char]
"" in (SourcePos
pos, SourcePos
pos)

-- | Extend type environment
inEnv :: (ExtIdent, TypeMetadata TCScheme) -> Infer a -> Infer a
inEnv :: forall a. (ExtIdent, TypeMetadata TCScheme) -> Infer a -> Infer a
inEnv (ExtIdent
x, TypeMetadata TCScheme
meta) Infer a
m = do
  let scope :: Env -> Env
scope Env
e = (Env -> ExtIdent -> Env
Env.remove Env
e ExtIdent
x) Env -> (ExtIdent, TypeMetadata TCScheme) -> Env
`Env.extend` (ExtIdent
x, TypeMetadata TCScheme
meta)
  forall r (m :: * -> *) a. MonadReader r m => (r -> r) -> m a -> m a
local Env -> Env
scope Infer a
m

-- | Lookup type in the environment
lookupEnv :: Location SourcePos -> Either VCObjectHash ExtIdent -> Infer (TypeMetadata (Set.Set TypeClass, ImplType))
lookupEnv :: Location SourcePos
-> Either VCObjectHash ExtIdent
-> Infer (TypeMetadata (Set TypeClass, ImplType))
lookupEnv Location SourcePos
loc Either VCObjectHash ExtIdent
x = do
  Env
env <- forall r (m :: * -> *). MonadReader r m => m r
ask
  case forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either (forall a b c. (a -> b -> c) -> b -> a -> c
flip VCObjectHash -> Env -> Maybe (TypeMetadata TCScheme)
Env.lookupPinned Env
env) (forall a b c. (a -> b -> c) -> b -> a -> c
flip ExtIdent -> Env -> Maybe (TypeMetadata TCScheme)
Env.lookup Env
env) Either VCObjectHash ExtIdent
x of
    Maybe (TypeMetadata TCScheme)
Nothing ->
      forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError
        [ forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either
            (\VCObjectHash
hsh -> forall a.
Scoped ModuleName
-> Either VCObjectHash Namespace -> Location a -> TypeError a
UnboundNameInNamespace forall a. Scoped a
LocalScope (forall a b. a -> Either a b
Left VCObjectHash
hsh) Location SourcePos
loc)
            (\ExtIdent
i -> forall a.
Scoped ModuleName -> ExtIdent -> Location a -> TypeError a
UnboundExtIdent forall a. Scoped a
LocalScope ExtIdent
i Location SourcePos
loc)
            Either VCObjectHash ExtIdent
x
        ]
    Just TypeMetadata TCScheme
meta -> do
      (Set TypeClass, ImplType)
iTy <- TCScheme -> Infer (Set TypeClass, ImplType)
instantiate forall a b. (a -> b) -> a -> b
$ forall ty. TypeMetadata ty -> ty
ty TypeMetadata TCScheme
meta
      forall (m :: * -> *) a. Monad m => a -> m a
return TypeMetadata TCScheme
meta {ty :: (Set TypeClass, ImplType)
ty = (Set TypeClass, ImplType)
iTy}

mergeImplicitMaps :: Location SourcePos -> [Map.Map ExtIdent InfernoType] -> (Map.Map ExtIdent InfernoType, [Constraint])
mergeImplicitMaps :: Location SourcePos
-> [Map ExtIdent InfernoType]
-> (Map ExtIdent InfernoType, [Constraint])
mergeImplicitMaps Location SourcePos
loc =
  forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr
    ( \Map ExtIdent InfernoType
m (Map ExtIdent InfernoType
mAll, [Constraint]
cs) ->
        let cs' :: [Either (InfernoType, InfernoType, [TypeError SourcePos]) d]
cs' = forall k a. Map k a -> [a]
Map.elems forall a b. (a -> b) -> a -> b
$ forall k a b c.
Ord k =>
(k -> a -> b -> c) -> Map k a -> Map k b -> Map k c
Map.intersectionWithKey (\ExtIdent
ident InfernoType
t1 InfernoType
t2 -> forall a b c d. a -> b -> c -> Either (a, b, c) d
tyConstr InfernoType
t1 InfernoType
t2 [forall a.
Set TypeClass
-> ExtIdent
-> InfernoType
-> InfernoType
-> Location a
-> TypeError a
ImplicitVarTypeOverlap forall a. Monoid a => a
mempty ExtIdent
ident InfernoType
t1 InfernoType
t2 Location SourcePos
loc]) Map ExtIdent InfernoType
mAll Map ExtIdent InfernoType
m
         in (Map ExtIdent InfernoType
mAll forall k a. Ord k => Map k a -> Map k a -> Map k a
`Map.union` Map ExtIdent InfernoType
m, forall {d}.
[Either (InfernoType, InfernoType, [TypeError SourcePos]) d]
cs' forall a. [a] -> [a] -> [a]
++ [Constraint]
cs)
    )
    (forall k a. Map k a
Map.empty, [])

fresh :: Infer InfernoType
fresh :: Infer InfernoType
fresh = do
  s :: InferState
s@InferState {Int
[(Location SourcePos, [Pat (Pinned VCObjectHash) SourcePos])]
Map (Location SourcePos) (TypeMetadata (Set TypeClass, ImplType))
Map ModuleName (Module ())
Set TypeClass
patternsToCheck :: [(Location SourcePos, [Pat (Pinned VCObjectHash) SourcePos])]
typeClasses :: Set TypeClass
modules :: Map ModuleName (Module ())
typeMap :: Map (Location SourcePos) (TypeMetadata (Set TypeClass, ImplType))
count :: Int
patternsToCheck :: InferState
-> [(Location SourcePos, [Pat (Pinned VCObjectHash) SourcePos])]
typeClasses :: InferState -> Set TypeClass
modules :: InferState -> Map ModuleName (Module ())
typeMap :: InferState
-> Map
     (Location SourcePos) (TypeMetadata (Set TypeClass, ImplType))
count :: InferState -> Int
..} <- forall s (m :: * -> *). MonadState s m => m s
get
  forall s (m :: * -> *). MonadState s m => s -> m ()
put InferState
s {count :: Int
count = Int
count forall a. Num a => a -> a -> a
+ Int
1}
  forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Int -> InfernoType
var Int
count

freshRaw :: Infer Int
freshRaw :: Infer Int
freshRaw = do
  s :: InferState
s@InferState {Int
[(Location SourcePos, [Pat (Pinned VCObjectHash) SourcePos])]
Map (Location SourcePos) (TypeMetadata (Set TypeClass, ImplType))
Map ModuleName (Module ())
Set TypeClass
patternsToCheck :: [(Location SourcePos, [Pat (Pinned VCObjectHash) SourcePos])]
typeClasses :: Set TypeClass
modules :: Map ModuleName (Module ())
typeMap :: Map (Location SourcePos) (TypeMetadata (Set TypeClass, ImplType))
count :: Int
patternsToCheck :: InferState
-> [(Location SourcePos, [Pat (Pinned VCObjectHash) SourcePos])]
typeClasses :: InferState -> Set TypeClass
modules :: InferState -> Map ModuleName (Module ())
typeMap :: InferState
-> Map
     (Location SourcePos) (TypeMetadata (Set TypeClass, ImplType))
count :: InferState -> Int
..} <- forall s (m :: * -> *). MonadState s m => m s
get
  forall s (m :: * -> *). MonadState s m => s -> m ()
put InferState
s {count :: Int
count = Int
count forall a. Num a => a -> a -> a
+ Int
1}
  forall (m :: * -> *) a. Monad m => a -> m a
return Int
count

attachTypeToPosition :: Location SourcePos -> TypeMetadata (Set.Set TypeClass, ImplType) -> Infer ()
attachTypeToPosition :: Location SourcePos
-> TypeMetadata (Set TypeClass, ImplType) -> Infer ()
attachTypeToPosition Location SourcePos
k TypeMetadata (Set TypeClass, ImplType)
meta =
  forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify (\InferState
s -> InferState
s {typeMap :: Map (Location SourcePos) (TypeMetadata (Set TypeClass, ImplType))
typeMap = forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert Location SourcePos
k TypeMetadata (Set TypeClass, ImplType)
meta forall a b. (a -> b) -> a -> b
$ InferState
-> Map
     (Location SourcePos) (TypeMetadata (Set TypeClass, ImplType))
typeMap InferState
s})

addCasePatterns :: Location SourcePos -> [Pat (Pinned VCObjectHash) SourcePos] -> Infer ()
addCasePatterns :: Location SourcePos
-> [Pat (Pinned VCObjectHash) SourcePos] -> Infer ()
addCasePatterns Location SourcePos
k [Pat (Pinned VCObjectHash) SourcePos]
pttrns =
  forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify
    ( \InferState
s ->
        InferState
s
          { patternsToCheck :: [(Location SourcePos, [Pat (Pinned VCObjectHash) SourcePos])]
patternsToCheck = (Location SourcePos
k, [Pat (Pinned VCObjectHash) SourcePos]
pttrns) forall a. a -> [a] -> [a]
: InferState
-> [(Location SourcePos, [Pat (Pinned VCObjectHash) SourcePos])]
patternsToCheck InferState
s
          }
    )

instantiate :: TCScheme -> Infer (Set.Set TypeClass, ImplType)
instantiate :: TCScheme -> Infer (Set TypeClass, ImplType)
instantiate (ForallTC [TV]
as Set TypeClass
tcs ImplType
t) = do
  [InfernoType]
as' <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (forall a b. a -> b -> a
const Infer InfernoType
fresh) [TV]
as
  let s :: Subst
s = Map TV InfernoType -> Subst
Subst forall a b. (a -> b) -> a -> b
$ forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList forall a b. (a -> b) -> a -> b
$ forall a b. [a] -> [b] -> [(a, b)]
zip [TV]
as [InfernoType]
as'
  forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ (forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map (forall a. Substitutable a => Subst -> a -> a
apply Subst
s) Set TypeClass
tcs, forall a. Substitutable a => Subst -> a -> a
apply Subst
s ImplType
t)

opGetTyComponents :: ImplType -> (InfernoType, InfernoType, InfernoType)
opGetTyComponents :: ImplType -> (InfernoType, InfernoType, InfernoType)
opGetTyComponents (ImplType Map ExtIdent InfernoType
_ (InfernoType
t1 `TArr` (InfernoType
t2 `TArr` InfernoType
t3))) = (InfernoType
t1, InfernoType
t2, InfernoType
t3)
opGetTyComponents ImplType
_ = forall a. HasCallStack => [Char] -> a
error [Char]
"Invalid op type signature"

preOpGetTyComponents :: ImplType -> (InfernoType, InfernoType)
preOpGetTyComponents :: ImplType -> (InfernoType, InfernoType)
preOpGetTyComponents (ImplType Map ExtIdent InfernoType
_ (InfernoType
t1 `TArr` InfernoType
t2)) = (InfernoType
t1, InfernoType
t2)
preOpGetTyComponents ImplType
_ = forall a. HasCallStack => [Char] -> a
error [Char]
"Invalid pre-op type signature"

tyConstr :: a -> b -> c -> Either (a, b, c) d
tyConstr :: forall a b c d. a -> b -> c -> Either (a, b, c) d
tyConstr a
t1 b
t2 c
es = forall a b. a -> Either a b
Left (a
t1, b
t2, c
es)

inferLit :: Expr (Pinned VCObjectHash) SourcePos -> Location SourcePos -> Lit -> InfernoType -> Infer (Expr (Pinned VCObjectHash) SourcePos, ImplType, Set.Set Constraint)
inferLit :: Expr (Pinned VCObjectHash) SourcePos
-> Location SourcePos
-> Lit
-> InfernoType
-> Infer
     (Expr (Pinned VCObjectHash) SourcePos, ImplType, Set Constraint)
inferLit Expr (Pinned VCObjectHash) SourcePos
expr Location SourcePos
loc Lit
l InfernoType
t = do
  Location SourcePos
-> TypeMetadata (Set TypeClass, ImplType) -> Infer ()
attachTypeToPosition Location SourcePos
loc forall a b. (a -> b) -> a -> b
$
    TypeMetadata
      { identExpr :: Expr () ()
identExpr = forall hash pos. pos -> Lit -> Expr hash pos
Lit () Lit
l,
        ty :: (Set TypeClass, ImplType)
ty = (forall a. Set a
Set.empty, Map ExtIdent InfernoType -> InfernoType -> ImplType
ImplType forall k a. Map k a
Map.empty InfernoType
t),
        docs :: Maybe Text
docs = forall a. Maybe a
Nothing
      }
  forall (m :: * -> *) a. Monad m => a -> m a
return (Expr (Pinned VCObjectHash) SourcePos
expr, Map ExtIdent InfernoType -> InfernoType -> ImplType
ImplType forall k a. Map k a
Map.empty InfernoType
t, forall a. Set a
Set.empty)

infer :: Expr (Pinned VCObjectHash) SourcePos -> Infer (Expr (Pinned VCObjectHash) SourcePos, ImplType, Set.Set Constraint)
infer :: Expr (Pinned VCObjectHash) SourcePos
-> Infer
     (Expr (Pinned VCObjectHash) SourcePos, ImplType, Set Constraint)
infer Expr (Pinned VCObjectHash) SourcePos
expr =
  let exprLoc :: Location SourcePos
exprLoc = forall (f :: * -> *).
BlockUtils f =>
f SourcePos -> Location SourcePos
blockPosition Expr (Pinned VCObjectHash) SourcePos
expr
   in case Expr (Pinned VCObjectHash) SourcePos
expr of
        Lit SourcePos
pos l :: Lit
l@(LInt Int64
_) -> do
          InfernoType
tv <- Infer InfernoType
fresh
          let tyCls :: TypeClass
tyCls = Text -> [InfernoType] -> TypeClass
TypeClass Text
"numeric" [InfernoType
tv]
          Location SourcePos
-> TypeMetadata (Set TypeClass, ImplType) -> Infer ()
attachTypeToPosition Location SourcePos
exprLoc forall a b. (a -> b) -> a -> b
$
            TypeMetadata
              { identExpr :: Expr () ()
identExpr = forall hash pos. pos -> Lit -> Expr hash pos
Lit () Lit
l,
                ty :: (Set TypeClass, ImplType)
ty = (forall a. a -> Set a
Set.singleton TypeClass
tyCls, Map ExtIdent InfernoType -> InfernoType -> ImplType
ImplType forall k a. Map k a
Map.empty InfernoType
tv),
                docs :: Maybe Text
docs = forall a. Maybe a
Nothing
              }

          ExtIdent
i <- Either Int Text -> ExtIdent
ExtIdent forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. a -> Either a b
Left forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Infer Int
freshRaw
          forall (m :: * -> *) a. Monad m => a -> m a
return (forall hash pos. Expr hash pos -> Expr hash pos -> Expr hash pos
App Expr (Pinned VCObjectHash) SourcePos
expr (forall hash pos.
pos -> hash -> Scoped ModuleName -> ImplExpl -> Expr hash pos
Var SourcePos
pos forall a. Pinned a
Local forall a. Scoped a
LocalScope forall a b. (a -> b) -> a -> b
$ ExtIdent -> ImplExpl
Impl ExtIdent
i), Map ExtIdent InfernoType -> InfernoType -> ImplType
ImplType (forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList [(ExtIdent
i, InfernoType -> InfernoType
TRep InfernoType
tv)]) InfernoType
tv, forall a. a -> Set a
Set.singleton forall a b. (a -> b) -> a -> b
$ forall a b. b -> Either a b
Right (Location SourcePos
exprLoc, TypeClass
tyCls))
        Lit SourcePos
_ Lit
l ->
          Expr (Pinned VCObjectHash) SourcePos
-> Location SourcePos
-> Lit
-> InfernoType
-> Infer
     (Expr (Pinned VCObjectHash) SourcePos, ImplType, Set Constraint)
inferLit
            Expr (Pinned VCObjectHash) SourcePos
expr
            Location SourcePos
exprLoc
            Lit
l
            (Lit -> InfernoType
handleLit Lit
l)
          where
            handleLit :: Lit -> InfernoType
handleLit (LDouble Double
_) = InfernoType
typeDouble
            handleLit (LHex Word64
_) = InfernoType
typeWord64
            handleLit (LText Text
_) = InfernoType
typeText
            handleLit (LInt Int64
_) = forall a. HasCallStack => a
undefined
        Var SourcePos
pos Pinned VCObjectHash
mHash Scoped ModuleName
_modNm (Expl ExtIdent
x) -> do
          TypeMetadata (Set TypeClass, ImplType)
meta <- Location SourcePos
-> Either VCObjectHash ExtIdent
-> Infer (TypeMetadata (Set TypeClass, ImplType))
lookupEnv Location SourcePos
exprLoc (forall b a. b -> (a -> b) -> Maybe a -> b
maybe (forall a b. b -> Either a b
Right ExtIdent
x) forall a b. a -> Either a b
Left forall a b. (a -> b) -> a -> b
$ Pinned VCObjectHash -> Maybe VCObjectHash
pinnedToMaybe Pinned VCObjectHash
mHash)
          let (Set TypeClass
tcs, t :: ImplType
t@(ImplType Map ExtIdent InfernoType
impl InfernoType
t'')) = forall ty. TypeMetadata ty -> ty
ty TypeMetadata (Set TypeClass, ImplType)
meta
          Location SourcePos
-> TypeMetadata (Set TypeClass, ImplType) -> Infer ()
attachTypeToPosition Location SourcePos
exprLoc TypeMetadata (Set TypeClass, ImplType)
meta
          (Expr (Pinned VCObjectHash) SourcePos
expr', ImplType
t') <- case forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Maybe a
find (\(TypeClass Text
nm [InfernoType]
_) -> Text
nm forall a. Eq a => a -> a -> Bool
== Text
"rep") forall a b. (a -> b) -> a -> b
$ forall a. Set a -> [a]
Set.toList Set TypeClass
tcs of
            Just (TypeClass Text
_ [InfernoType]
runtimeRepTys) -> do
              [(ExtIdent, InfernoType)]
implRepTyps <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [InfernoType]
runtimeRepTys forall a b. (a -> b) -> a -> b
$ \InfernoType
repTy -> do
                Int
i <- Infer Int
freshRaw
                forall (f :: * -> *) a. Applicative f => a -> f a
pure (Either Int Text -> ExtIdent
ExtIdent forall a b. (a -> b) -> a -> b
$ forall a b. a -> Either a b
Left Int
i, InfernoType -> InfernoType
TRep InfernoType
repTy)
              let ([ExtIdent]
vars, [InfernoType]
_) = forall a b. [(a, b)] -> ([a], [b])
unzip [(ExtIdent, InfernoType)]
implRepTyps

              forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl forall hash pos. Expr hash pos -> Expr hash pos -> Expr hash pos
App Expr (Pinned VCObjectHash) SourcePos
expr forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map (forall hash pos.
pos -> hash -> Scoped ModuleName -> ImplExpl -> Expr hash pos
Var SourcePos
pos forall a. Pinned a
Local forall a. Scoped a
LocalScope forall b c a. (b -> c) -> (a -> b) -> a -> c
. ExtIdent -> ImplExpl
Impl) [ExtIdent]
vars, Map ExtIdent InfernoType -> InfernoType -> ImplType
ImplType (Map ExtIdent InfernoType
impl forall k a. Ord k => Map k a -> Map k a -> Map k a
`Map.union` forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList [(ExtIdent, InfernoType)]
implRepTyps) InfernoType
t'')
            Maybe TypeClass
Nothing -> forall (f :: * -> *) a. Applicative f => a -> f a
pure (Expr (Pinned VCObjectHash) SourcePos
expr, ImplType
t)
          forall (m :: * -> *) a. Monad m => a -> m a
return (Expr (Pinned VCObjectHash) SourcePos
expr', ImplType
t', forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map (forall a b. b -> Either a b
Right forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Location SourcePos
exprLoc,)) forall a b. (a -> b) -> a -> b
$ forall a. (a -> Bool) -> Set a -> Set a
Set.filter (\case TypeClass Text
"rep" [InfernoType]
_ -> Bool
False; TypeClass
_ -> Bool
True) Set TypeClass
tcs)
        Var SourcePos
_ Pinned VCObjectHash
_ Scoped ModuleName
_ (Impl ExtIdent
x) -> do
          InfernoType
tv <- Infer InfernoType
fresh
          Location SourcePos
-> TypeMetadata (Set TypeClass, ImplType) -> Infer ()
attachTypeToPosition
            Location SourcePos
exprLoc
            TypeMetadata
              { identExpr :: Expr () ()
identExpr = forall (p :: * -> * -> *) a b c d.
Bifunctor p =>
(a -> b) -> (c -> d) -> p a c -> p b d
bimap (forall a b. a -> b -> a
const ()) (forall a b. a -> b -> a
const ()) Expr (Pinned VCObjectHash) SourcePos
expr,
                ty :: (Set TypeClass, ImplType)
ty = (forall a. Set a
Set.empty, Map ExtIdent InfernoType -> InfernoType -> ImplType
ImplType (forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList [(ExtIdent
x, InfernoType
tv)]) InfernoType
tv),
                docs :: Maybe Text
docs = forall a. Maybe a
Nothing
              }
          forall (m :: * -> *) a. Monad m => a -> m a
return (Expr (Pinned VCObjectHash) SourcePos
expr, Map ExtIdent InfernoType -> InfernoType -> ImplType
ImplType (forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList [(ExtIdent
x, InfernoType
tv)]) InfernoType
tv, forall a. Set a
Set.empty)
        OpVar SourcePos
_ Pinned VCObjectHash
mHash Scoped ModuleName
_ Ident
_ -> do
          TypeMetadata (Set TypeClass, ImplType)
meta <- Location SourcePos
-> Either VCObjectHash ExtIdent
-> Infer (TypeMetadata (Set TypeClass, ImplType))
lookupEnv Location SourcePos
exprLoc (forall b a. b -> (a -> b) -> Maybe a -> b
maybe (forall a. HasCallStack => [Char] -> a
error [Char]
"internal error, op vars must always be pinned!!") forall a b. a -> Either a b
Left forall a b. (a -> b) -> a -> b
$ Pinned VCObjectHash -> Maybe VCObjectHash
pinnedToMaybe Pinned VCObjectHash
mHash)
          let (Set TypeClass
tcs, ImplType
t) = forall ty. TypeMetadata ty -> ty
ty TypeMetadata (Set TypeClass, ImplType)
meta
          Location SourcePos
-> TypeMetadata (Set TypeClass, ImplType) -> Infer ()
attachTypeToPosition Location SourcePos
exprLoc TypeMetadata (Set TypeClass, ImplType)
meta
          forall (m :: * -> *) a. Monad m => a -> m a
return (Expr (Pinned VCObjectHash) SourcePos
expr, ImplType
t, forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map (forall a b. b -> Either a b
Right forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Location SourcePos
exprLoc,)) Set TypeClass
tcs)
        TypeRep SourcePos
_pos InfernoType
t -> forall (m :: * -> *) a. Monad m => a -> m a
return (Expr (Pinned VCObjectHash) SourcePos
expr, Map ExtIdent InfernoType -> InfernoType -> ImplType
ImplType forall a. Monoid a => a
mempty forall a b. (a -> b) -> a -> b
$ InfernoType -> InfernoType
TRep InfernoType
t, forall a. Set a
Set.empty)
        Enum SourcePos
_ Pinned VCObjectHash
mHash Scoped ModuleName
_ Ident
_ -> do
          TypeMetadata (Set TypeClass, ImplType)
meta <- Location SourcePos
-> Either VCObjectHash ExtIdent
-> Infer (TypeMetadata (Set TypeClass, ImplType))
lookupEnv Location SourcePos
exprLoc (forall b a. b -> (a -> b) -> Maybe a -> b
maybe (forall a. HasCallStack => [Char] -> a
error [Char]
"internal error, enums must always be pinned!!") forall a b. a -> Either a b
Left forall a b. (a -> b) -> a -> b
$ Pinned VCObjectHash -> Maybe VCObjectHash
pinnedToMaybe Pinned VCObjectHash
mHash)
          let (Set TypeClass
_, ImplType
t) = forall ty. TypeMetadata ty -> ty
ty TypeMetadata (Set TypeClass, ImplType)
meta
          Location SourcePos
-> TypeMetadata (Set TypeClass, ImplType) -> Infer ()
attachTypeToPosition Location SourcePos
exprLoc TypeMetadata (Set TypeClass, ImplType)
meta {identExpr :: Expr () ()
identExpr = forall (p :: * -> * -> *) a b c d.
Bifunctor p =>
(a -> b) -> (c -> d) -> p a c -> p b d
bimap (forall a b. a -> b -> a
const ()) (forall a b. a -> b -> a
const ()) forall a b. (a -> b) -> a -> b
$ Expr (Pinned VCObjectHash) SourcePos
expr}
          forall (m :: * -> *) a. Monad m => a -> m a
return (Expr (Pinned VCObjectHash) SourcePos
expr, ImplType
t, forall a. Set a
Set.empty)
        InterpolatedString SourcePos
p1 SomeIStr
  (SourcePos, Expr (Pinned VCObjectHash) SourcePos, SourcePos)
xs SourcePos
p2 -> do
          Location SourcePos
-> TypeMetadata (Set TypeClass, ImplType) -> Infer ()
attachTypeToPosition
            Location SourcePos
exprLoc
            TypeMetadata
              { identExpr :: Expr () ()
identExpr = forall (p :: * -> * -> *) a b c d.
Bifunctor p =>
(a -> b) -> (c -> d) -> p a c -> p b d
bimap (forall a b. a -> b -> a
const ()) (forall a b. a -> b -> a
const ()) forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) pos. BlockUtils f => f pos -> f pos
removeComments Expr (Pinned VCObjectHash) SourcePos
expr,
                ty :: (Set TypeClass, ImplType)
ty = (forall a. Set a
Set.empty, Map ExtIdent InfernoType -> InfernoType -> ImplType
ImplType forall k a. Map k a
Map.empty InfernoType
typeText),
                docs :: Maybe Text
docs = forall a. Maybe a
Nothing
              }
          ([Either
   Text (SourcePos, Expr (Pinned VCObjectHash) SourcePos, SourcePos)]
xs', [Map ExtIdent InfernoType]
is, [Set Constraint]
css) <-
            forall a b c. [(a, b, c)] -> ([a], [b], [c])
unzip3
              forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ( forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM (forall e. SomeIStr e -> [Either Text e]
toEitherList SomeIStr
  (SourcePos, Expr (Pinned VCObjectHash) SourcePos, SourcePos)
xs) forall a b. (a -> b) -> a -> b
$ \case
                      Left Text
str -> forall (m :: * -> *) a. Monad m => a -> m a
return (forall a b. a -> Either a b
Left Text
str, forall k a. Map k a
Map.empty, forall a. Set a
Set.empty)
                      Right (SourcePos
p3, Expr (Pinned VCObjectHash) SourcePos
e, SourcePos
p4) -> (\(Expr (Pinned VCObjectHash) SourcePos
e', ImplType Map ExtIdent InfernoType
is InfernoType
_t, Set Constraint
cs) -> (forall a b. b -> Either a b
Right (SourcePos
p3, Expr (Pinned VCObjectHash) SourcePos
e', SourcePos
p4), Map ExtIdent InfernoType
is, Set Constraint
cs)) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr (Pinned VCObjectHash) SourcePos
-> Infer
     (Expr (Pinned VCObjectHash) SourcePos, ImplType, Set Constraint)
infer Expr (Pinned VCObjectHash) SourcePos
e
                  )
          let (Map ExtIdent InfernoType
isMerged, [Constraint]
ics) = Location SourcePos
-> [Map ExtIdent InfernoType]
-> (Map ExtIdent InfernoType, [Constraint])
mergeImplicitMaps (forall (f :: * -> *).
BlockUtils f =>
f SourcePos -> Location SourcePos
blockPosition Expr (Pinned VCObjectHash) SourcePos
expr) [Map ExtIdent InfernoType]
is
          forall (m :: * -> *) a. Monad m => a -> m a
return (forall hash pos.
pos -> SomeIStr (pos, Expr hash pos, pos) -> pos -> Expr hash pos
InterpolatedString SourcePos
p1 (forall e. [Either Text e] -> SomeIStr e
fromEitherList [Either
   Text (SourcePos, Expr (Pinned VCObjectHash) SourcePos, SourcePos)]
xs') SourcePos
p2, Map ExtIdent InfernoType -> InfernoType -> ImplType
ImplType Map ExtIdent InfernoType
isMerged InfernoType
typeText, forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
Set.unions [Set Constraint]
css forall a. Ord a => Set a -> Set a -> Set a
`Set.union` forall a. Ord a => [a] -> Set a
Set.fromList [Constraint]
ics)
        Array SourcePos
_ [] SourcePos
_ -> do
          InfernoType
tv <- Infer InfernoType
fresh
          let meta :: TypeMetadata (Set a, ImplType)
meta =
                TypeMetadata
                  { identExpr :: Expr () ()
identExpr = forall (p :: * -> * -> *) a b c d.
Bifunctor p =>
(a -> b) -> (c -> d) -> p a c -> p b d
bimap (forall a b. a -> b -> a
const ()) (forall a b. a -> b -> a
const ()) forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) pos. BlockUtils f => f pos -> f pos
removeComments Expr (Pinned VCObjectHash) SourcePos
expr,
                    ty :: (Set a, ImplType)
ty = (forall a. Set a
Set.empty, Map ExtIdent InfernoType -> InfernoType -> ImplType
ImplType forall k a. Map k a
Map.empty forall a b. (a -> b) -> a -> b
$ InfernoType -> InfernoType
TArray InfernoType
tv),
                    docs :: Maybe Text
docs = forall a. Maybe a
Nothing
                  }
          let (Set Any
_, ImplType
t) = forall ty. TypeMetadata ty -> ty
ty forall {a}. TypeMetadata (Set a, ImplType)
meta
          Location SourcePos
-> TypeMetadata (Set TypeClass, ImplType) -> Infer ()
attachTypeToPosition Location SourcePos
exprLoc forall {a}. TypeMetadata (Set a, ImplType)
meta
          forall (m :: * -> *) a. Monad m => a -> m a
return (Expr (Pinned VCObjectHash) SourcePos
expr, ImplType
t, forall a. Set a
Set.empty)
        Array SourcePos
p1 ((Expr (Pinned VCObjectHash) SourcePos
e, Maybe SourcePos
p2) : [(Expr (Pinned VCObjectHash) SourcePos, Maybe SourcePos)]
es) SourcePos
p3 -> do
          (Expr (Pinned VCObjectHash) SourcePos
e', ImplType Map ExtIdent InfernoType
i InfernoType
t, Set Constraint
cs) <- Expr (Pinned VCObjectHash) SourcePos
-> Infer
     (Expr (Pinned VCObjectHash) SourcePos, ImplType, Set Constraint)
infer Expr (Pinned VCObjectHash) SourcePos
e
          ([(Expr (Pinned VCObjectHash) SourcePos, Maybe SourcePos)]
es', [Map ExtIdent InfernoType]
impls, Set Constraint
cs') <- forall {b}.
InfernoType
-> [(Expr (Pinned VCObjectHash) SourcePos, b)]
-> ReaderT
     Env
     (StateT InferState (ExceptT [TypeError SourcePos] Identity))
     ([(Expr (Pinned VCObjectHash) SourcePos, b)],
      [Map ExtIdent InfernoType], Set Constraint)
go InfernoType
t [(Expr (Pinned VCObjectHash) SourcePos, Maybe SourcePos)]
es
          let (Map ExtIdent InfernoType
isMerged, [Constraint]
ics) = Location SourcePos
-> [Map ExtIdent InfernoType]
-> (Map ExtIdent InfernoType, [Constraint])
mergeImplicitMaps (forall (f :: * -> *).
BlockUtils f =>
f SourcePos -> Location SourcePos
blockPosition Expr (Pinned VCObjectHash) SourcePos
expr) forall a b. (a -> b) -> a -> b
$ Map ExtIdent InfernoType
i forall a. a -> [a] -> [a]
: [Map ExtIdent InfernoType]
impls
          let inferredTy :: ImplType
inferredTy = Map ExtIdent InfernoType -> InfernoType -> ImplType
ImplType Map ExtIdent InfernoType
isMerged forall a b. (a -> b) -> a -> b
$ InfernoType -> InfernoType
TArray InfernoType
t
          Location SourcePos
-> TypeMetadata (Set TypeClass, ImplType) -> Infer ()
attachTypeToPosition
            Location SourcePos
exprLoc
            TypeMetadata
              { identExpr :: Expr () ()
identExpr = forall (p :: * -> * -> *) a b c d.
Bifunctor p =>
(a -> b) -> (c -> d) -> p a c -> p b d
bimap (forall a b. a -> b -> a
const ()) (forall a b. a -> b -> a
const ()) forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) pos. BlockUtils f => f pos -> f pos
removeComments Expr (Pinned VCObjectHash) SourcePos
expr,
                ty :: (Set TypeClass, ImplType)
ty = (forall a. Set a
Set.empty, ImplType
inferredTy),
                docs :: Maybe Text
docs = forall a. Maybe a
Nothing
              }

          forall (m :: * -> *) a. Monad m => a -> m a
return
            ( forall hash pos.
pos -> [(Expr hash pos, Maybe pos)] -> pos -> Expr hash pos
Array SourcePos
p1 ((Expr (Pinned VCObjectHash) SourcePos
e', Maybe SourcePos
p2) forall a. a -> [a] -> [a]
: [(Expr (Pinned VCObjectHash) SourcePos, Maybe SourcePos)]
es') SourcePos
p3,
              ImplType
inferredTy,
              forall a. Ord a => [a] -> Set a
Set.fromList [Constraint]
ics forall a. Ord a => Set a -> Set a -> Set a
`Set.union` Set Constraint
cs forall a. Ord a => Set a -> Set a -> Set a
`Set.union` Set Constraint
cs'
            )
          where
            go :: InfernoType
-> [(Expr (Pinned VCObjectHash) SourcePos, b)]
-> ReaderT
     Env
     (StateT InferState (ExceptT [TypeError SourcePos] Identity))
     ([(Expr (Pinned VCObjectHash) SourcePos, b)],
      [Map ExtIdent InfernoType], Set Constraint)
go InfernoType
_t [] = forall (m :: * -> *) a. Monad m => a -> m a
return ([], [], forall a. Set a
Set.empty)
            go InfernoType
t ((Expr (Pinned VCObjectHash) SourcePos
e', b
p4) : [(Expr (Pinned VCObjectHash) SourcePos, b)]
es') = do
              (Expr (Pinned VCObjectHash) SourcePos
e'', ImplType Map ExtIdent InfernoType
i InfernoType
t', Set Constraint
cs) <- Expr (Pinned VCObjectHash) SourcePos
-> Infer
     (Expr (Pinned VCObjectHash) SourcePos, ImplType, Set Constraint)
infer Expr (Pinned VCObjectHash) SourcePos
e'
              ([(Expr (Pinned VCObjectHash) SourcePos, b)]
es'', [Map ExtIdent InfernoType]
impls, Set Constraint
csRest) <- InfernoType
-> [(Expr (Pinned VCObjectHash) SourcePos, b)]
-> ReaderT
     Env
     (StateT InferState (ExceptT [TypeError SourcePos] Identity))
     ([(Expr (Pinned VCObjectHash) SourcePos, b)],
      [Map ExtIdent InfernoType], Set Constraint)
go InfernoType
t [(Expr (Pinned VCObjectHash) SourcePos, b)]
es'
              forall (m :: * -> *) a. Monad m => a -> m a
return
                ( (Expr (Pinned VCObjectHash) SourcePos
e'', b
p4) forall a. a -> [a] -> [a]
: [(Expr (Pinned VCObjectHash) SourcePos, b)]
es'',
                  Map ExtIdent InfernoType
i forall a. a -> [a] -> [a]
: [Map ExtIdent InfernoType]
impls,
                  Set Constraint
cs
                    forall a. Ord a => Set a -> Set a -> Set a
`Set.union` Set Constraint
csRest
                    forall a. Ord a => Set a -> Set a -> Set a
`Set.union` forall a. Ord a => [a] -> Set a
Set.fromList
                      [ forall a b c d. a -> b -> c -> Either (a, b, c) d
tyConstr
                          InfernoType
t
                          InfernoType
t'
                          [ forall a.
Set TypeClass
-> InfernoType -> InfernoType -> Location a -> TypeError a
UnificationFail
                              (forall a. Ord a => [a] -> Set a
Set.fromList forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> b
snd forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. [Either a b] -> [b]
rights forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Set a -> [a]
Set.toList forall a b. (a -> b) -> a -> b
$ Set Constraint
cs forall a. Ord a => Set a -> Set a -> Set a
`Set.union` Set Constraint
csRest)
                              InfernoType
t
                              InfernoType
t'
                              forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *).
BlockUtils f =>
f SourcePos -> Location SourcePos
blockPosition Expr (Pinned VCObjectHash) SourcePos
e'
                          ]
                      ]
                )
        ArrayComp SourcePos
p1 Expr (Pinned VCObjectHash) SourcePos
e SourcePos
p2 NonEmpty
  (SourcePos, Ident, SourcePos, Expr (Pinned VCObjectHash) SourcePos,
   Maybe SourcePos)
sels Maybe (SourcePos, Expr (Pinned VCObjectHash) SourcePos)
cond SourcePos
p3 -> do
          ()
_ <- forall b.
[(SourcePos, Ident, SourcePos, b, Maybe SourcePos)] -> Infer ()
checkVariableOverlap forall a b. (a -> b) -> a -> b
$ forall a. NonEmpty a -> [a]
NEList.toList NonEmpty
  (SourcePos, Ident, SourcePos, Expr (Pinned VCObjectHash) SourcePos,
   Maybe SourcePos)
sels
          ([(SourcePos, Ident, SourcePos,
  Expr (Pinned VCObjectHash) SourcePos, Maybe SourcePos)]
sels', [(ExtIdent, TypeMetadata TCScheme)]
vars, [Map ExtIdent InfernoType]
is, [Set Constraint]
css) <- forall a b c d. [(a, b, c, d)] -> ([a], [b], [c], [d])
unzip4 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall {a} {c} {e} {d}.
Ord a =>
[(SourcePos, Ident, c, Expr (Pinned VCObjectHash) SourcePos, e)]
-> (Infer
      (Expr (Pinned VCObjectHash) SourcePos, ImplType, Set Constraint)
    -> Infer
         (d, ImplType,
          Set
            (Either
               (InfernoType, InfernoType, [TypeError SourcePos]) (a, TypeClass))))
-> ReaderT
     Env
     (StateT InferState (ExceptT [TypeError SourcePos] Identity))
     [((SourcePos, Ident, c, d, e), (ExtIdent, TypeMetadata TCScheme),
       Map ExtIdent InfernoType,
       Set
         (Either
            (InfernoType, InfernoType, [TypeError SourcePos]) (a, TypeClass)))]
go (forall a. NonEmpty a -> [a]
NEList.toList NonEmpty
  (SourcePos, Ident, SourcePos, Expr (Pinned VCObjectHash) SourcePos,
   Maybe SourcePos)
sels) forall a. a -> a
id

          (Expr (Pinned VCObjectHash) SourcePos
e', ImplType Map ExtIdent InfernoType
i_e InfernoType
t_e, Set Constraint
c_e) <- forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr forall a. (ExtIdent, TypeMetadata TCScheme) -> Infer a -> Infer a
inEnv (Expr (Pinned VCObjectHash) SourcePos
-> Infer
     (Expr (Pinned VCObjectHash) SourcePos, ImplType, Set Constraint)
infer Expr (Pinned VCObjectHash) SourcePos
e) [(ExtIdent, TypeMetadata TCScheme)]
vars

          (Maybe (SourcePos, Expr (Pinned VCObjectHash) SourcePos)
cond', Map ExtIdent InfernoType
i_cond, Set Constraint
c_cond) <- case Maybe (SourcePos, Expr (Pinned VCObjectHash) SourcePos)
cond of
            Just (SourcePos
p4, Expr (Pinned VCObjectHash) SourcePos
e_cond) -> do
              (Expr (Pinned VCObjectHash) SourcePos
e_cond', ImplType Map ExtIdent InfernoType
i_cond InfernoType
t_cond, Set Constraint
c_cond) <- forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr forall a. (ExtIdent, TypeMetadata TCScheme) -> Infer a -> Infer a
inEnv (Expr (Pinned VCObjectHash) SourcePos
-> Infer
     (Expr (Pinned VCObjectHash) SourcePos, ImplType, Set Constraint)
infer Expr (Pinned VCObjectHash) SourcePos
e_cond) [(ExtIdent, TypeMetadata TCScheme)]
vars
              forall (m :: * -> *) a. Monad m => a -> m a
return
                ( forall a. a -> Maybe a
Just (SourcePos
p4, Expr (Pinned VCObjectHash) SourcePos
e_cond'),
                  Map ExtIdent InfernoType
i_cond,
                  Set Constraint
c_cond
                    forall a. Ord a => Set a -> Set a -> Set a
`Set.union` forall a. a -> Set a
Set.singleton (forall a b c d. a -> b -> c -> Either (a, b, c) d
tyConstr InfernoType
t_cond InfernoType
typeBool [forall a.
Set TypeClass
-> InfernoType -> InfernoType -> Location a -> TypeError a
UnificationFail (forall a. Ord a => [a] -> Set a
Set.fromList forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> b
snd forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. [Either a b] -> [b]
rights forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Set a -> [a]
Set.toList forall a b. (a -> b) -> a -> b
$ Set Constraint
c_cond) InfernoType
t_cond InfernoType
typeBool forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *).
BlockUtils f =>
f SourcePos -> Location SourcePos
blockPosition Expr (Pinned VCObjectHash) SourcePos
e_cond])
                )
            Maybe (SourcePos, Expr (Pinned VCObjectHash) SourcePos)
Nothing -> forall (m :: * -> *) a. Monad m => a -> m a
return (forall a. Maybe a
Nothing, forall k a. Map k a
Map.empty, forall a. Set a
Set.empty)

          let (Map ExtIdent InfernoType
isMerged, [Constraint]
ics) = Location SourcePos
-> [Map ExtIdent InfernoType]
-> (Map ExtIdent InfernoType, [Constraint])
mergeImplicitMaps (forall (f :: * -> *).
BlockUtils f =>
f SourcePos -> Location SourcePos
blockPosition Expr (Pinned VCObjectHash) SourcePos
expr) forall a b. (a -> b) -> a -> b
$ [Map ExtIdent InfernoType
i_e, Map ExtIdent InfernoType
i_cond] forall a. [a] -> [a] -> [a]
++ [Map ExtIdent InfernoType]
is
          forall (m :: * -> *) a. Monad m => a -> m a
return
            ( forall hash pos.
pos
-> Expr hash pos
-> pos
-> NonEmpty (pos, Ident, pos, Expr hash pos, Maybe pos)
-> Maybe (pos, Expr hash pos)
-> pos
-> Expr hash pos
ArrayComp SourcePos
p1 Expr (Pinned VCObjectHash) SourcePos
e' SourcePos
p2 (forall a. [a] -> NonEmpty a
NEList.fromList [(SourcePos, Ident, SourcePos,
  Expr (Pinned VCObjectHash) SourcePos, Maybe SourcePos)]
sels') Maybe (SourcePos, Expr (Pinned VCObjectHash) SourcePos)
cond' SourcePos
p3,
              Map ExtIdent InfernoType -> InfernoType -> ImplType
ImplType Map ExtIdent InfernoType
isMerged (InfernoType -> InfernoType
TArray InfernoType
t_e),
              forall a. Ord a => [a] -> Set a
Set.fromList [Constraint]
ics
                forall a. Ord a => Set a -> Set a -> Set a
`Set.union` Set Constraint
c_e
                forall a. Ord a => Set a -> Set a -> Set a
`Set.union` Set Constraint
c_cond
                forall a. Ord a => Set a -> Set a -> Set a
`Set.union` forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
Set.unions [Set Constraint]
css
            )
          where
            go :: [(SourcePos, Ident, c, Expr (Pinned VCObjectHash) SourcePos, e)]
-> (Infer
      (Expr (Pinned VCObjectHash) SourcePos, ImplType, Set Constraint)
    -> Infer
         (d, ImplType,
          Set
            (Either
               (InfernoType, InfernoType, [TypeError SourcePos]) (a, TypeClass))))
-> ReaderT
     Env
     (StateT InferState (ExceptT [TypeError SourcePos] Identity))
     [((SourcePos, Ident, c, d, e), (ExtIdent, TypeMetadata TCScheme),
       Map ExtIdent InfernoType,
       Set
         (Either
            (InfernoType, InfernoType, [TypeError SourcePos]) (a, TypeClass)))]
go [] Infer
  (Expr (Pinned VCObjectHash) SourcePos, ImplType, Set Constraint)
-> Infer
     (d, ImplType,
      Set
        (Either
           (InfernoType, InfernoType, [TypeError SourcePos]) (a, TypeClass)))
_ = forall (m :: * -> *) a. Monad m => a -> m a
return []
            go ((SourcePos
pos, Ident Text
x, c
p4, Expr (Pinned VCObjectHash) SourcePos
e_s, e
p5) : [(SourcePos, Ident, c, Expr (Pinned VCObjectHash) SourcePos, e)]
xs) Infer
  (Expr (Pinned VCObjectHash) SourcePos, ImplType, Set Constraint)
-> Infer
     (d, ImplType,
      Set
        (Either
           (InfernoType, InfernoType, [TypeError SourcePos]) (a, TypeClass)))
f = do
              (d
e_s', ImplType Map ExtIdent InfernoType
i_s InfernoType
t_s, Set
  (Either
     (InfernoType, InfernoType, [TypeError SourcePos]) (a, TypeClass))
c_s) <- Infer
  (Expr (Pinned VCObjectHash) SourcePos, ImplType, Set Constraint)
-> Infer
     (d, ImplType,
      Set
        (Either
           (InfernoType, InfernoType, [TypeError SourcePos]) (a, TypeClass)))
f forall a b. (a -> b) -> a -> b
$ Expr (Pinned VCObjectHash) SourcePos
-> Infer
     (Expr (Pinned VCObjectHash) SourcePos, ImplType, Set Constraint)
infer Expr (Pinned VCObjectHash) SourcePos
e_s
              InfernoType
tv <- Infer InfernoType
fresh
              Location SourcePos
-> TypeMetadata (Set TypeClass, ImplType) -> Infer ()
attachTypeToPosition
                (forall a. ElementPosition a => SourcePos -> a -> Location SourcePos
elementPosition SourcePos
pos forall a b. (a -> b) -> a -> b
$ Text -> Ident
Ident Text
x)
                TypeMetadata
                  { identExpr :: Expr () ()
identExpr = forall hash pos.
pos -> hash -> Scoped ModuleName -> ImplExpl -> Expr hash pos
Var () () forall a. Scoped a
LocalScope forall a b. (a -> b) -> a -> b
$ ExtIdent -> ImplExpl
Expl forall a b. (a -> b) -> a -> b
$ Either Int Text -> ExtIdent
ExtIdent forall a b. (a -> b) -> a -> b
$ forall a b. b -> Either a b
Right Text
x,
                    ty :: (Set TypeClass, ImplType)
ty = (forall a. Ord a => [a] -> Set a
Set.fromList forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> b
snd forall a b. (a -> b) -> a -> b
$ forall a b. [Either a b] -> [b]
rights forall a b. (a -> b) -> a -> b
$ forall a. Set a -> [a]
Set.toList Set
  (Either
     (InfernoType, InfernoType, [TypeError SourcePos]) (a, TypeClass))
c_s, Map ExtIdent InfernoType -> InfernoType -> ImplType
ImplType Map ExtIdent InfernoType
i_s InfernoType
tv),
                    docs :: Maybe Text
docs = forall a. Maybe a
Nothing
                  }
              let newEnv :: (ExtIdent, TypeMetadata TCScheme)
newEnv =
                    ( Either Int Text -> ExtIdent
ExtIdent forall a b. (a -> b) -> a -> b
$ forall a b. b -> Either a b
Right Text
x,
                      TypeMetadata
                        { identExpr :: Expr () ()
identExpr = forall hash pos.
pos -> hash -> Scoped ModuleName -> ImplExpl -> Expr hash pos
Var () () forall a. Scoped a
LocalScope forall a b. (a -> b) -> a -> b
$ ExtIdent -> ImplExpl
Expl forall a b. (a -> b) -> a -> b
$ Either Int Text -> ExtIdent
ExtIdent forall a b. (a -> b) -> a -> b
$ forall a b. b -> Either a b
Right Text
x,
                          ty :: TCScheme
ty = [TV] -> Set TypeClass -> ImplType -> TCScheme
ForallTC [] (forall a. Ord a => [a] -> Set a
Set.fromList forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> b
snd forall a b. (a -> b) -> a -> b
$ forall a b. [Either a b] -> [b]
rights forall a b. (a -> b) -> a -> b
$ forall a. Set a -> [a]
Set.toList Set
  (Either
     (InfernoType, InfernoType, [TypeError SourcePos]) (a, TypeClass))
c_s) forall a b. (a -> b) -> a -> b
$ Map ExtIdent InfernoType -> InfernoType -> ImplType
ImplType Map ExtIdent InfernoType
i_s InfernoType
tv,
                          docs :: Maybe Text
docs = forall a. Maybe a
Nothing
                        }
                    )
              [((SourcePos, Ident, c, d, e), (ExtIdent, TypeMetadata TCScheme),
  Map ExtIdent InfernoType,
  Set
    (Either
       (InfernoType, InfernoType, [TypeError SourcePos]) (a, TypeClass)))]
rest <- [(SourcePos, Ident, c, Expr (Pinned VCObjectHash) SourcePos, e)]
-> (Infer
      (Expr (Pinned VCObjectHash) SourcePos, ImplType, Set Constraint)
    -> Infer
         (d, ImplType,
          Set
            (Either
               (InfernoType, InfernoType, [TypeError SourcePos]) (a, TypeClass))))
-> ReaderT
     Env
     (StateT InferState (ExceptT [TypeError SourcePos] Identity))
     [((SourcePos, Ident, c, d, e), (ExtIdent, TypeMetadata TCScheme),
       Map ExtIdent InfernoType,
       Set
         (Either
            (InfernoType, InfernoType, [TypeError SourcePos]) (a, TypeClass)))]
go [(SourcePos, Ident, c, Expr (Pinned VCObjectHash) SourcePos, e)]
xs (forall a. (ExtIdent, TypeMetadata TCScheme) -> Infer a -> Infer a
inEnv (ExtIdent, TypeMetadata TCScheme)
newEnv forall b c a. (b -> c) -> (a -> b) -> a -> c
. Infer
  (Expr (Pinned VCObjectHash) SourcePos, ImplType, Set Constraint)
-> Infer
     (d, ImplType,
      Set
        (Either
           (InfernoType, InfernoType, [TypeError SourcePos]) (a, TypeClass)))
f)
              forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$
                ( (SourcePos
pos, Text -> Ident
Ident Text
x, c
p4, d
e_s', e
p5),
                  (ExtIdent, TypeMetadata TCScheme)
newEnv,
                  Map ExtIdent InfernoType
i_s,
                  Set
  (Either
     (InfernoType, InfernoType, [TypeError SourcePos]) (a, TypeClass))
c_s forall a. Ord a => Set a -> Set a -> Set a
`Set.union` forall a. a -> Set a
Set.singleton (forall a b c d. a -> b -> c -> Either (a, b, c) d
tyConstr InfernoType
t_s (InfernoType -> InfernoType
TArray InfernoType
tv) [forall a.
Set TypeClass
-> InfernoType -> InfernoType -> Location a -> TypeError a
UnificationFail (forall a. Ord a => [a] -> Set a
Set.fromList forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> b
snd forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. [Either a b] -> [b]
rights forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Set a -> [a]
Set.toList forall a b. (a -> b) -> a -> b
$ Set
  (Either
     (InfernoType, InfernoType, [TypeError SourcePos]) (a, TypeClass))
c_s) InfernoType
t_s (InfernoType -> InfernoType
TArray InfernoType
tv) forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *).
BlockUtils f =>
f SourcePos -> Location SourcePos
blockPosition Expr (Pinned VCObjectHash) SourcePos
e_s])
                )
                  forall a. a -> [a] -> [a]
: [((SourcePos, Ident, c, d, e), (ExtIdent, TypeMetadata TCScheme),
  Map ExtIdent InfernoType,
  Set
    (Either
       (InfernoType, InfernoType, [TypeError SourcePos]) (a, TypeClass)))]
rest

            checkVariableOverlap :: [(SourcePos, Ident, SourcePos, b, Maybe SourcePos)] -> Infer ()
            checkVariableOverlap :: forall b.
[(SourcePos, Ident, SourcePos, b, Maybe SourcePos)] -> Infer ()
checkVariableOverlap = \case
              [] -> forall (m :: * -> *) a. Monad m => a -> m a
return ()
              (SourcePos
loc, Ident
x, SourcePos
_, b
_e, Maybe SourcePos
_) : [(SourcePos, Ident, SourcePos, b, Maybe SourcePos)]
xs -> case forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Maybe a
find (\(SourcePos
_, Ident
x', SourcePos
_, b
_, Maybe SourcePos
_) -> Ident
x forall a. Eq a => a -> a -> Bool
== Ident
x') [(SourcePos, Ident, SourcePos, b, Maybe SourcePos)]
xs of
                Just (SourcePos
loc', Ident
x', SourcePos
_, b
_, Maybe SourcePos
_) -> forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError [forall a. Ident -> Location a -> Location a -> TypeError a
VarMultipleOccurrence Ident
x (forall a. ElementPosition a => SourcePos -> a -> Location SourcePos
elementPosition SourcePos
loc Ident
x) (forall a. ElementPosition a => SourcePos -> a -> Location SourcePos
elementPosition SourcePos
loc' Ident
x')]
                Maybe (SourcePos, Ident, SourcePos, b, Maybe SourcePos)
Nothing -> forall b.
[(SourcePos, Ident, SourcePos, b, Maybe SourcePos)] -> Infer ()
checkVariableOverlap [(SourcePos, Ident, SourcePos, b, Maybe SourcePos)]
xs
        Lam SourcePos
p1 NonEmpty (SourcePos, Maybe ExtIdent)
args SourcePos
p2 Expr (Pinned VCObjectHash) SourcePos
e -> do
          (Expr (Pinned VCObjectHash) SourcePos
e', ImplType
ty, Set Constraint
cs) <- [(SourcePos, Maybe ExtIdent)]
-> Infer
     (Expr (Pinned VCObjectHash) SourcePos, ImplType, Set Constraint)
go forall a b. (a -> b) -> a -> b
$ forall a. NonEmpty a -> [a]
NEList.toList NonEmpty (SourcePos, Maybe ExtIdent)
args
          forall (m :: * -> *) a. Monad m => a -> m a
return (forall hash pos.
pos
-> NonEmpty (pos, Maybe ExtIdent)
-> pos
-> Expr hash pos
-> Expr hash pos
Lam SourcePos
p1 NonEmpty (SourcePos, Maybe ExtIdent)
args SourcePos
p2 Expr (Pinned VCObjectHash) SourcePos
e', ImplType
ty, Set Constraint
cs)
          where
            go :: [(SourcePos, Maybe ExtIdent)]
-> Infer
     (Expr (Pinned VCObjectHash) SourcePos, ImplType, Set Constraint)
go = \case
              [] -> Expr (Pinned VCObjectHash) SourcePos
-> Infer
     (Expr (Pinned VCObjectHash) SourcePos, ImplType, Set Constraint)
infer Expr (Pinned VCObjectHash) SourcePos
e
              (SourcePos
pos, Just ExtIdent
x) : [(SourcePos, Maybe ExtIdent)]
xs -> do
                InfernoType
tv <- Infer InfernoType
fresh
                let newEnv :: (ExtIdent, TypeMetadata TCScheme)
newEnv =
                      ( ExtIdent
x,
                        TypeMetadata
                          { identExpr :: Expr () ()
identExpr = forall hash pos.
pos -> hash -> Scoped ModuleName -> ImplExpl -> Expr hash pos
Var () () forall a. Scoped a
LocalScope forall a b. (a -> b) -> a -> b
$ ExtIdent -> ImplExpl
Expl ExtIdent
x,
                            ty :: TCScheme
ty = [TV] -> Set TypeClass -> ImplType -> TCScheme
ForallTC [] forall a. Set a
Set.empty forall a b. (a -> b) -> a -> b
$ Map ExtIdent InfernoType -> InfernoType -> ImplType
ImplType forall k a. Map k a
Map.empty InfernoType
tv,
                            docs :: Maybe Text
docs = forall a. Maybe a
Nothing
                          }
                      )
                (Expr (Pinned VCObjectHash) SourcePos
e', ImplType Map ExtIdent InfernoType
is InfernoType
t, Set Constraint
cs) <- forall a. (ExtIdent, TypeMetadata TCScheme) -> Infer a -> Infer a
inEnv (ExtIdent, TypeMetadata TCScheme)
newEnv forall a b. (a -> b) -> a -> b
$ [(SourcePos, Maybe ExtIdent)]
-> Infer
     (Expr (Pinned VCObjectHash) SourcePos, ImplType, Set Constraint)
go [(SourcePos, Maybe ExtIdent)]
xs
                case ExtIdent
x of
                  ExtIdent (Left Int
_) -> forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
                  ExtIdent (Right Text
i) ->
                    Location SourcePos
-> TypeMetadata (Set TypeClass, ImplType) -> Infer ()
attachTypeToPosition
                      (forall a. ElementPosition a => SourcePos -> a -> Location SourcePos
elementPosition SourcePos
pos forall a b. (a -> b) -> a -> b
$ forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ Text -> Ident
Ident Text
i)
                      TypeMetadata
                        { identExpr :: Expr () ()
identExpr = forall hash pos.
pos -> hash -> Scoped ModuleName -> ImplExpl -> Expr hash pos
Var () () forall a. Scoped a
LocalScope forall a b. (a -> b) -> a -> b
$ ExtIdent -> ImplExpl
Expl ExtIdent
x,
                          ty :: (Set TypeClass, ImplType)
ty = (forall a. Set a
Set.empty, Map ExtIdent InfernoType -> InfernoType -> ImplType
ImplType forall k a. Map k a
Map.empty InfernoType
tv),
                          docs :: Maybe Text
docs = forall a. Maybe a
Nothing
                        }
                forall (m :: * -> *) a. Monad m => a -> m a
return (Expr (Pinned VCObjectHash) SourcePos
e', Map ExtIdent InfernoType -> InfernoType -> ImplType
ImplType Map ExtIdent InfernoType
is forall a b. (a -> b) -> a -> b
$ InfernoType
tv InfernoType -> InfernoType -> InfernoType
`TArr` InfernoType
t, Set Constraint
cs)
              (SourcePos
pos, Maybe ExtIdent
Nothing) : [(SourcePos, Maybe ExtIdent)]
xs -> do
                InfernoType
tv <- Infer InfernoType
fresh
                Location SourcePos
-> TypeMetadata (Set TypeClass, ImplType) -> Infer ()
attachTypeToPosition
                  (forall a. ElementPosition a => SourcePos -> a -> Location SourcePos
elementPosition SourcePos
pos (forall a. Maybe a
Nothing :: Maybe Ident))
                  TypeMetadata
                    { identExpr :: Expr () ()
identExpr = forall hash pos.
pos -> hash -> Scoped ModuleName -> ImplExpl -> Expr hash pos
Var () () forall a. Scoped a
LocalScope forall a b. (a -> b) -> a -> b
$ ExtIdent -> ImplExpl
Expl forall a b. (a -> b) -> a -> b
$ Either Int Text -> ExtIdent
ExtIdent forall a b. (a -> b) -> a -> b
$ forall a b. b -> Either a b
Right Text
"_",
                      ty :: (Set TypeClass, ImplType)
ty = (forall a. Set a
Set.empty, Map ExtIdent InfernoType -> InfernoType -> ImplType
ImplType forall k a. Map k a
Map.empty InfernoType
tv),
                      docs :: Maybe Text
docs = forall a. Maybe a
Nothing
                    }
                (Expr (Pinned VCObjectHash) SourcePos
e', ImplType Map ExtIdent InfernoType
is InfernoType
t, Set Constraint
cs) <- [(SourcePos, Maybe ExtIdent)]
-> Infer
     (Expr (Pinned VCObjectHash) SourcePos, ImplType, Set Constraint)
go [(SourcePos, Maybe ExtIdent)]
xs
                forall (m :: * -> *) a. Monad m => a -> m a
return (Expr (Pinned VCObjectHash) SourcePos
e', Map ExtIdent InfernoType -> InfernoType -> ImplType
ImplType Map ExtIdent InfernoType
is forall a b. (a -> b) -> a -> b
$ InfernoType
tv InfernoType -> InfernoType -> InfernoType
`TArr` InfernoType
t, Set Constraint
cs)
        App Expr (Pinned VCObjectHash) SourcePos
e1 Expr (Pinned VCObjectHash) SourcePos
e2 -> do
          (Expr (Pinned VCObjectHash) SourcePos
e1', ImplType Map ExtIdent InfernoType
i1 InfernoType
t1, Set Constraint
c1) <- Expr (Pinned VCObjectHash) SourcePos
-> Infer
     (Expr (Pinned VCObjectHash) SourcePos, ImplType, Set Constraint)
infer Expr (Pinned VCObjectHash) SourcePos
e1
          (Expr (Pinned VCObjectHash) SourcePos
e2', ImplType Map ExtIdent InfernoType
i2 InfernoType
t2, Set Constraint
c2) <- Expr (Pinned VCObjectHash) SourcePos
-> Infer
     (Expr (Pinned VCObjectHash) SourcePos, ImplType, Set Constraint)
infer Expr (Pinned VCObjectHash) SourcePos
e2

          case InfernoType
t1 of
            InfernoType
t1a `TArr` InfernoType
t1b -> do
              InfernoType
tv <- Infer InfernoType
fresh
              let (Map ExtIdent InfernoType
isMerged, [Constraint]
ics) = Location SourcePos
-> [Map ExtIdent InfernoType]
-> (Map ExtIdent InfernoType, [Constraint])
mergeImplicitMaps (forall (f :: * -> *).
BlockUtils f =>
f SourcePos -> Location SourcePos
blockPosition Expr (Pinned VCObjectHash) SourcePos
expr) [Map ExtIdent InfernoType
i1, Map ExtIdent InfernoType
i2]
                  tyCls :: Set TypeClass
tyCls = forall a. Ord a => [a] -> Set a
Set.fromList forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> b
snd forall a b. (a -> b) -> a -> b
$ forall a b. [Either a b] -> [b]
rights forall a b. (a -> b) -> a -> b
$ forall a. Set a -> [a]
Set.toList forall a b. (a -> b) -> a -> b
$ Set Constraint
c1 forall a. Ord a => Set a -> Set a -> Set a
`Set.union` Set Constraint
c2
              forall (m :: * -> *) a. Monad m => a -> m a
return
                ( forall hash pos. Expr hash pos -> Expr hash pos -> Expr hash pos
App Expr (Pinned VCObjectHash) SourcePos
e1' Expr (Pinned VCObjectHash) SourcePos
e2',
                  Map ExtIdent InfernoType -> InfernoType -> ImplType
ImplType Map ExtIdent InfernoType
isMerged InfernoType
tv,
                  forall a. Ord a => [a] -> Set a
Set.fromList [Constraint]
ics
                    forall a. Ord a => Set a -> Set a -> Set a
`Set.union` Set Constraint
c1
                    forall a. Ord a => Set a -> Set a -> Set a
`Set.union` Set Constraint
c2
                    forall a. Ord a => Set a -> Set a -> Set a
`Set.union` forall a. Ord a => [a] -> Set a
Set.fromList
                      [ forall a b c d. a -> b -> c -> Either (a, b, c) d
tyConstr InfernoType
t1a InfernoType
t2 [forall a.
Set TypeClass
-> InfernoType -> InfernoType -> Location a -> TypeError a
UnificationFail Set TypeClass
tyCls InfernoType
t1a InfernoType
t2 forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *).
BlockUtils f =>
f SourcePos -> Location SourcePos
blockPosition Expr (Pinned VCObjectHash) SourcePos
e2],
                        forall a b c d. a -> b -> c -> Either (a, b, c) d
tyConstr InfernoType
t1b InfernoType
tv [forall a.
Set TypeClass
-> InfernoType -> InfernoType -> Location a -> TypeError a
UnificationFail Set TypeClass
tyCls InfernoType
t1b InfernoType
tv forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *).
BlockUtils f =>
f SourcePos -> Location SourcePos
blockPosition Expr (Pinned VCObjectHash) SourcePos
expr]
                      ]
                )
            InfernoType
_ -> do
              InfernoType
tv <- Infer InfernoType
fresh
              let (Map ExtIdent InfernoType
isMerged, [Constraint]
ics) = Location SourcePos
-> [Map ExtIdent InfernoType]
-> (Map ExtIdent InfernoType, [Constraint])
mergeImplicitMaps (forall (f :: * -> *).
BlockUtils f =>
f SourcePos -> Location SourcePos
blockPosition Expr (Pinned VCObjectHash) SourcePos
expr) [Map ExtIdent InfernoType
i1, Map ExtIdent InfernoType
i2]
                  tyCls :: Set TypeClass
tyCls = forall a. Ord a => [a] -> Set a
Set.fromList forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> b
snd forall a b. (a -> b) -> a -> b
$ forall a b. [Either a b] -> [b]
rights forall a b. (a -> b) -> a -> b
$ forall a. Set a -> [a]
Set.toList forall a b. (a -> b) -> a -> b
$ Set Constraint
c1 forall a. Ord a => Set a -> Set a -> Set a
`Set.union` Set Constraint
c2
              -- if we end up on this branch, we will be throwing a unification error and
              -- want to highlight e1, thus we attach `blockPosition e1` to the error
              forall (m :: * -> *) a. Monad m => a -> m a
return
                ( forall hash pos. Expr hash pos -> Expr hash pos -> Expr hash pos
App Expr (Pinned VCObjectHash) SourcePos
e1' Expr (Pinned VCObjectHash) SourcePos
e2',
                  Map ExtIdent InfernoType -> InfernoType -> ImplType
ImplType Map ExtIdent InfernoType
isMerged InfernoType
tv,
                  forall a. Ord a => [a] -> Set a
Set.fromList [Constraint]
ics
                    forall a. Ord a => Set a -> Set a -> Set a
`Set.union` Set Constraint
c1
                    forall a. Ord a => Set a -> Set a -> Set a
`Set.union` Set Constraint
c2
                    forall a. Ord a => Set a -> Set a -> Set a
`Set.union` forall a. Ord a => [a] -> Set a
Set.fromList
                      [ forall a b c d. a -> b -> c -> Either (a, b, c) d
tyConstr InfernoType
t1 (InfernoType
t2 InfernoType -> InfernoType -> InfernoType
`TArr` InfernoType
tv) [forall a.
Set TypeClass
-> InfernoType -> InfernoType -> Location a -> TypeError a
ExpectedFunction Set TypeClass
tyCls (InfernoType
t2 InfernoType -> InfernoType -> InfernoType
`TArr` InfernoType
tv) InfernoType
t1 forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *).
BlockUtils f =>
f SourcePos -> Location SourcePos
blockPosition Expr (Pinned VCObjectHash) SourcePos
e1]
                      ]
                )

        -- non generalized let
        Let SourcePos
p1 SourcePos
loc (Expl ExtIdent
x) SourcePos
p2 Expr (Pinned VCObjectHash) SourcePos
e1 SourcePos
p3 Expr (Pinned VCObjectHash) SourcePos
e2 -> do
          (Expr (Pinned VCObjectHash) SourcePos
e1', ImplType Map ExtIdent InfernoType
i1 InfernoType
t1, Set Constraint
c1) <- Expr (Pinned VCObjectHash) SourcePos
-> Infer
     (Expr (Pinned VCObjectHash) SourcePos, ImplType, Set Constraint)
infer Expr (Pinned VCObjectHash) SourcePos
e1
          Location SourcePos
-> TypeMetadata (Set TypeClass, ImplType) -> Infer ()
attachTypeToPosition
            (forall a. ElementPosition a => SourcePos -> a -> Location SourcePos
elementPosition SourcePos
loc forall a b. (a -> b) -> a -> b
$ ExtIdent -> ImplExpl
Expl ExtIdent
x)
            TypeMetadata
              { identExpr :: Expr () ()
identExpr = forall hash pos.
pos -> hash -> Scoped ModuleName -> ImplExpl -> Expr hash pos
Var () () forall a. Scoped a
LocalScope forall a b. (a -> b) -> a -> b
$ ExtIdent -> ImplExpl
Expl ExtIdent
x,
                ty :: (Set TypeClass, ImplType)
ty = (forall a. Ord a => [a] -> Set a
Set.fromList forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> b
snd forall a b. (a -> b) -> a -> b
$ forall a b. [Either a b] -> [b]
rights forall a b. (a -> b) -> a -> b
$ forall a. Set a -> [a]
Set.toList Set Constraint
c1, Map ExtIdent InfernoType -> InfernoType -> ImplType
ImplType Map ExtIdent InfernoType
i1 InfernoType
t1),
                docs :: Maybe Text
docs = forall a. Maybe a
Nothing
              }

          let newEnv :: (ExtIdent, TypeMetadata TCScheme)
newEnv =
                ( ExtIdent
x,
                  TypeMetadata
                    { identExpr :: Expr () ()
identExpr = forall hash pos.
pos -> hash -> Scoped ModuleName -> ImplExpl -> Expr hash pos
Var () () forall a. Scoped a
LocalScope forall a b. (a -> b) -> a -> b
$ ExtIdent -> ImplExpl
Expl ExtIdent
x,
                      ty :: TCScheme
ty = [TV] -> Set TypeClass -> ImplType -> TCScheme
ForallTC [] (forall a. Ord a => [a] -> Set a
Set.fromList forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> b
snd forall a b. (a -> b) -> a -> b
$ forall a b. [Either a b] -> [b]
rights forall a b. (a -> b) -> a -> b
$ forall a. Set a -> [a]
Set.toList Set Constraint
c1) forall a b. (a -> b) -> a -> b
$ Map ExtIdent InfernoType -> InfernoType -> ImplType
ImplType Map ExtIdent InfernoType
i1 InfernoType
t1,
                      docs :: Maybe Text
docs = forall a. Maybe a
Nothing
                    }
                )
          (Expr (Pinned VCObjectHash) SourcePos
e2', ImplType Map ExtIdent InfernoType
i2 InfernoType
t2, Set Constraint
c2) <- forall a. (ExtIdent, TypeMetadata TCScheme) -> Infer a -> Infer a
inEnv (ExtIdent, TypeMetadata TCScheme)
newEnv forall a b. (a -> b) -> a -> b
$ Expr (Pinned VCObjectHash) SourcePos
-> Infer
     (Expr (Pinned VCObjectHash) SourcePos, ImplType, Set Constraint)
infer Expr (Pinned VCObjectHash) SourcePos
e2
          let (Map ExtIdent InfernoType
isMerged, [Constraint]
ics) = Location SourcePos
-> [Map ExtIdent InfernoType]
-> (Map ExtIdent InfernoType, [Constraint])
mergeImplicitMaps (forall (f :: * -> *).
BlockUtils f =>
f SourcePos -> Location SourcePos
blockPosition Expr (Pinned VCObjectHash) SourcePos
expr) [Map ExtIdent InfernoType
i1, Map ExtIdent InfernoType
i2]
          forall (m :: * -> *) a. Monad m => a -> m a
return
            ( forall hash pos.
pos
-> pos
-> ImplExpl
-> pos
-> Expr hash pos
-> pos
-> Expr hash pos
-> Expr hash pos
Let SourcePos
p1 SourcePos
loc (ExtIdent -> ImplExpl
Expl ExtIdent
x) SourcePos
p2 Expr (Pinned VCObjectHash) SourcePos
e1' SourcePos
p3 Expr (Pinned VCObjectHash) SourcePos
e2',
              Map ExtIdent InfernoType -> InfernoType -> ImplType
ImplType Map ExtIdent InfernoType
isMerged InfernoType
t2,
              forall a. Ord a => [a] -> Set a
Set.fromList [Constraint]
ics forall a. Ord a => Set a -> Set a -> Set a
`Set.union` Set Constraint
c1 forall a. Ord a => Set a -> Set a -> Set a
`Set.union` Set Constraint
c2
            )
        Let SourcePos
p1 SourcePos
loc (Impl ExtIdent
x) SourcePos
p2 Expr (Pinned VCObjectHash) SourcePos
e1 SourcePos
p3 Expr (Pinned VCObjectHash) SourcePos
e2 -> do
          (Expr (Pinned VCObjectHash) SourcePos
e1', ImplType Map ExtIdent InfernoType
i1 InfernoType
t1, Set Constraint
c1) <- Expr (Pinned VCObjectHash) SourcePos
-> Infer
     (Expr (Pinned VCObjectHash) SourcePos, ImplType, Set Constraint)
infer Expr (Pinned VCObjectHash) SourcePos
e1
          (Expr (Pinned VCObjectHash) SourcePos
e2', ImplType Map ExtIdent InfernoType
i2 InfernoType
t2, Set Constraint
c2) <- Expr (Pinned VCObjectHash) SourcePos
-> Infer
     (Expr (Pinned VCObjectHash) SourcePos, ImplType, Set Constraint)
infer Expr (Pinned VCObjectHash) SourcePos
e2

          InfernoType
v1 <- case forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup ExtIdent
x Map ExtIdent InfernoType
i2 of
            Just InfernoType
t -> forall (m :: * -> *) a. Monad m => a -> m a
return InfernoType
t
            Maybe InfernoType
Nothing -> Infer InfernoType
fresh

          let (Map ExtIdent InfernoType
isMerged, [Constraint]
ics) = Location SourcePos
-> [Map ExtIdent InfernoType]
-> (Map ExtIdent InfernoType, [Constraint])
mergeImplicitMaps (forall (f :: * -> *).
BlockUtils f =>
f SourcePos -> Location SourcePos
blockPosition Expr (Pinned VCObjectHash) SourcePos
expr) [Map ExtIdent InfernoType
i1, forall k a. Ord k => Map k a -> Set k -> Map k a
Map.withoutKeys Map ExtIdent InfernoType
i2 (forall a. a -> Set a
Set.singleton ExtIdent
x)]
              tyCls :: Set TypeClass
tyCls = forall a. Ord a => [a] -> Set a
Set.fromList forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> b
snd forall a b. (a -> b) -> a -> b
$ forall a b. [Either a b] -> [b]
rights forall a b. (a -> b) -> a -> b
$ forall a. Set a -> [a]
Set.toList forall a b. (a -> b) -> a -> b
$ Set Constraint
c1 forall a. Ord a => Set a -> Set a -> Set a
`Set.union` Set Constraint
c2

          forall (m :: * -> *) a. Monad m => a -> m a
return
            ( forall hash pos.
pos
-> pos
-> ImplExpl
-> pos
-> Expr hash pos
-> pos
-> Expr hash pos
-> Expr hash pos
Let SourcePos
p1 SourcePos
loc (ExtIdent -> ImplExpl
Impl ExtIdent
x) SourcePos
p2 Expr (Pinned VCObjectHash) SourcePos
e1' SourcePos
p3 Expr (Pinned VCObjectHash) SourcePos
e2',
              Map ExtIdent InfernoType -> InfernoType -> ImplType
ImplType Map ExtIdent InfernoType
isMerged InfernoType
t2,
              forall a. Ord a => [a] -> Set a
Set.fromList [Constraint]
ics
                forall a. Ord a => Set a -> Set a -> Set a
`Set.union` Set Constraint
c1
                forall a. Ord a => Set a -> Set a -> Set a
`Set.union` Set Constraint
c2
                forall a. Ord a => Set a -> Set a -> Set a
`Set.union` forall a. a -> Set a
Set.singleton (forall a b c d. a -> b -> c -> Either (a, b, c) d
tyConstr InfernoType
v1 InfernoType
t1 [forall a.
Set TypeClass
-> ExtIdent
-> InfernoType
-> InfernoType
-> Location a
-> TypeError a
ImplicitVarTypeOverlap Set TypeClass
tyCls ExtIdent
x InfernoType
v1 InfernoType
t1 forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *).
BlockUtils f =>
f SourcePos -> Location SourcePos
blockPosition Expr (Pinned VCObjectHash) SourcePos
expr])
            )
        Op Expr (Pinned VCObjectHash) SourcePos
e1 SourcePos
loc Pinned VCObjectHash
mHash (Int, InfixFixity)
opMeta Scoped ModuleName
modNm Ident
op Expr (Pinned VCObjectHash) SourcePos
e2 -> do
          let (SourcePos
sPos, SourcePos
ePos) = forall a. ElementPosition a => SourcePos -> a -> Location SourcePos
elementPosition SourcePos
loc Ident
op
          let opLoc :: Location SourcePos
opLoc = (SourcePos
sPos, SourcePos -> Int -> SourcePos
incSourceCol SourcePos
ePos forall a b. (a -> b) -> a -> b
$ forall a. a -> Scoped a -> a
fromScoped Int
0 forall a b. (a -> b) -> a -> b
$ (forall a. Num a => a -> a -> a
+ Int
1) forall b c a. (b -> c) -> (a -> b) -> a -> c
. Text -> Int
Text.length forall b c a. (b -> c) -> (a -> b) -> a -> c
. ModuleName -> Text
unModuleName forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Scoped ModuleName
modNm)

          (Expr (Pinned VCObjectHash) SourcePos
e1', ImplType Map ExtIdent InfernoType
i1 InfernoType
t1, Set Constraint
c1) <- Expr (Pinned VCObjectHash) SourcePos
-> Infer
     (Expr (Pinned VCObjectHash) SourcePos, ImplType, Set Constraint)
infer Expr (Pinned VCObjectHash) SourcePos
e1
          (Expr (Pinned VCObjectHash) SourcePos
e2', ImplType Map ExtIdent InfernoType
i2 InfernoType
t2, Set Constraint
c2) <- Expr (Pinned VCObjectHash) SourcePos
-> Infer
     (Expr (Pinned VCObjectHash) SourcePos, ImplType, Set Constraint)
infer Expr (Pinned VCObjectHash) SourcePos
e2

          TypeMetadata (Set TypeClass, ImplType)
meta <- Location SourcePos
-> Either VCObjectHash ExtIdent
-> Infer (TypeMetadata (Set TypeClass, ImplType))
lookupEnv Location SourcePos
opLoc (forall b a. b -> (a -> b) -> Maybe a -> b
maybe (forall a. HasCallStack => [Char] -> a
error [Char]
"internal error, infix ops must always be pinned!!") forall a b. a -> Either a b
Left forall a b. (a -> b) -> a -> b
$ Pinned VCObjectHash -> Maybe VCObjectHash
pinnedToMaybe Pinned VCObjectHash
mHash)
          let (Set TypeClass
tcs, (InfernoType
u1, InfernoType
u2, InfernoType
u3)) = ImplType -> (InfernoType, InfernoType, InfernoType)
opGetTyComponents forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall ty. TypeMetadata ty -> ty
ty TypeMetadata (Set TypeClass, ImplType)
meta

          InfernoType
tv <- Infer InfernoType
fresh
          let (Map ExtIdent InfernoType
isMerged, [Constraint]
ics) = Location SourcePos
-> [Map ExtIdent InfernoType]
-> (Map ExtIdent InfernoType, [Constraint])
mergeImplicitMaps (forall (f :: * -> *).
BlockUtils f =>
f SourcePos -> Location SourcePos
blockPosition Expr (Pinned VCObjectHash) SourcePos
expr) [Map ExtIdent InfernoType
i1, Map ExtIdent InfernoType
i2]
              tyCls :: Set TypeClass
tyCls = forall a. Ord a => [a] -> Set a
Set.fromList forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> b
snd forall a b. (a -> b) -> a -> b
$ forall a b. [Either a b] -> [b]
rights forall a b. (a -> b) -> a -> b
$ forall a. Set a -> [a]
Set.toList forall a b. (a -> b) -> a -> b
$ Set Constraint
c1 forall a. Ord a => Set a -> Set a -> Set a
`Set.union` Set Constraint
c2

          Location SourcePos
-> TypeMetadata (Set TypeClass, ImplType) -> Infer ()
attachTypeToPosition Location SourcePos
opLoc TypeMetadata (Set TypeClass, ImplType)
meta {ty :: (Set TypeClass, ImplType)
ty = (Set TypeClass
tcs, Map ExtIdent InfernoType -> InfernoType -> ImplType
ImplType forall k a. Map k a
Map.empty forall a b. (a -> b) -> a -> b
$ InfernoType
t1 InfernoType -> InfernoType -> InfernoType
`TArr` (InfernoType
t2 InfernoType -> InfernoType -> InfernoType
`TArr` InfernoType
tv))}

          forall (m :: * -> *) a. Monad m => a -> m a
return
            ( forall hash pos.
Expr hash pos
-> pos
-> hash
-> (Int, InfixFixity)
-> Scoped ModuleName
-> Ident
-> Expr hash pos
-> Expr hash pos
Op Expr (Pinned VCObjectHash) SourcePos
e1' SourcePos
loc Pinned VCObjectHash
mHash (Int, InfixFixity)
opMeta Scoped ModuleName
modNm Ident
op Expr (Pinned VCObjectHash) SourcePos
e2',
              Map ExtIdent InfernoType -> InfernoType -> ImplType
ImplType Map ExtIdent InfernoType
isMerged InfernoType
tv,
              forall a. Ord a => [a] -> Set a
Set.fromList [Constraint]
ics
                forall a. Ord a => Set a -> Set a -> Set a
`Set.union` Set Constraint
c1
                forall a. Ord a => Set a -> Set a -> Set a
`Set.union` Set Constraint
c2
                forall a. Ord a => Set a -> Set a -> Set a
`Set.union` forall a. Ord a => [a] -> Set a
Set.fromList
                  [ forall a b c d. a -> b -> c -> Either (a, b, c) d
tyConstr InfernoType
u1 InfernoType
t1 [forall a.
Set TypeClass
-> InfernoType -> InfernoType -> Location a -> TypeError a
UnificationFail Set TypeClass
tyCls InfernoType
u1 InfernoType
t1 forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *).
BlockUtils f =>
f SourcePos -> Location SourcePos
blockPosition Expr (Pinned VCObjectHash) SourcePos
e1],
                    forall a b c d. a -> b -> c -> Either (a, b, c) d
tyConstr InfernoType
u2 InfernoType
t2 [forall a.
Set TypeClass
-> InfernoType -> InfernoType -> Location a -> TypeError a
UnificationFail Set TypeClass
tyCls InfernoType
u2 InfernoType
t2 forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *).
BlockUtils f =>
f SourcePos -> Location SourcePos
blockPosition Expr (Pinned VCObjectHash) SourcePos
e2],
                    forall a b c d. a -> b -> c -> Either (a, b, c) d
tyConstr InfernoType
u3 InfernoType
tv [forall a.
Set TypeClass
-> InfernoType -> InfernoType -> Location a -> TypeError a
UnificationFail Set TypeClass
tyCls InfernoType
u3 InfernoType
tv forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *).
BlockUtils f =>
f SourcePos -> Location SourcePos
blockPosition Expr (Pinned VCObjectHash) SourcePos
expr]
                  ]
                forall a. Ord a => Set a -> Set a -> Set a
`Set.union` (forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map (forall a b. b -> Either a b
Right forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Location SourcePos
opLoc,)) Set TypeClass
tcs)
            )
        PreOp SourcePos
loc Pinned VCObjectHash
mHash Int
opMeta Scoped ModuleName
modNm Ident
op Expr (Pinned VCObjectHash) SourcePos
e -> do
          let (SourcePos
sPos, SourcePos
ePos) = forall a. ElementPosition a => SourcePos -> a -> Location SourcePos
elementPosition SourcePos
loc Ident
op
          let opLoc :: Location SourcePos
opLoc = (SourcePos
sPos, SourcePos -> Int -> SourcePos
incSourceCol SourcePos
ePos forall a b. (a -> b) -> a -> b
$ forall a. a -> Scoped a -> a
fromScoped Int
0 forall a b. (a -> b) -> a -> b
$ (forall a. Num a => a -> a -> a
+ Int
1) forall b c a. (b -> c) -> (a -> b) -> a -> c
. Text -> Int
Text.length forall b c a. (b -> c) -> (a -> b) -> a -> c
. ModuleName -> Text
unModuleName forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Scoped ModuleName
modNm)

          (Expr (Pinned VCObjectHash) SourcePos
e', ImplType Map ExtIdent InfernoType
i InfernoType
t, Set Constraint
c) <- Expr (Pinned VCObjectHash) SourcePos
-> Infer
     (Expr (Pinned VCObjectHash) SourcePos, ImplType, Set Constraint)
infer Expr (Pinned VCObjectHash) SourcePos
e

          TypeMetadata (Set TypeClass, ImplType)
meta <- Location SourcePos
-> Either VCObjectHash ExtIdent
-> Infer (TypeMetadata (Set TypeClass, ImplType))
lookupEnv Location SourcePos
opLoc (forall b a. b -> (a -> b) -> Maybe a -> b
maybe (forall a. HasCallStack => [Char] -> a
error [Char]
"internal error, prefix ops must always be pinned!!") forall a b. a -> Either a b
Left forall a b. (a -> b) -> a -> b
$ Pinned VCObjectHash -> Maybe VCObjectHash
pinnedToMaybe Pinned VCObjectHash
mHash)
          let (Set TypeClass
tcs, (InfernoType
u1, InfernoType
u2)) = ImplType -> (InfernoType, InfernoType)
preOpGetTyComponents forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall ty. TypeMetadata ty -> ty
ty TypeMetadata (Set TypeClass, ImplType)
meta
              tyCls :: Set TypeClass
tyCls = forall a. Ord a => [a] -> Set a
Set.fromList forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> b
snd forall a b. (a -> b) -> a -> b
$ forall a b. [Either a b] -> [b]
rights forall a b. (a -> b) -> a -> b
$ forall a. Set a -> [a]
Set.toList forall a b. (a -> b) -> a -> b
$ Set Constraint
c

          InfernoType
tv <- Infer InfernoType
fresh
          Location SourcePos
-> TypeMetadata (Set TypeClass, ImplType) -> Infer ()
attachTypeToPosition Location SourcePos
opLoc TypeMetadata (Set TypeClass, ImplType)
meta {ty :: (Set TypeClass, ImplType)
ty = (Set TypeClass
tcs, Map ExtIdent InfernoType -> InfernoType -> ImplType
ImplType forall k a. Map k a
Map.empty forall a b. (a -> b) -> a -> b
$ InfernoType
t InfernoType -> InfernoType -> InfernoType
`TArr` InfernoType
tv)}

          forall (m :: * -> *) a. Monad m => a -> m a
return
            ( forall hash pos.
pos
-> hash
-> Int
-> Scoped ModuleName
-> Ident
-> Expr hash pos
-> Expr hash pos
PreOp SourcePos
loc Pinned VCObjectHash
mHash Int
opMeta Scoped ModuleName
modNm Ident
op Expr (Pinned VCObjectHash) SourcePos
e',
              Map ExtIdent InfernoType -> InfernoType -> ImplType
ImplType Map ExtIdent InfernoType
i InfernoType
tv,
              Set Constraint
c
                forall a. Ord a => Set a -> Set a -> Set a
`Set.union` forall a. Ord a => [a] -> Set a
Set.fromList
                  [ forall a b c d. a -> b -> c -> Either (a, b, c) d
tyConstr InfernoType
u1 InfernoType
t [forall a.
Set TypeClass
-> InfernoType -> InfernoType -> Location a -> TypeError a
UnificationFail Set TypeClass
tyCls InfernoType
u1 InfernoType
t forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *).
BlockUtils f =>
f SourcePos -> Location SourcePos
blockPosition Expr (Pinned VCObjectHash) SourcePos
e],
                    forall a b c d. a -> b -> c -> Either (a, b, c) d
tyConstr InfernoType
u2 InfernoType
tv [forall a.
Set TypeClass
-> InfernoType -> InfernoType -> Location a -> TypeError a
UnificationFail Set TypeClass
tyCls InfernoType
u2 InfernoType
tv forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *).
BlockUtils f =>
f SourcePos -> Location SourcePos
blockPosition Expr (Pinned VCObjectHash) SourcePos
expr]
                  ]
                forall a. Ord a => Set a -> Set a -> Set a
`Set.union` (forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map (forall a b. b -> Either a b
Right forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Location SourcePos
opLoc,)) Set TypeClass
tcs)
            )
        If SourcePos
p1 Expr (Pinned VCObjectHash) SourcePos
cond SourcePos
p2 Expr (Pinned VCObjectHash) SourcePos
tr SourcePos
p3 Expr (Pinned VCObjectHash) SourcePos
fl -> do
          (Expr (Pinned VCObjectHash) SourcePos
cond', ImplType Map ExtIdent InfernoType
i1 InfernoType
t1, Set Constraint
c1) <- Expr (Pinned VCObjectHash) SourcePos
-> Infer
     (Expr (Pinned VCObjectHash) SourcePos, ImplType, Set Constraint)
infer Expr (Pinned VCObjectHash) SourcePos
cond
          (Expr (Pinned VCObjectHash) SourcePos
tr', ImplType Map ExtIdent InfernoType
i2 InfernoType
t2, Set Constraint
c2) <- Expr (Pinned VCObjectHash) SourcePos
-> Infer
     (Expr (Pinned VCObjectHash) SourcePos, ImplType, Set Constraint)
infer Expr (Pinned VCObjectHash) SourcePos
tr
          (Expr (Pinned VCObjectHash) SourcePos
fl', ImplType Map ExtIdent InfernoType
i3 InfernoType
t3, Set Constraint
c3) <- Expr (Pinned VCObjectHash) SourcePos
-> Infer
     (Expr (Pinned VCObjectHash) SourcePos, ImplType, Set Constraint)
infer Expr (Pinned VCObjectHash) SourcePos
fl

          let (Map ExtIdent InfernoType
isMerged, [Constraint]
ics) = Location SourcePos
-> [Map ExtIdent InfernoType]
-> (Map ExtIdent InfernoType, [Constraint])
mergeImplicitMaps (forall (f :: * -> *).
BlockUtils f =>
f SourcePos -> Location SourcePos
blockPosition Expr (Pinned VCObjectHash) SourcePos
expr) [Map ExtIdent InfernoType
i1, Map ExtIdent InfernoType
i2, Map ExtIdent InfernoType
i3]
              tyCls :: Set TypeClass
tyCls = forall a. Ord a => [a] -> Set a
Set.fromList forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> b
snd forall a b. (a -> b) -> a -> b
$ forall a b. [Either a b] -> [b]
rights forall a b. (a -> b) -> a -> b
$ forall a. Set a -> [a]
Set.toList forall a b. (a -> b) -> a -> b
$ Set Constraint
c1 forall a. Ord a => Set a -> Set a -> Set a
`Set.union` Set Constraint
c2 forall a. Ord a => Set a -> Set a -> Set a
`Set.union` Set Constraint
c3

          forall (m :: * -> *) a. Monad m => a -> m a
return
            ( forall hash pos.
pos
-> Expr hash pos
-> pos
-> Expr hash pos
-> pos
-> Expr hash pos
-> Expr hash pos
If SourcePos
p1 Expr (Pinned VCObjectHash) SourcePos
cond' SourcePos
p2 Expr (Pinned VCObjectHash) SourcePos
tr' SourcePos
p3 Expr (Pinned VCObjectHash) SourcePos
fl',
              Map ExtIdent InfernoType -> InfernoType -> ImplType
ImplType Map ExtIdent InfernoType
isMerged InfernoType
t2,
              forall a. Ord a => [a] -> Set a
Set.fromList [Constraint]
ics
                forall a. Ord a => Set a -> Set a -> Set a
`Set.union` Set Constraint
c1
                forall a. Ord a => Set a -> Set a -> Set a
`Set.union` Set Constraint
c2
                forall a. Ord a => Set a -> Set a -> Set a
`Set.union` Set Constraint
c3
                forall a. Ord a => Set a -> Set a -> Set a
`Set.union` forall a. Ord a => [a] -> Set a
Set.fromList
                  [ forall a b c d. a -> b -> c -> Either (a, b, c) d
tyConstr InfernoType
t1 InfernoType
typeBool [forall a. Set TypeClass -> InfernoType -> Location a -> TypeError a
IfConditionMustBeBool Set TypeClass
tyCls InfernoType
t1 forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *).
BlockUtils f =>
f SourcePos -> Location SourcePos
blockPosition Expr (Pinned VCObjectHash) SourcePos
cond],
                    forall a b c d. a -> b -> c -> Either (a, b, c) d
tyConstr InfernoType
t2 InfernoType
t3 [forall a.
Set TypeClass
-> InfernoType
-> InfernoType
-> Location a
-> Location a
-> TypeError a
IfBranchesMustBeEqType Set TypeClass
tyCls InfernoType
t2 InfernoType
t3 (forall (f :: * -> *).
BlockUtils f =>
f SourcePos -> Location SourcePos
blockPosition Expr (Pinned VCObjectHash) SourcePos
tr) (forall (f :: * -> *).
BlockUtils f =>
f SourcePos -> Location SourcePos
blockPosition Expr (Pinned VCObjectHash) SourcePos
fl)]
                  ]
            )
        Tuple SourcePos
p1 TList (Expr (Pinned VCObjectHash) SourcePos, Maybe SourcePos)
es SourcePos
p2 -> do
          ([(Expr (Pinned VCObjectHash) SourcePos, Maybe SourcePos)]
es', [Map ExtIdent InfernoType]
impls, [InfernoType]
tys, Set Constraint
cs) <- forall {b}.
[(Expr (Pinned VCObjectHash) SourcePos, b)]
-> ReaderT
     Env
     (StateT InferState (ExceptT [TypeError SourcePos] Identity))
     ([(Expr (Pinned VCObjectHash) SourcePos, b)],
      [Map ExtIdent InfernoType], [InfernoType], Set Constraint)
go forall a b. (a -> b) -> a -> b
$ forall a. TList a -> [a]
tListToList TList (Expr (Pinned VCObjectHash) SourcePos, Maybe SourcePos)
es
          let (Map ExtIdent InfernoType
isMerged, [Constraint]
ics) = Location SourcePos
-> [Map ExtIdent InfernoType]
-> (Map ExtIdent InfernoType, [Constraint])
mergeImplicitMaps (forall (f :: * -> *).
BlockUtils f =>
f SourcePos -> Location SourcePos
blockPosition Expr (Pinned VCObjectHash) SourcePos
expr) [Map ExtIdent InfernoType]
impls
          let inferredTy :: ImplType
inferredTy = Map ExtIdent InfernoType -> InfernoType -> ImplType
ImplType Map ExtIdent InfernoType
isMerged forall a b. (a -> b) -> a -> b
$ TList InfernoType -> InfernoType
TTuple forall a b. (a -> b) -> a -> b
$ forall a. [a] -> TList a
tListFromList [InfernoType]
tys
          Location SourcePos
-> TypeMetadata (Set TypeClass, ImplType) -> Infer ()
attachTypeToPosition
            Location SourcePos
exprLoc
            TypeMetadata
              { identExpr :: Expr () ()
identExpr = forall (p :: * -> * -> *) a b c d.
Bifunctor p =>
(a -> b) -> (c -> d) -> p a c -> p b d
bimap (forall a b. a -> b -> a
const ()) (forall a b. a -> b -> a
const ()) forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) pos. BlockUtils f => f pos -> f pos
removeComments Expr (Pinned VCObjectHash) SourcePos
expr,
                ty :: (Set TypeClass, ImplType)
ty = (forall a. Set a
Set.empty, ImplType
inferredTy),
                docs :: Maybe Text
docs = forall a. Maybe a
Nothing
              }

          forall (m :: * -> *) a. Monad m => a -> m a
return
            ( forall hash pos.
pos -> TList (Expr hash pos, Maybe pos) -> pos -> Expr hash pos
Tuple SourcePos
p1 (forall a. [a] -> TList a
tListFromList [(Expr (Pinned VCObjectHash) SourcePos, Maybe SourcePos)]
es') SourcePos
p2,
              ImplType
inferredTy,
              forall a. Ord a => [a] -> Set a
Set.fromList [Constraint]
ics forall a. Ord a => Set a -> Set a -> Set a
`Set.union` Set Constraint
cs
            )
          where
            go :: [(Expr (Pinned VCObjectHash) SourcePos, b)]
-> ReaderT
     Env
     (StateT InferState (ExceptT [TypeError SourcePos] Identity))
     ([(Expr (Pinned VCObjectHash) SourcePos, b)],
      [Map ExtIdent InfernoType], [InfernoType], Set Constraint)
go [] = forall (m :: * -> *) a. Monad m => a -> m a
return ([], [], [], forall a. Set a
Set.empty)
            go ((Expr (Pinned VCObjectHash) SourcePos
e', b
p3) : [(Expr (Pinned VCObjectHash) SourcePos, b)]
es') = do
              (Expr (Pinned VCObjectHash) SourcePos
e'', ImplType Map ExtIdent InfernoType
i InfernoType
t, Set Constraint
cs) <- Expr (Pinned VCObjectHash) SourcePos
-> Infer
     (Expr (Pinned VCObjectHash) SourcePos, ImplType, Set Constraint)
infer Expr (Pinned VCObjectHash) SourcePos
e'
              ([(Expr (Pinned VCObjectHash) SourcePos, b)]
es'', [Map ExtIdent InfernoType]
impls, [InfernoType]
tRest, Set Constraint
csRest) <- [(Expr (Pinned VCObjectHash) SourcePos, b)]
-> ReaderT
     Env
     (StateT InferState (ExceptT [TypeError SourcePos] Identity))
     ([(Expr (Pinned VCObjectHash) SourcePos, b)],
      [Map ExtIdent InfernoType], [InfernoType], Set Constraint)
go [(Expr (Pinned VCObjectHash) SourcePos, b)]
es'
              forall (m :: * -> *) a. Monad m => a -> m a
return ((Expr (Pinned VCObjectHash) SourcePos
e'', b
p3) forall a. a -> [a] -> [a]
: [(Expr (Pinned VCObjectHash) SourcePos, b)]
es'', Map ExtIdent InfernoType
i forall a. a -> [a] -> [a]
: [Map ExtIdent InfernoType]
impls, InfernoType
t forall a. a -> [a] -> [a]
: [InfernoType]
tRest, Set Constraint
cs forall a. Ord a => Set a -> Set a -> Set a
`Set.union` Set Constraint
csRest)
        Assert SourcePos
p1 Expr (Pinned VCObjectHash) SourcePos
cond SourcePos
p2 Expr (Pinned VCObjectHash) SourcePos
e -> do
          (Expr (Pinned VCObjectHash) SourcePos
cond', ImplType Map ExtIdent InfernoType
i1 InfernoType
t1, Set Constraint
c1) <- Expr (Pinned VCObjectHash) SourcePos
-> Infer
     (Expr (Pinned VCObjectHash) SourcePos, ImplType, Set Constraint)
infer Expr (Pinned VCObjectHash) SourcePos
cond
          (Expr (Pinned VCObjectHash) SourcePos
e', ImplType Map ExtIdent InfernoType
i2 InfernoType
t2, Set Constraint
c2) <- Expr (Pinned VCObjectHash) SourcePos
-> Infer
     (Expr (Pinned VCObjectHash) SourcePos, ImplType, Set Constraint)
infer Expr (Pinned VCObjectHash) SourcePos
e

          let (Map ExtIdent InfernoType
isMerged, [Constraint]
ics) = Location SourcePos
-> [Map ExtIdent InfernoType]
-> (Map ExtIdent InfernoType, [Constraint])
mergeImplicitMaps (forall (f :: * -> *).
BlockUtils f =>
f SourcePos -> Location SourcePos
blockPosition Expr (Pinned VCObjectHash) SourcePos
expr) [Map ExtIdent InfernoType
i1, Map ExtIdent InfernoType
i2]
          forall (m :: * -> *) a. Monad m => a -> m a
return
            ( forall hash pos.
pos -> Expr hash pos -> pos -> Expr hash pos -> Expr hash pos
Assert SourcePos
p1 Expr (Pinned VCObjectHash) SourcePos
cond' SourcePos
p2 Expr (Pinned VCObjectHash) SourcePos
e',
              Map ExtIdent InfernoType -> InfernoType -> ImplType
ImplType Map ExtIdent InfernoType
isMerged InfernoType
t2,
              forall a. Ord a => [a] -> Set a
Set.fromList [Constraint]
ics
                forall a. Ord a => Set a -> Set a -> Set a
`Set.union` Set Constraint
c1
                forall a. Ord a => Set a -> Set a -> Set a
`Set.union` Set Constraint
c2
                forall a. Ord a => Set a -> Set a -> Set a
`Set.union` forall a. a -> Set a
Set.singleton (forall a b c d. a -> b -> c -> Either (a, b, c) d
tyConstr InfernoType
t1 InfernoType
typeBool [forall a. Set TypeClass -> InfernoType -> Location a -> TypeError a
AssertConditionMustBeBool (forall a. Ord a => [a] -> Set a
Set.fromList forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> b
snd forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. [Either a b] -> [b]
rights forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Set a -> [a]
Set.toList forall a b. (a -> b) -> a -> b
$ Set Constraint
c1 forall a. Ord a => Set a -> Set a -> Set a
`Set.union` Set Constraint
c2) InfernoType
t1 forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *).
BlockUtils f =>
f SourcePos -> Location SourcePos
blockPosition Expr (Pinned VCObjectHash) SourcePos
cond])
            )
        Empty SourcePos
_ -> do
          TypeMetadata (Set TypeClass, ImplType)
meta <- Location SourcePos
-> Either VCObjectHash ExtIdent
-> Infer (TypeMetadata (Set TypeClass, ImplType))
lookupEnv Location SourcePos
exprLoc forall a b. (a -> b) -> a -> b
$ forall a b. a -> Either a b
Left VCObjectHash
emptyHash
          let (Set TypeClass
_, ImplType
t) = forall ty. TypeMetadata ty -> ty
ty TypeMetadata (Set TypeClass, ImplType)
meta
          Location SourcePos
-> TypeMetadata (Set TypeClass, ImplType) -> Infer ()
attachTypeToPosition Location SourcePos
exprLoc TypeMetadata (Set TypeClass, ImplType)
meta
          forall (m :: * -> *) a. Monad m => a -> m a
return (Expr (Pinned VCObjectHash) SourcePos
expr, ImplType
t, forall a. Set a
Set.empty)
        One SourcePos
p Expr (Pinned VCObjectHash) SourcePos
e -> do
          (Expr (Pinned VCObjectHash) SourcePos
e', ImplType Map ExtIdent InfernoType
is InfernoType
ty, Set Constraint
cs) <- Expr (Pinned VCObjectHash) SourcePos
-> Infer
     (Expr (Pinned VCObjectHash) SourcePos, ImplType, Set Constraint)
infer Expr (Pinned VCObjectHash) SourcePos
e
          TypeMetadata (Set TypeClass, ImplType)
meta <- Location SourcePos
-> Either VCObjectHash ExtIdent
-> Infer (TypeMetadata (Set TypeClass, ImplType))
lookupEnv Location SourcePos
exprLoc forall a b. (a -> b) -> a -> b
$ forall a b. a -> Either a b
Left VCObjectHash
oneHash
          Location SourcePos
-> TypeMetadata (Set TypeClass, ImplType) -> Infer ()
attachTypeToPosition Location SourcePos
exprLoc TypeMetadata (Set TypeClass, ImplType)
meta {ty :: (Set TypeClass, ImplType)
ty = (forall a. Set a
Set.empty, Map ExtIdent InfernoType -> InfernoType -> ImplType
ImplType Map ExtIdent InfernoType
is forall a b. (a -> b) -> a -> b
$ InfernoType -> InfernoType
TOptional InfernoType
ty)}
          forall (m :: * -> *) a. Monad m => a -> m a
return (forall hash pos. pos -> Expr hash pos -> Expr hash pos
One SourcePos
p Expr (Pinned VCObjectHash) SourcePos
e', Map ExtIdent InfernoType -> InfernoType -> ImplType
ImplType Map ExtIdent InfernoType
is forall a b. (a -> b) -> a -> b
$ InfernoType -> InfernoType
TOptional InfernoType
ty, Set Constraint
cs)
        Case SourcePos
p1 Expr (Pinned VCObjectHash) SourcePos
e SourcePos
p2 NonEmpty
  (SourcePos, Pat (Pinned VCObjectHash) SourcePos, SourcePos,
   Expr (Pinned VCObjectHash) SourcePos)
patExprs' SourcePos
p3 -> do
          let patExprs :: [(SourcePos, Pat (Pinned VCObjectHash) SourcePos, SourcePos,
  Expr (Pinned VCObjectHash) SourcePos)]
patExprs = forall a. NonEmpty a -> [a]
NEList.toList NonEmpty
  (SourcePos, Pat (Pinned VCObjectHash) SourcePos, SourcePos,
   Expr (Pinned VCObjectHash) SourcePos)
patExprs'
          (Expr (Pinned VCObjectHash) SourcePos
e', ImplType Map ExtIdent InfernoType
i_e InfernoType
t_e, Set Constraint
cs_e) <- Expr (Pinned VCObjectHash) SourcePos
-> Infer
     (Expr (Pinned VCObjectHash) SourcePos, ImplType, Set Constraint)
infer Expr (Pinned VCObjectHash) SourcePos
e
          ([InfernoType]
patTys, [[(Ident, TypeMetadata TCScheme)]]
patVars) <-
            forall a b. [(a, b)] -> ([a], [b])
unzip
              forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM
                (\Pat (Pinned VCObjectHash) SourcePos
p -> Map Ident (Location SourcePos)
-> Pat (Pinned VCObjectHash) SourcePos
-> Infer (Map Ident (Location SourcePos))
checkVariableOverlap forall k a. Map k a
Map.empty Pat (Pinned VCObjectHash) SourcePos
p forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Pat (Pinned VCObjectHash) SourcePos
-> ReaderT
     Env
     (StateT InferState (ExceptT [TypeError SourcePos] Identity))
     (InfernoType, [(Ident, TypeMetadata TCScheme)])
mkPatConstraint Pat (Pinned VCObjectHash) SourcePos
p)
                (forall a b. (a -> b) -> [a] -> [b]
map (\(SourcePos
_, Pat (Pinned VCObjectHash) SourcePos
p, SourcePos
_, Expr (Pinned VCObjectHash) SourcePos
_) -> Pat (Pinned VCObjectHash) SourcePos
p) [(SourcePos, Pat (Pinned VCObjectHash) SourcePos, SourcePos,
  Expr (Pinned VCObjectHash) SourcePos)]
patExprs)

          Location SourcePos
-> [Pat (Pinned VCObjectHash) SourcePos] -> Infer ()
addCasePatterns Location SourcePos
exprLoc forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map (\(SourcePos
_, Pat (Pinned VCObjectHash) SourcePos
p, SourcePos
_, Expr (Pinned VCObjectHash) SourcePos
_) -> Pat (Pinned VCObjectHash) SourcePos
p) [(SourcePos, Pat (Pinned VCObjectHash) SourcePos, SourcePos,
  Expr (Pinned VCObjectHash) SourcePos)]
patExprs

          [(Expr (Pinned VCObjectHash) SourcePos, ImplType, Set Constraint)]
res <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM (forall a b. [a] -> [b] -> [(a, b)]
zip [[(Ident, TypeMetadata TCScheme)]]
patVars forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map (\(SourcePos
_, Pat (Pinned VCObjectHash) SourcePos
_p, SourcePos
_, Expr (Pinned VCObjectHash) SourcePos
e'') -> Expr (Pinned VCObjectHash) SourcePos
e'') [(SourcePos, Pat (Pinned VCObjectHash) SourcePos, SourcePos,
  Expr (Pinned VCObjectHash) SourcePos)]
patExprs) forall a b. (a -> b) -> a -> b
$
            \([(Ident, TypeMetadata TCScheme)]
vars, Expr (Pinned VCObjectHash) SourcePos
e''') -> forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr forall a. (ExtIdent, TypeMetadata TCScheme) -> Infer a -> Infer a
inEnv (Expr (Pinned VCObjectHash) SourcePos
-> Infer
     (Expr (Pinned VCObjectHash) SourcePos, ImplType, Set Constraint)
infer Expr (Pinned VCObjectHash) SourcePos
e''') forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map (\(Ident Text
x, TypeMetadata TCScheme
meta) -> (Either Int Text -> ExtIdent
ExtIdent forall a b. (a -> b) -> a -> b
$ forall a b. b -> Either a b
Right Text
x, TypeMetadata TCScheme
meta)) [(Ident, TypeMetadata TCScheme)]
vars

          let ([Expr (Pinned VCObjectHash) SourcePos]
es'', [Map ExtIdent InfernoType]
is_res, [InfernoType]
ts_res, [Set Constraint]
cs_res) = forall a b c d. [(a, b, c, d)] -> ([a], [b], [c], [d])
unzip4 forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map (\(Expr (Pinned VCObjectHash) SourcePos
e'', ImplType Map ExtIdent InfernoType
i_r InfernoType
t_r, Set Constraint
cs_r) -> (Expr (Pinned VCObjectHash) SourcePos
e'', Map ExtIdent InfernoType
i_r, InfernoType
t_r, Set Constraint
cs_r)) [(Expr (Pinned VCObjectHash) SourcePos, ImplType, Set Constraint)]
res
              (Map ExtIdent InfernoType
isMerged, [Constraint]
ics) = Location SourcePos
-> [Map ExtIdent InfernoType]
-> (Map ExtIdent InfernoType, [Constraint])
mergeImplicitMaps (forall (f :: * -> *).
BlockUtils f =>
f SourcePos -> Location SourcePos
blockPosition Expr (Pinned VCObjectHash) SourcePos
expr) (Map ExtIdent InfernoType
i_e forall a. a -> [a] -> [a]
: [Map ExtIdent InfernoType]
is_res)
              tyCls :: Set TypeClass
tyCls = forall a. Ord a => [a] -> Set a
Set.fromList forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> b
snd forall a b. (a -> b) -> a -> b
$ forall a b. [Either a b] -> [b]
rights forall a b. (a -> b) -> a -> b
$ forall a. Set a -> [a]
Set.toList forall a b. (a -> b) -> a -> b
$ Set Constraint
cs_e forall a. Ord a => Set a -> Set a -> Set a
`Set.union` (forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
Set.unions [Set Constraint]
cs_res)
              patTysEqConstraints :: Set Constraint
patTysEqConstraints =
                forall a. Ord a => [a] -> Set a
Set.fromList
                  [ forall a b c d. a -> b -> c -> Either (a, b, c) d
tyConstr InfernoType
tPat4 InfernoType
tPat5 [forall a.
Set TypeClass
-> InfernoType
-> InfernoType
-> Pat (Pinned VCObjectHash) a
-> Pat (Pinned VCObjectHash) a
-> Location a
-> Location a
-> TypeError a
PatternsMustBeEqType Set TypeClass
tyCls InfernoType
tPat4 InfernoType
tPat5 Pat (Pinned VCObjectHash) SourcePos
p4 Pat (Pinned VCObjectHash) SourcePos
p5 (forall (f :: * -> *).
BlockUtils f =>
f SourcePos -> Location SourcePos
blockPosition Pat (Pinned VCObjectHash) SourcePos
p4) (forall (f :: * -> *).
BlockUtils f =>
f SourcePos -> Location SourcePos
blockPosition Pat (Pinned VCObjectHash) SourcePos
p5)]
                    | (InfernoType
tPat4, Pat (Pinned VCObjectHash) SourcePos
p4) <- forall a b. [a] -> [b] -> [(a, b)]
zip [InfernoType]
patTys (forall a b. (a -> b) -> [a] -> [b]
map (\(SourcePos
_, Pat (Pinned VCObjectHash) SourcePos
p, SourcePos
_, Expr (Pinned VCObjectHash) SourcePos
_) -> Pat (Pinned VCObjectHash) SourcePos
p) [(SourcePos, Pat (Pinned VCObjectHash) SourcePos, SourcePos,
  Expr (Pinned VCObjectHash) SourcePos)]
patExprs),
                      (InfernoType
tPat5, Pat (Pinned VCObjectHash) SourcePos
p5) <- forall a b. [a] -> [b] -> [(a, b)]
zip [InfernoType]
patTys (forall a b. (a -> b) -> [a] -> [b]
map (\(SourcePos
_, Pat (Pinned VCObjectHash) SourcePos
p, SourcePos
_, Expr (Pinned VCObjectHash) SourcePos
_) -> Pat (Pinned VCObjectHash) SourcePos
p) [(SourcePos, Pat (Pinned VCObjectHash) SourcePos, SourcePos,
  Expr (Pinned VCObjectHash) SourcePos)]
patExprs),
                      Pat (Pinned VCObjectHash) SourcePos
p4 forall a. Eq a => a -> a -> Bool
/= Pat (Pinned VCObjectHash) SourcePos
p5
                  ]
              patTysMustEqCaseExprTy :: InfernoType
-> Set (Either (InfernoType, InfernoType, [TypeError SourcePos]) d)
patTysMustEqCaseExprTy InfernoType
cExprTy =
                forall a. Ord a => [a] -> Set a
Set.fromList
                  [ forall a b c d. a -> b -> c -> Either (a, b, c) d
tyConstr InfernoType
tPat InfernoType
cExprTy [forall a.
InfernoType
-> InfernoType
-> Pat (Pinned VCObjectHash) a
-> Location a
-> TypeError a
PatternUnificationFail InfernoType
tPat InfernoType
cExprTy Pat (Pinned VCObjectHash) SourcePos
p forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *).
BlockUtils f =>
f SourcePos -> Location SourcePos
blockPosition Pat (Pinned VCObjectHash) SourcePos
p]
                    | (InfernoType
tPat, Pat (Pinned VCObjectHash) SourcePos
p) <- forall a b. [a] -> [b] -> [(a, b)]
zip [InfernoType]
patTys (forall a b. (a -> b) -> [a] -> [b]
map (\(SourcePos
_, Pat (Pinned VCObjectHash) SourcePos
p, SourcePos
_, Expr (Pinned VCObjectHash) SourcePos
_) -> Pat (Pinned VCObjectHash) SourcePos
p) [(SourcePos, Pat (Pinned VCObjectHash) SourcePos, SourcePos,
  Expr (Pinned VCObjectHash) SourcePos)]
patExprs)
                  ]
              patExpTysEqConstraints :: [(ImplType, f SourcePos)]
-> Set (Either (InfernoType, InfernoType, [TypeError SourcePos]) d)
patExpTysEqConstraints [(ImplType, f SourcePos)]
set =
                forall a. Ord a => [a] -> Set a
Set.fromList
                  [ forall a b c d. a -> b -> c -> Either (a, b, c) d
tyConstr InfernoType
t1 InfernoType
t2 [forall a.
Set TypeClass
-> InfernoType
-> InfernoType
-> Location a
-> Location a
-> TypeError a
CaseBranchesMustBeEqType Set TypeClass
tyCls InfernoType
t1 InfernoType
t2 (forall (f :: * -> *).
BlockUtils f =>
f SourcePos -> Location SourcePos
blockPosition f SourcePos
e1) (forall (f :: * -> *).
BlockUtils f =>
f SourcePos -> Location SourcePos
blockPosition f SourcePos
e2)]
                    | (ImplType Map ExtIdent InfernoType
_ InfernoType
t1, f SourcePos
e1) <- [(ImplType, f SourcePos)]
set,
                      (ImplType Map ExtIdent InfernoType
_ InfernoType
t2, f SourcePos
e2) <- [(ImplType, f SourcePos)]
set,
                      f SourcePos
e1 forall a. Eq a => a -> a -> Bool
/= f SourcePos
e2
                  ]

          forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$
            ( forall hash pos.
pos
-> Expr hash pos
-> pos
-> NonEmpty (pos, Pat hash pos, pos, Expr hash pos)
-> pos
-> Expr hash pos
Case SourcePos
p1 Expr (Pinned VCObjectHash) SourcePos
e' SourcePos
p2 (forall a. [a] -> NonEmpty a
NEList.fromList forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map (\(Expr (Pinned VCObjectHash) SourcePos
e'', (SourcePos
p6, Pat (Pinned VCObjectHash) SourcePos
pat, SourcePos
p7, Expr (Pinned VCObjectHash) SourcePos
_)) -> (SourcePos
p6, Pat (Pinned VCObjectHash) SourcePos
pat, SourcePos
p7, Expr (Pinned VCObjectHash) SourcePos
e'')) forall a b. (a -> b) -> a -> b
$ forall a b. [a] -> [b] -> [(a, b)]
zip [Expr (Pinned VCObjectHash) SourcePos]
es'' [(SourcePos, Pat (Pinned VCObjectHash) SourcePos, SourcePos,
  Expr (Pinned VCObjectHash) SourcePos)]
patExprs) SourcePos
p3,
              Map ExtIdent InfernoType -> InfernoType -> ImplType
ImplType Map ExtIdent InfernoType
isMerged forall a b. (a -> b) -> a -> b
$ forall a. [a] -> a
head [InfernoType]
ts_res,
              (forall a. Ord a => [a] -> Set a
Set.fromList [Constraint]
ics)
                forall a. Ord a => Set a -> Set a -> Set a
`Set.union` Set Constraint
cs_e
                forall a. Ord a => Set a -> Set a -> Set a
`Set.union` Set Constraint
patTysEqConstraints
                forall a. Ord a => Set a -> Set a -> Set a
`Set.union` forall {d}.
Ord d =>
InfernoType
-> Set (Either (InfernoType, InfernoType, [TypeError SourcePos]) d)
patTysMustEqCaseExprTy InfernoType
t_e
                forall a. Ord a => Set a -> Set a -> Set a
`Set.union` forall {d} {f :: * -> *}.
(Ord d, BlockUtils f, Eq (f SourcePos)) =>
[(ImplType, f SourcePos)]
-> Set (Either (InfernoType, InfernoType, [TypeError SourcePos]) d)
patExpTysEqConstraints (forall a b. [a] -> [b] -> [(a, b)]
zip (forall a b. (a -> b) -> [a] -> [b]
map (\(Expr (Pinned VCObjectHash) SourcePos
_, ImplType
ty, Set Constraint
_) -> ImplType
ty) [(Expr (Pinned VCObjectHash) SourcePos, ImplType, Set Constraint)]
res) (forall a b. (a -> b) -> [a] -> [b]
map (\(SourcePos
_, Pat (Pinned VCObjectHash) SourcePos
_p, SourcePos
_, Expr (Pinned VCObjectHash) SourcePos
e'') -> Expr (Pinned VCObjectHash) SourcePos
e'') [(SourcePos, Pat (Pinned VCObjectHash) SourcePos, SourcePos,
  Expr (Pinned VCObjectHash) SourcePos)]
patExprs))
                forall a. Ord a => Set a -> Set a -> Set a
`Set.union` (forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
Set.unions [Set Constraint]
cs_res)
            )
          where
            mkPatConstraint :: Pat (Pinned VCObjectHash) SourcePos -> Infer (InfernoType, [(Ident, TypeMetadata TCScheme)])
            mkPatConstraint :: Pat (Pinned VCObjectHash) SourcePos
-> ReaderT
     Env
     (StateT InferState (ExceptT [TypeError SourcePos] Identity))
     (InfernoType, [(Ident, TypeMetadata TCScheme)])
mkPatConstraint Pat (Pinned VCObjectHash) SourcePos
pattern =
              let patLoc :: Location SourcePos
patLoc = forall (f :: * -> *).
BlockUtils f =>
f SourcePos -> Location SourcePos
blockPosition Pat (Pinned VCObjectHash) SourcePos
pattern
               in case Pat (Pinned VCObjectHash) SourcePos
pattern of
                    PVar SourcePos
_ (Just (Ident Text
x)) -> do
                      InfernoType
tv <- Infer InfernoType
fresh
                      Location SourcePos
-> TypeMetadata (Set TypeClass, ImplType) -> Infer ()
attachTypeToPosition
                        Location SourcePos
patLoc
                        TypeMetadata
                          { identExpr :: Expr () ()
identExpr = forall hash pos.
pos -> hash -> Scoped ModuleName -> ImplExpl -> Expr hash pos
Var () () forall a. Scoped a
LocalScope forall a b. (a -> b) -> a -> b
$ ExtIdent -> ImplExpl
Expl forall a b. (a -> b) -> a -> b
$ Either Int Text -> ExtIdent
ExtIdent forall a b. (a -> b) -> a -> b
$ forall a b. b -> Either a b
Right Text
x,
                            ty :: (Set TypeClass, ImplType)
ty = (forall a. Set a
Set.empty, Map ExtIdent InfernoType -> InfernoType -> ImplType
ImplType forall k a. Map k a
Map.empty InfernoType
tv),
                            docs :: Maybe Text
docs = forall a. Maybe a
Nothing
                          }
                      let meta :: TypeMetadata TCScheme
meta =
                            TypeMetadata
                              { identExpr :: Expr () ()
identExpr = forall hash pos.
pos -> hash -> Scoped ModuleName -> ImplExpl -> Expr hash pos
Var () () forall a. Scoped a
LocalScope forall a b. (a -> b) -> a -> b
$ ExtIdent -> ImplExpl
Expl forall a b. (a -> b) -> a -> b
$ Either Int Text -> ExtIdent
ExtIdent forall a b. (a -> b) -> a -> b
$ forall a b. b -> Either a b
Right Text
x,
                                ty :: TCScheme
ty = [TV] -> Set TypeClass -> ImplType -> TCScheme
ForallTC [] forall a. Set a
Set.empty forall a b. (a -> b) -> a -> b
$ Map ExtIdent InfernoType -> InfernoType -> ImplType
ImplType forall k a. Map k a
Map.empty InfernoType
tv,
                                docs :: Maybe Text
docs = forall a. Maybe a
Nothing
                              }
                      forall (m :: * -> *) a. Monad m => a -> m a
return (InfernoType
tv, [(Text -> Ident
Ident Text
x, TypeMetadata TCScheme
meta)])
                    PEnum SourcePos
_ Pinned VCObjectHash
Local Scoped ModuleName
_ Ident
_ -> forall a. HasCallStack => [Char] -> a
error [Char]
"internal error, malformed pattern enum must be pinned"
                    PEnum SourcePos
_ Pinned VCObjectHash
hash Scoped ModuleName
sc Ident
i -> do
                      TypeMetadata (Set TypeClass, ImplType)
meta <- Location SourcePos
-> Either VCObjectHash ExtIdent
-> Infer (TypeMetadata (Set TypeClass, ImplType))
lookupEnv Location SourcePos
patLoc forall a b. (a -> b) -> a -> b
$ forall a b. a -> Either a b
Left forall a b. (a -> b) -> a -> b
$ forall a. HasCallStack => Maybe a -> a
fromJust forall a b. (a -> b) -> a -> b
$ Pinned VCObjectHash -> Maybe VCObjectHash
pinnedToMaybe Pinned VCObjectHash
hash
                      let (Set TypeClass
_, ImplType Map ExtIdent InfernoType
_ InfernoType
t) = forall ty. TypeMetadata ty -> ty
ty TypeMetadata (Set TypeClass, ImplType)
meta
                      Location SourcePos
-> TypeMetadata (Set TypeClass, ImplType) -> Infer ()
attachTypeToPosition Location SourcePos
patLoc TypeMetadata (Set TypeClass, ImplType)
meta {identExpr :: Expr () ()
identExpr = forall hash pos.
pos -> hash -> Scoped ModuleName -> Ident -> Expr hash pos
Enum () () Scoped ModuleName
sc Ident
i}
                      forall (m :: * -> *) a. Monad m => a -> m a
return (InfernoType
t, [])
                    PLit SourcePos
_ Lit
l ->
                      forall b.
Location SourcePos
-> Lit -> InfernoType -> Infer (InfernoType, [b])
inferPatLit
                        Location SourcePos
patLoc
                        Lit
l
                        ( case Lit
l of
                            LInt Int64
_ -> InfernoType
typeInt
                            LDouble Double
_ -> InfernoType
typeDouble
                            LHex Word64
_ -> InfernoType
typeWord64
                            LText Text
_ -> InfernoType
typeText
                        )
                    POne SourcePos
_ Pat (Pinned VCObjectHash) SourcePos
p -> do
                      (InfernoType
t, [(Ident, TypeMetadata TCScheme)]
vars) <- Pat (Pinned VCObjectHash) SourcePos
-> ReaderT
     Env
     (StateT InferState (ExceptT [TypeError SourcePos] Identity))
     (InfernoType, [(Ident, TypeMetadata TCScheme)])
mkPatConstraint Pat (Pinned VCObjectHash) SourcePos
p
                      TypeMetadata (Set TypeClass, ImplType)
meta <- Location SourcePos
-> Either VCObjectHash ExtIdent
-> Infer (TypeMetadata (Set TypeClass, ImplType))
lookupEnv Location SourcePos
patLoc forall a b. (a -> b) -> a -> b
$ forall a b. a -> Either a b
Left VCObjectHash
oneHash
                      Location SourcePos
-> TypeMetadata (Set TypeClass, ImplType) -> Infer ()
attachTypeToPosition Location SourcePos
patLoc TypeMetadata (Set TypeClass, ImplType)
meta {ty :: (Set TypeClass, ImplType)
ty = (forall a. Set a
Set.empty, Map ExtIdent InfernoType -> InfernoType -> ImplType
ImplType forall k a. Map k a
Map.empty forall a b. (a -> b) -> a -> b
$ InfernoType
t InfernoType -> InfernoType -> InfernoType
.-> InfernoType -> InfernoType
TOptional InfernoType
t)}
                      forall (m :: * -> *) a. Monad m => a -> m a
return (InfernoType -> InfernoType
TOptional InfernoType
t, [(Ident, TypeMetadata TCScheme)]
vars)
                    PEmpty SourcePos
_ -> do
                      TypeMetadata (Set TypeClass, ImplType)
meta <- Location SourcePos
-> Either VCObjectHash ExtIdent
-> Infer (TypeMetadata (Set TypeClass, ImplType))
lookupEnv Location SourcePos
patLoc forall a b. (a -> b) -> a -> b
$ forall a b. a -> Either a b
Left VCObjectHash
emptyHash
                      let (Set TypeClass
_, ImplType Map ExtIdent InfernoType
_ InfernoType
t) = forall ty. TypeMetadata ty -> ty
ty TypeMetadata (Set TypeClass, ImplType)
meta
                      Location SourcePos
-> TypeMetadata (Set TypeClass, ImplType) -> Infer ()
attachTypeToPosition Location SourcePos
patLoc TypeMetadata (Set TypeClass, ImplType)
meta
                      forall (m :: * -> *) a. Monad m => a -> m a
return (InfernoType
t, [])
                    PTuple SourcePos
_ TList (Pat (Pinned VCObjectHash) SourcePos, Maybe SourcePos)
ps SourcePos
_ -> do
                      ([InfernoType]
ts, [(Ident, TypeMetadata TCScheme)]
cs) <- forall {b}.
[(Pat (Pinned VCObjectHash) SourcePos, b)]
-> ReaderT
     Env
     (StateT InferState (ExceptT [TypeError SourcePos] Identity))
     ([InfernoType], [(Ident, TypeMetadata TCScheme)])
aux forall a b. (a -> b) -> a -> b
$ forall a. TList a -> [a]
tListToList TList (Pat (Pinned VCObjectHash) SourcePos, Maybe SourcePos)
ps
                      let inferredTy :: InfernoType
inferredTy = TList InfernoType -> InfernoType
TTuple forall a b. (a -> b) -> a -> b
$ forall a. [a] -> TList a
tListFromList [InfernoType]
ts
                      Location SourcePos
-> TypeMetadata (Set TypeClass, ImplType) -> Infer ()
attachTypeToPosition
                        Location SourcePos
patLoc
                        TypeMetadata
                          { identExpr :: Expr () ()
identExpr = Pat () () -> Expr () ()
patternToExpr forall a b. (a -> b) -> a -> b
$ forall (p :: * -> * -> *) a b c d.
Bifunctor p =>
(a -> b) -> (c -> d) -> p a c -> p b d
bimap (forall a b. a -> b -> a
const ()) (forall a b. a -> b -> a
const ()) Pat (Pinned VCObjectHash) SourcePos
pattern,
                            ty :: (Set TypeClass, ImplType)
ty = (forall a. Set a
Set.empty, Map ExtIdent InfernoType -> InfernoType -> ImplType
ImplType forall k a. Map k a
Map.empty forall a b. (a -> b) -> a -> b
$ InfernoType
inferredTy),
                            docs :: Maybe Text
docs = forall a. Maybe a
Nothing
                          }
                      forall (m :: * -> *) a. Monad m => a -> m a
return (InfernoType
inferredTy, [(Ident, TypeMetadata TCScheme)]
cs)
                      where
                        aux :: [(Pat (Pinned VCObjectHash) SourcePos, b)]
-> ReaderT
     Env
     (StateT InferState (ExceptT [TypeError SourcePos] Identity))
     ([InfernoType], [(Ident, TypeMetadata TCScheme)])
aux [] = forall (m :: * -> *) a. Monad m => a -> m a
return ([], [])
                        aux ((Pat (Pinned VCObjectHash) SourcePos
p', b
_l) : [(Pat (Pinned VCObjectHash) SourcePos, b)]
ps') = do
                          (InfernoType
t, [(Ident, TypeMetadata TCScheme)]
vars1) <- Pat (Pinned VCObjectHash) SourcePos
-> ReaderT
     Env
     (StateT InferState (ExceptT [TypeError SourcePos] Identity))
     (InfernoType, [(Ident, TypeMetadata TCScheme)])
mkPatConstraint Pat (Pinned VCObjectHash) SourcePos
p'
                          ([InfernoType]
ts, [(Ident, TypeMetadata TCScheme)]
vars2) <- [(Pat (Pinned VCObjectHash) SourcePos, b)]
-> ReaderT
     Env
     (StateT InferState (ExceptT [TypeError SourcePos] Identity))
     ([InfernoType], [(Ident, TypeMetadata TCScheme)])
aux [(Pat (Pinned VCObjectHash) SourcePos, b)]
ps'
                          forall (m :: * -> *) a. Monad m => a -> m a
return (InfernoType
t forall a. a -> [a] -> [a]
: [InfernoType]
ts, [(Ident, TypeMetadata TCScheme)]
vars1 forall a. [a] -> [a] -> [a]
++ [(Ident, TypeMetadata TCScheme)]
vars2)
                    PVar SourcePos
_ Maybe Ident
Nothing -> do
                      InfernoType
tv <- Infer InfernoType
fresh
                      let meta :: TypeMetadata (Set a, ImplType)
meta =
                            TypeMetadata
                              { identExpr :: Expr () ()
identExpr = Pat () () -> Expr () ()
patternToExpr forall a b. (a -> b) -> a -> b
$ forall (p :: * -> * -> *) a b c d.
Bifunctor p =>
(a -> b) -> (c -> d) -> p a c -> p b d
bimap (forall a b. a -> b -> a
const ()) (forall a b. a -> b -> a
const ()) Pat (Pinned VCObjectHash) SourcePos
pattern,
                                ty :: (Set a, ImplType)
ty = (forall a. Set a
Set.empty, Map ExtIdent InfernoType -> InfernoType -> ImplType
ImplType forall k a. Map k a
Map.empty InfernoType
tv),
                                docs :: Maybe Text
docs = forall a. Maybe a
Nothing
                              }
                      Location SourcePos
-> TypeMetadata (Set TypeClass, ImplType) -> Infer ()
attachTypeToPosition Location SourcePos
patLoc forall {a}. TypeMetadata (Set a, ImplType)
meta
                      forall (m :: * -> *) a. Monad m => a -> m a
return (InfernoType
tv, [])
                    PCommentAbove Comment SourcePos
_ Pat (Pinned VCObjectHash) SourcePos
p -> Pat (Pinned VCObjectHash) SourcePos
-> ReaderT
     Env
     (StateT InferState (ExceptT [TypeError SourcePos] Identity))
     (InfernoType, [(Ident, TypeMetadata TCScheme)])
mkPatConstraint Pat (Pinned VCObjectHash) SourcePos
p
                    PCommentAfter Pat (Pinned VCObjectHash) SourcePos
p Comment SourcePos
_ -> Pat (Pinned VCObjectHash) SourcePos
-> ReaderT
     Env
     (StateT InferState (ExceptT [TypeError SourcePos] Identity))
     (InfernoType, [(Ident, TypeMetadata TCScheme)])
mkPatConstraint Pat (Pinned VCObjectHash) SourcePos
p
                    PCommentBelow Pat (Pinned VCObjectHash) SourcePos
p Comment SourcePos
_ -> Pat (Pinned VCObjectHash) SourcePos
-> ReaderT
     Env
     (StateT InferState (ExceptT [TypeError SourcePos] Identity))
     (InfernoType, [(Ident, TypeMetadata TCScheme)])
mkPatConstraint Pat (Pinned VCObjectHash) SourcePos
p

            checkVariableOverlap :: Map.Map Ident (Location SourcePos) -> Pat (Pinned VCObjectHash) SourcePos -> Infer (Map.Map Ident (Location SourcePos))
            checkVariableOverlap :: Map Ident (Location SourcePos)
-> Pat (Pinned VCObjectHash) SourcePos
-> Infer (Map Ident (Location SourcePos))
checkVariableOverlap Map Ident (Location SourcePos)
vars Pat (Pinned VCObjectHash) SourcePos
pattern =
              let patLoc :: Location SourcePos
patLoc = forall (f :: * -> *).
BlockUtils f =>
f SourcePos -> Location SourcePos
blockPosition Pat (Pinned VCObjectHash) SourcePos
pattern
               in case Pat (Pinned VCObjectHash) SourcePos
pattern of
                    PVar SourcePos
_ (Just Ident
x) -> case forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Ident
x Map Ident (Location SourcePos)
vars of
                      Just Location SourcePos
loc' -> forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError [forall a. Ident -> Location a -> Location a -> TypeError a
VarMultipleOccurrence Ident
x Location SourcePos
patLoc Location SourcePos
loc']
                      Maybe (Location SourcePos)
Nothing -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert Ident
x Location SourcePos
patLoc Map Ident (Location SourcePos)
vars
                    POne SourcePos
_ Pat (Pinned VCObjectHash) SourcePos
p -> Map Ident (Location SourcePos)
-> Pat (Pinned VCObjectHash) SourcePos
-> Infer (Map Ident (Location SourcePos))
checkVariableOverlap Map Ident (Location SourcePos)
vars Pat (Pinned VCObjectHash) SourcePos
p
                    PTuple SourcePos
_ TList (Pat (Pinned VCObjectHash) SourcePos, Maybe SourcePos)
ps SourcePos
_ -> forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM Map Ident (Location SourcePos)
-> Pat (Pinned VCObjectHash) SourcePos
-> Infer (Map Ident (Location SourcePos))
checkVariableOverlap Map Ident (Location SourcePos)
vars forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> a
fst forall a b. (a -> b) -> a -> b
$ forall a. TList a -> [a]
tListToList TList (Pat (Pinned VCObjectHash) SourcePos, Maybe SourcePos)
ps
                    Pat (Pinned VCObjectHash) SourcePos
_ -> forall (m :: * -> *) a. Monad m => a -> m a
return Map Ident (Location SourcePos)
vars
        CommentAbove Comment SourcePos
p Expr (Pinned VCObjectHash) SourcePos
e -> do
          (Expr (Pinned VCObjectHash) SourcePos
e', ImplType
ty, Set Constraint
cs) <- Expr (Pinned VCObjectHash) SourcePos
-> Infer
     (Expr (Pinned VCObjectHash) SourcePos, ImplType, Set Constraint)
infer Expr (Pinned VCObjectHash) SourcePos
e
          forall (m :: * -> *) a. Monad m => a -> m a
return (forall hash pos. Comment pos -> Expr hash pos -> Expr hash pos
CommentAbove Comment SourcePos
p Expr (Pinned VCObjectHash) SourcePos
e', ImplType
ty, Set Constraint
cs)
        CommentAfter Expr (Pinned VCObjectHash) SourcePos
e Comment SourcePos
p -> do
          (Expr (Pinned VCObjectHash) SourcePos
e', ImplType
ty, Set Constraint
cs) <- Expr (Pinned VCObjectHash) SourcePos
-> Infer
     (Expr (Pinned VCObjectHash) SourcePos, ImplType, Set Constraint)
infer Expr (Pinned VCObjectHash) SourcePos
e
          forall (m :: * -> *) a. Monad m => a -> m a
return (forall hash pos. Expr hash pos -> Comment pos -> Expr hash pos
CommentAfter Expr (Pinned VCObjectHash) SourcePos
e' Comment SourcePos
p, ImplType
ty, Set Constraint
cs)
        CommentBelow Expr (Pinned VCObjectHash) SourcePos
e Comment SourcePos
p -> do
          (Expr (Pinned VCObjectHash) SourcePos
e', ImplType
ty, Set Constraint
cs) <- Expr (Pinned VCObjectHash) SourcePos
-> Infer
     (Expr (Pinned VCObjectHash) SourcePos, ImplType, Set Constraint)
infer Expr (Pinned VCObjectHash) SourcePos
e
          forall (m :: * -> *) a. Monad m => a -> m a
return (forall hash pos. Expr hash pos -> Comment pos -> Expr hash pos
CommentBelow Expr (Pinned VCObjectHash) SourcePos
e' Comment SourcePos
p, ImplType
ty, Set Constraint
cs)
        Bracketed SourcePos
p1 Expr (Pinned VCObjectHash) SourcePos
e SourcePos
p2 -> do
          (Expr (Pinned VCObjectHash) SourcePos
e', ImplType
ty, Set Constraint
cs) <- Expr (Pinned VCObjectHash) SourcePos
-> Infer
     (Expr (Pinned VCObjectHash) SourcePos, ImplType, Set Constraint)
infer Expr (Pinned VCObjectHash) SourcePos
e
          forall (m :: * -> *) a. Monad m => a -> m a
return (forall hash pos. pos -> Expr hash pos -> pos -> Expr hash pos
Bracketed SourcePos
p1 Expr (Pinned VCObjectHash) SourcePos
e' SourcePos
p2, ImplType
ty, Set Constraint
cs)
        RenameModule SourcePos
l1 ModuleName
newNm SourcePos
l2 ModuleName
oldNm SourcePos
l3 Expr (Pinned VCObjectHash) SourcePos
e -> do
          s :: InferState
s@InferState {modules :: InferState -> Map ModuleName (Module ())
modules = Map ModuleName (Module ())
mods} <- forall s (m :: * -> *). MonadState s m => m s
get
          forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (ModuleName
newNm forall k a. Ord k => k -> Map k a -> Bool
`Map.member` Map ModuleName (Module ())
mods) forall a b. (a -> b) -> a -> b
$ forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError [forall a. ModuleName -> Location a -> TypeError a
ModuleNameTaken ModuleName
newNm forall a b. (a -> b) -> a -> b
$ forall a. ElementPosition a => SourcePos -> a -> Location SourcePos
elementPosition SourcePos
l1 ModuleName
newNm]
          case forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup ModuleName
oldNm Map ModuleName (Module ())
mods of
            Maybe (Module ())
Nothing -> forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError [forall a. ModuleName -> Location a -> TypeError a
ModuleDoesNotExist ModuleName
oldNm (SourcePos
l2, SourcePos
l3)]
            Just Module ()
oldNmMod -> do
              forall s (m :: * -> *). MonadState s m => s -> m ()
put InferState
s {modules :: Map ModuleName (Module ())
modules = forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert ModuleName
newNm Module ()
oldNmMod Map ModuleName (Module ())
mods}
              (Expr (Pinned VCObjectHash) SourcePos
e', ImplType
ty, Set Constraint
cs) <- Expr (Pinned VCObjectHash) SourcePos
-> Infer
     (Expr (Pinned VCObjectHash) SourcePos, ImplType, Set Constraint)
infer Expr (Pinned VCObjectHash) SourcePos
e
              forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify (\InferState
s' -> InferState
s' {modules :: Map ModuleName (Module ())
modules = forall k a. Ord k => k -> Map k a -> Map k a
Map.delete ModuleName
newNm forall a b. (a -> b) -> a -> b
$ InferState -> Map ModuleName (Module ())
modules InferState
s})
              forall (m :: * -> *) a. Monad m => a -> m a
return (forall hash pos.
pos
-> ModuleName
-> pos
-> ModuleName
-> pos
-> Expr hash pos
-> Expr hash pos
RenameModule SourcePos
l1 ModuleName
newNm SourcePos
l2 ModuleName
oldNm SourcePos
l3 Expr (Pinned VCObjectHash) SourcePos
e', ImplType
ty, Set Constraint
cs)
        OpenModule SourcePos
l1 Pinned VCObjectHash
mHash modNm :: ModuleName
modNm@(ModuleName Text
n) [(Import SourcePos, Maybe SourcePos)]
imports SourcePos
p Expr (Pinned VCObjectHash) SourcePos
e -> do
          InferState {modules :: InferState -> Map ModuleName (Module ())
modules = Map ModuleName (Module ())
mods} <- forall s (m :: * -> *). MonadState s m => m s
get
          case forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup ModuleName
modNm Map ModuleName (Module ())
mods of
            Maybe (Module ())
Nothing -> forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError [forall a. ModuleName -> Location a -> TypeError a
ModuleDoesNotExist ModuleName
modNm forall a b. (a -> b) -> a -> b
$ forall a. ElementPosition a => SourcePos -> a -> Location SourcePos
elementPosition SourcePos
l1 forall a b. (a -> b) -> a -> b
$ Text -> Ident
Ident Text
n]
            Just Module ()
_openMod -> do
              (Expr (Pinned VCObjectHash) SourcePos
e', ImplType
ty, Set Constraint
cs) <- Expr (Pinned VCObjectHash) SourcePos
-> Infer
     (Expr (Pinned VCObjectHash) SourcePos, ImplType, Set Constraint)
infer Expr (Pinned VCObjectHash) SourcePos
e
              forall (m :: * -> *) a. Monad m => a -> m a
return (forall hash pos.
pos
-> hash
-> ModuleName
-> [(Import pos, Maybe pos)]
-> pos
-> Expr hash pos
-> Expr hash pos
OpenModule SourcePos
l1 Pinned VCObjectHash
mHash ModuleName
modNm [(Import SourcePos, Maybe SourcePos)]
imports SourcePos
p Expr (Pinned VCObjectHash) SourcePos
e', ImplType
ty, Set Constraint
cs)

inferPatLit :: Location SourcePos -> Lit -> InfernoType -> Infer (InfernoType, [b])
inferPatLit :: forall b.
Location SourcePos
-> Lit -> InfernoType -> Infer (InfernoType, [b])
inferPatLit Location SourcePos
loc Lit
n InfernoType
t =
  Location SourcePos
-> TypeMetadata (Set TypeClass, ImplType) -> Infer ()
attachTypeToPosition
    Location SourcePos
loc
    TypeMetadata
      { identExpr :: Expr () ()
identExpr = forall hash pos. pos -> Lit -> Expr hash pos
Lit () Lit
n,
        ty :: (Set TypeClass, ImplType)
ty = (forall a. Set a
Set.empty, Map ExtIdent InfernoType -> InfernoType -> ImplType
ImplType forall k a. Map k a
Map.empty InfernoType
t),
        docs :: Maybe Text
docs = forall a. Maybe a
Nothing
      }
    forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> forall (m :: * -> *) a. Monad m => a -> m a
return (InfernoType
t, [])

-------------------------------------------------------------------------------
-- Constraint Solver
-------------------------------------------------------------------------------

-- | The empty substitution
emptySubst :: Subst
emptySubst :: Subst
emptySubst = forall a. Monoid a => a
mempty

-- | Compose substitutions
compose :: Subst -> Subst -> Subst
(Subst Map TV InfernoType
s1) compose :: Subst -> Subst -> Subst
`compose` (Subst Map TV InfernoType
s2) = Map TV InfernoType -> Subst
Subst forall a b. (a -> b) -> a -> b
$ forall a b k. (a -> b) -> Map k a -> Map k b
Map.map (forall a. Substitutable a => Subst -> a -> a
apply (Map TV InfernoType -> Subst
Subst Map TV InfernoType
s1)) Map TV InfernoType
s2 forall k a. Ord k => Map k a -> Map k a -> Map k a
`Map.union` Map TV InfernoType
s1

-- | Run the constraint solver
runSolve :: Set.Set TypeClass -> [Constraint] -> Either [TypeError SourcePos] Subst
runSolve :: Set TypeClass -> [Constraint] -> Either [TypeError SourcePos] Subst
runSolve Set TypeClass
allClasses [Constraint]
cs = forall a. Identity a -> a
runIdentity forall a b. (a -> b) -> a -> b
$ forall e (m :: * -> *) a. ExceptT e m a -> m (Either e a)
runExceptT forall a b. (a -> b) -> a -> b
$ forall a b c. (a -> b -> c) -> b -> a -> c
flip forall r (m :: * -> *) a. ReaderT r m a -> r -> m a
runReaderT Set TypeClass
allClasses forall a b. (a -> b) -> a -> b
$ Unifier -> Solve Subst
solver Unifier
st
  where
    st :: Unifier
st = (Subst
emptySubst, [Constraint]
cs)

unifyMany :: [TypeError SourcePos] -> [InfernoType] -> [InfernoType] -> Solve Subst
unifyMany :: [TypeError SourcePos]
-> [InfernoType] -> [InfernoType] -> Solve Subst
unifyMany [TypeError SourcePos]
_ [] [] = forall (m :: * -> *) a. Monad m => a -> m a
return Subst
emptySubst
unifyMany [TypeError SourcePos]
err (InfernoType
t1 : [InfernoType]
ts1) (InfernoType
t2 : [InfernoType]
ts2) = do
  Subst
su1 <- [TypeError SourcePos] -> InfernoType -> InfernoType -> Solve Subst
unifies [TypeError SourcePos]
err InfernoType
t1 InfernoType
t2
  Subst
su2 <- [TypeError SourcePos]
-> [InfernoType] -> [InfernoType] -> Solve Subst
unifyMany [TypeError SourcePos]
err (forall a. Substitutable a => Subst -> a -> a
apply Subst
su1 [InfernoType]
ts1) (forall a. Substitutable a => Subst -> a -> a
apply Subst
su1 [InfernoType]
ts2)
  forall (m :: * -> *) a. Monad m => a -> m a
return (Subst
su2 Subst -> Subst -> Subst
`compose` Subst
su1)
unifyMany [TypeError SourcePos]
err [InfernoType]
_ [InfernoType]
_ = forall a. [Char] -> a -> a
trace [Char]
"throwing in unifyMany " forall a b. (a -> b) -> a -> b
$ forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError [TypeError SourcePos]
err

unifies :: [TypeError SourcePos] -> InfernoType -> InfernoType -> Solve Subst
unifies :: [TypeError SourcePos] -> InfernoType -> InfernoType -> Solve Subst
unifies [TypeError SourcePos]
_ InfernoType
t1 InfernoType
t2 | InfernoType
t1 forall a. Eq a => a -> a -> Bool
== InfernoType
t2 = forall (m :: * -> *) a. Monad m => a -> m a
return Subst
emptySubst
unifies [TypeError SourcePos]
err (TVar TV
v) InfernoType
t = [TypeError SourcePos] -> TV -> InfernoType -> Solve Subst
bind [TypeError SourcePos]
err TV
v InfernoType
t
unifies [TypeError SourcePos]
err InfernoType
t (TVar TV
v) = [TypeError SourcePos] -> TV -> InfernoType -> Solve Subst
bind [TypeError SourcePos]
err TV
v InfernoType
t
unifies [TypeError SourcePos]
err (TArr InfernoType
t1 InfernoType
t2) (TArr InfernoType
t3 InfernoType
t4) = [TypeError SourcePos]
-> [InfernoType] -> [InfernoType] -> Solve Subst
unifyMany [TypeError SourcePos]
err [InfernoType
t1, InfernoType
t2] [InfernoType
t3, InfernoType
t4]
unifies [TypeError SourcePos]
err (TArray InfernoType
t1) (TArray InfernoType
t2) = [TypeError SourcePos] -> InfernoType -> InfernoType -> Solve Subst
unifies [TypeError SourcePos]
err InfernoType
t1 InfernoType
t2
unifies [TypeError SourcePos]
err (TSeries InfernoType
t1) (TSeries InfernoType
t2) = [TypeError SourcePos] -> InfernoType -> InfernoType -> Solve Subst
unifies [TypeError SourcePos]
err InfernoType
t1 InfernoType
t2
unifies [TypeError SourcePos]
err (TOptional InfernoType
t1) (TOptional InfernoType
t2) = [TypeError SourcePos] -> InfernoType -> InfernoType -> Solve Subst
unifies [TypeError SourcePos]
err InfernoType
t1 InfernoType
t2
unifies [TypeError SourcePos]
err (TTuple TList InfernoType
ts1) (TTuple TList InfernoType
ts2)
  | forall (t :: * -> *) a. Foldable t => t a -> Int
length (forall a. TList a -> [a]
tListToList TList InfernoType
ts1) forall a. Eq a => a -> a -> Bool
== forall (t :: * -> *) a. Foldable t => t a -> Int
length (forall a. TList a -> [a]
tListToList TList InfernoType
ts2) = [TypeError SourcePos]
-> [InfernoType] -> [InfernoType] -> Solve Subst
unifyMany [TypeError SourcePos]
err (forall a. TList a -> [a]
tListToList TList InfernoType
ts1) (forall a. TList a -> [a]
tListToList TList InfernoType
ts2)
  | Bool
otherwise = forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError [forall a.
Set TypeClass
-> InfernoType -> InfernoType -> Location a -> TypeError a
UnificationFail (forall a. [TypeError a] -> Set TypeClass
getTypeClassFromErrs [TypeError SourcePos]
err) (TList InfernoType -> InfernoType
TTuple TList InfernoType
ts1) (TList InfernoType -> InfernoType
TTuple TList InfernoType
ts2) Location SourcePos
loc | Location SourcePos
loc <- (forall b. [TypeError b] -> [Location b]
getLocFromErrs [TypeError SourcePos]
err)]
unifies [TypeError SourcePos]
err InfernoType
_ InfernoType
_ =
  -- trace "throwing in unifies " $
  forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError [TypeError SourcePos]
err

-- Unification solver
solver :: Unifier -> Solve Subst
solver :: Unifier -> Solve Subst
solver (Subst
su, [Constraint]
cs) =
  case [Constraint]
cs of
    [] -> forall (m :: * -> *) a. Monad m => a -> m a
return Subst
su
    [Constraint]
_ -> do
      let ([(InfernoType, InfernoType, [TypeError SourcePos])]
tyConstrs, [(Location SourcePos, TypeClass)]
typeCls) = forall a b. [Either a b] -> ([a], [b])
partitionEithers [Constraint]
cs
      Subst
su1 <- Subst
-> [(InfernoType, InfernoType, [TypeError SourcePos])]
-> Solve Subst
solverTyCs Subst
su [(InfernoType, InfernoType, [TypeError SourcePos])]
tyConstrs
      let partResolvedTyCls :: [(Location SourcePos, TypeClass)]
partResolvedTyCls = forall a b. (a -> b) -> [a] -> [b]
map (\(Location SourcePos
loc, TypeClass
tc) -> (Location SourcePos
loc, forall a. Substitutable a => Subst -> a -> a
apply Subst
su1 TypeClass
tc)) [(Location SourcePos, TypeClass)]
typeCls
      -- trace ("partResolvedTyCls: " <> (intercalate "\n" $ map (unpack . renderPretty . pretty . snd) partResolvedTyCls)) $
      forall st a. SolveState st a -> st -> Solve a
evalSolveState (Subst
-> SolveState
     (Set (Location SourcePos, TypeClass),
      Set (Location SourcePos, TypeClass))
     Subst
solverTypeClasses forall a b. (a -> b) -> a -> b
$ Subst
su1 Subst -> Subst -> Subst
`compose` Subst
su) (forall a. Ord a => [a] -> Set a
Set.fromList [(Location SourcePos, TypeClass)]
partResolvedTyCls, forall a. Monoid a => a
mempty)

solverTyCs :: Subst -> [(InfernoType, InfernoType, [TypeError SourcePos])] -> Solve Subst
solverTyCs :: Subst
-> [(InfernoType, InfernoType, [TypeError SourcePos])]
-> Solve Subst
solverTyCs Subst
su [(InfernoType, InfernoType, [TypeError SourcePos])]
cs =
  case [(InfernoType, InfernoType, [TypeError SourcePos])]
cs of
    [] -> forall (m :: * -> *) a. Monad m => a -> m a
return Subst
su
    ((InfernoType
t1, InfernoType
t2, [TypeError SourcePos]
errs) : [(InfernoType, InfernoType, [TypeError SourcePos])]
cs0) -> do
      Subst
su1 <- [TypeError SourcePos] -> InfernoType -> InfernoType -> Solve Subst
unifies [TypeError SourcePos]
errs InfernoType
t1 InfernoType
t2
      Subst
-> [(InfernoType, InfernoType, [TypeError SourcePos])]
-> Solve Subst
solverTyCs (Subst
su1 Subst -> Subst -> Subst
`compose` Subst
su) (forall a b. (a -> b) -> [a] -> [b]
map (\(InfernoType
t1', InfernoType
t2', [TypeError SourcePos]
es) -> (forall a. Substitutable a => Subst -> a -> a
apply Subst
su1 InfernoType
t1', forall a. Substitutable a => Subst -> a -> a
apply Subst
su1 InfernoType
t2', forall a b. (a -> b) -> [a] -> [b]
map (forall a. Substitutable a => Subst -> a -> a
apply Subst
su1) [TypeError SourcePos]
es)) [(InfernoType, InfernoType, [TypeError SourcePos])]
cs0)

evalSolveState :: SolveState st a -> st -> Solve a
evalSolveState :: forall st a. SolveState st a -> st -> Solve a
evalSolveState (ReaderT Set TypeClass
-> StateT st (ExceptT [TypeError SourcePos] Identity) a
f) st
st = forall r (m :: * -> *) a. (r -> m a) -> ReaderT r m a
ReaderT forall a b. (a -> b) -> a -> b
$ \Set TypeClass
r -> forall (m :: * -> *) s a. Monad m => StateT s m a -> s -> m a
evalStateT (Set TypeClass
-> StateT st (ExceptT [TypeError SourcePos] Identity) a
f Set TypeClass
r) st
st

liftToSolveState :: Solve a -> SolveState st a
liftToSolveState :: forall a st. Solve a -> SolveState st a
liftToSolveState (ReaderT Set TypeClass -> ExceptT [TypeError SourcePos] Identity a
f) = forall r (m :: * -> *) a. (r -> m a) -> ReaderT r m a
ReaderT forall a b. (a -> b) -> a -> b
$ \Set TypeClass
r -> forall s (m :: * -> *) a. (s -> m (a, s)) -> StateT s m a
StateT forall a b. (a -> b) -> a -> b
$ \st
s -> (,st
s) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Set TypeClass -> ExceptT [TypeError SourcePos] Identity a
f Set TypeClass
r

pick :: (Show a, Ord a) => SolveState (Set.Set a, Set.Set a) (Maybe a)
pick :: forall a. (Show a, Ord a) => SolveState (Set a, Set a) (Maybe a)
pick = forall s (m :: * -> *) a. MonadState s m => (s -> (a, s)) -> m a
state forall a b. (a -> b) -> a -> b
$ \st :: (Set a, Set a)
st@(Set a
current, Set a
marked) ->
  case forall a. Set a -> Maybe a
Set.lookupMin Set a
current of
    Maybe a
Nothing -> (forall a. Maybe a
Nothing, (Set a, Set a)
st)
    Just a
a -> (forall a. a -> Maybe a
Just a
a, (forall a. Ord a => a -> Set a -> Set a
Set.delete a
a Set a
current, forall a. Ord a => a -> Set a -> Set a
Set.insert a
a Set a
marked))

-- | `applySubsts` applies the substitution `su` on both marked and unmarked typeclasses and an new information, propagated to
--   marked typeclasses, causes said typeclass to be moved back to the "current" set.
--   We then filter out any fully resolved classes in the marked set only!! to avoid extra unnecessary steps.
--   (Filtering the unprocessed, i.e. current classes may lead to subtle bugs if the class is fully instantiated but
--   is not in fact an instance found in `allClasses`)
applySubsts :: Ord loc => Subst -> SolveState (Set.Set (loc, TypeClass), Set.Set (loc, TypeClass)) ()
applySubsts :: forall loc.
Ord loc =>
Subst -> SolveState (Set (loc, TypeClass), Set (loc, TypeClass)) ()
applySubsts Subst
su = forall s (m :: * -> *) a. MonadState s m => (s -> (a, s)) -> m a
state forall a b. (a -> b) -> a -> b
$ \(Set (loc, TypeClass)
current, Set (loc, TypeClass)
marked) ->
  (\(Set (loc, TypeClass)
c, Set (loc, TypeClass)
m) -> ((), (Set (loc, TypeClass)
c, forall {a}. Set (a, TypeClass) -> Set (a, TypeClass)
filterFullyInstantiated Set (loc, TypeClass)
m))) forall a b. (a -> b) -> a -> b
$
    forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr
      ( \(loc
loc, TypeClass
a) (Set (loc, TypeClass)
current', Set (loc, TypeClass)
marked') ->
          let a' :: TypeClass
a' = forall a. Substitutable a => Subst -> a -> a
apply Subst
su TypeClass
a
           in if TypeClass
a forall a. Eq a => a -> a -> Bool
== TypeClass
a'
                then (Set (loc, TypeClass)
current', forall a. Ord a => a -> Set a -> Set a
Set.insert (loc
loc, TypeClass
a') Set (loc, TypeClass)
marked')
                else (forall a. Ord a => a -> Set a -> Set a
Set.insert (loc
loc, TypeClass
a') Set (loc, TypeClass)
current', Set (loc, TypeClass)
marked')
      )
      (forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map (\(loc
loc, TypeClass
a) -> (loc
loc, forall a. Substitutable a => Subst -> a -> a
apply Subst
su TypeClass
a)) Set (loc, TypeClass)
current, forall a. Monoid a => a
mempty)
      Set (loc, TypeClass)
marked
  where
    filterFullyInstantiated :: Set (a, TypeClass) -> Set (a, TypeClass)
filterFullyInstantiated =
      forall a. (a -> Bool) -> Set a -> Set a
Set.filter forall a b. (a -> b) -> a -> b
$
        Bool -> Bool
not
          forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Set a -> Bool
Set.null
          forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Substitutable a => a -> Set TV
ftv
          forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> b
snd

solverTypeClasses :: Subst -> SolveState (Set.Set (Location SourcePos, TypeClass), Set.Set (Location SourcePos, TypeClass)) Subst
solverTypeClasses :: Subst
-> SolveState
     (Set (Location SourcePos, TypeClass),
      Set (Location SourcePos, TypeClass))
     Subst
solverTypeClasses Subst
su =
  forall a. (Show a, Ord a) => SolveState (Set a, Set a) (Maybe a)
pick forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
    Maybe (Location SourcePos, TypeClass)
Nothing -> forall (m :: * -> *) a. Monad m => a -> m a
return Subst
su
    Just (Location SourcePos
loc, tc :: TypeClass
tc@(TypeClass Text
nm [InfernoType]
tys)) -> do
      Set TypeClass
allClasses <- forall r (m :: * -> *). MonadReader r m => m r
ask
      let matchingInstances :: [TypeClass]
matchingInstances = forall a. Set a -> [a]
Set.toList forall a b. (a -> b) -> a -> b
$ forall a. (a -> Bool) -> Set a -> Set a
Set.filter (\(TypeClass Text
nm' [InfernoType]
_) -> Text
nm forall a. Eq a => a -> a -> Bool
== Text
nm') Set TypeClass
allClasses
      if forall (t :: * -> *) a. Foldable t => t a -> Bool
null [TypeClass]
matchingInstances
        then forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError [forall a. Set TypeClass -> TypeClass -> Location a -> TypeError a
TypeClassNotFoundError Set TypeClass
allClasses TypeClass
tc Location SourcePos
loc]
        else do
          [Subst]
res <- forall a st. Solve a -> SolveState st a
liftToSolveState (forall a. [Maybe a] -> [a]
catMaybes forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [TypeClass]
matchingInstances ([InfernoType] -> TypeClass -> Solve (Maybe Subst)
tryMatchPartial [InfernoType]
tys))
          case [Subst]
res of
            [] -> forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError [forall a. TypeClass -> Location a -> TypeError a
TypeClassNoPartialMatch TypeClass
tc Location SourcePos
loc]
            (Subst Map TV InfernoType
s : [Subst]
xs) -> do
              -- even if we have multiple matching substitutions, we can still make progress if they all agree
              -- on some parameter
              let su' :: Subst
su' = (Map TV InfernoType -> Subst
Subst forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr Map TV InfernoType -> Map TV InfernoType -> Map TV InfernoType
intersection Map TV InfernoType
s [Map TV InfernoType
x | Subst Map TV InfernoType
x <- [Subst]
xs]) Subst -> Subst -> Subst
`compose` Subst
su
              -- trace ("applying su': "<> show su' <> "\nprevious was su: " <> show su) $
              forall loc.
Ord loc =>
Subst -> SolveState (Set (loc, TypeClass), Set (loc, TypeClass)) ()
applySubsts Subst
su'
              Subst
-> SolveState
     (Set (Location SourcePos, TypeClass),
      Set (Location SourcePos, TypeClass))
     Subst
solverTypeClasses Subst
su'
  where
    intersection :: Map TV InfernoType -> Map TV InfernoType -> Map TV InfernoType
intersection = 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
Map.merge forall (f :: * -> *) k x y. Applicative f => WhenMissing f k x y
Map.dropMissing forall (f :: * -> *) k x y. Applicative f => WhenMissing f k x y
Map.dropMissing (forall (f :: * -> *) k x y z.
Applicative f =>
(k -> x -> y -> Maybe z) -> WhenMatched f k x y z
Map.zipWithMaybeMatched forall a b. (a -> b) -> a -> b
$ \TV
_ InfernoType
a InfernoType
b -> if InfernoType
a forall a. Eq a => a -> a -> Bool
== InfernoType
b then forall a. a -> Maybe a
Just InfernoType
a else forall a. Maybe a
Nothing)

newtype Counter = Counter Int

-- | Use `getLit` if you want to remember what it points to, i.e. if mapping a (TVar, InfernoType) to a SAT solver variable
getLit :: (MonadState s m, HasType (Bimap.Bimap Int a) s, HasType Counter s, Ord a) => a -> m Int
getLit :: forall s (m :: * -> *) a.
(MonadState s m, HasType (Bimap Int a) s, HasType Counter s,
 Ord a) =>
a -> m Int
getLit a
a = do
  s
st <- forall s (m :: * -> *). MonadState s m => m s
get
  let bm :: Bimap Int a
bm = forall a s. HasType a s => s -> a
getTyped s
st
  let Counter Int
i = forall a s. HasType a s => s -> a
getTyped s
st
  case forall a b (m :: * -> *).
(Ord a, Ord b, MonadThrow m) =>
b -> Bimap a b -> m a
Bimap.lookupR a
a Bimap Int a
bm of
    Just Int
l -> forall (f :: * -> *) a. Applicative f => a -> f a
pure Int
l
    Maybe Int
Nothing -> do
      forall s (m :: * -> *). MonadState s m => s -> m ()
put forall a b. (a -> b) -> a -> b
$ forall a s. HasType a s => a -> s -> s
setTyped (Int -> Counter
Counter forall a b. (a -> b) -> a -> b
$ Int
i forall a. Num a => a -> a -> a
+ Int
1) forall a b. (a -> b) -> a -> b
$ forall a s. HasType a s => a -> s -> s
setTyped (forall a b. (Ord a, Ord b) => a -> b -> Bimap a b -> Bimap a b
Bimap.insert Int
i a
a Bimap Int a
bm) s
st
      forall (f :: * -> *) a. Applicative f => a -> f a
pure Int
i

-- | Return a fresh SAT solver variable
newLit :: (MonadState s m, HasType Counter s) => m Int
newLit :: forall s (m :: * -> *).
(MonadState s m, HasType Counter s) =>
m Int
newLit = do
  s
st <- forall s (m :: * -> *). MonadState s m => m s
get
  let Counter Int
i = forall a s. HasType a s => s -> a
getTyped s
st
  forall s (m :: * -> *). MonadState s m => s -> m ()
put forall a b. (a -> b) -> a -> b
$ forall a s. HasType a s => a -> s -> s
setTyped (Int -> Counter
Counter forall a b. (a -> b) -> a -> b
$ Int
i forall a. Num a => a -> a -> a
+ Int
1) s
st
  forall (f :: * -> *) a. Applicative f => a -> f a
pure Int
i

addClause :: (MonadState s m, HasType [[Int]] s) => [Int] -> m ()
addClause :: forall s (m :: * -> *).
(MonadState s m, HasType [[Int]] s) =>
[Int] -> m ()
addClause [Int]
c = do
  s
st <- forall s (m :: * -> *). MonadState s m => m s
get
  let clauses :: [[Int]]
clauses = forall a s. HasType a s => s -> a
getTyped s
st
  forall s (m :: * -> *). MonadState s m => s -> m ()
put forall a b. (a -> b) -> a -> b
$ forall a s. HasType a s => a -> s -> s
setTyped ([Int]
c forall a. a -> [a] -> [a]
: [[Int]]
clauses) s
st

-- | This function encodes our typeclasses into CNF clauses for the SAT-solver.
-- The translation works in the following way:
-- Given a set of type-classes, e.g. `{requires addition on 'a int producing 'b ,requires addition on 'b 'b producing double}`
-- we first compute all the matching instances from `allClasses`, in this case, we get:
-- `requires addition on 'a int producing 'b` matches:
-- - `requires addition on int int producing int`
-- - `requires addition on double int producing double`
-- `requires addition on 'b 'b producing double` matches:
-- - `requires addition on double double producing double`
-- Now we translate each possible class instantiation into the following clauses:
-- `requires addition on int int producing int` becomes:
-- `'a_int <-> add_class_1_inst_1_arg_1`
-- `'b_int <-> add_class_1_inst_1_arg_3`
-- `add_class_1_inst_1_arg_1 /\ add_class_1_inst_1_arg_3 <-> add_class_1_inst_1`
-- `requires addition on double int producing double` becomes:
-- `'a_double <-> add_class_1_inst_2_arg_1`
-- `'b_doube <-> add_class_1_inst_2_arg_3`
-- `add_class_1_inst_2_arg_1 /\ add_class_1_inst_2_arg_3 <-> add_class_1_inst_2`
-- We have to make sure that exactly one instance matches,
-- i.e. `requires addition on int int producing int` or `requires addition on double int producing double`, but not both:
-- `add_class_1_inst_1 XOR add_class_1_inst_2`
-- Next we encode the second set of matching instances, namely `requires addition on double double producing double`:
-- `'b_doube <-> add_class_2_inst_1_arg_1`
-- `'b_doube <-> add_class_2_inst_1_arg_2`
-- `add_class_2_inst_1_arg_1 /\ add_class_2_inst_1_arg_2 <-> add_class_2_inst_1`
-- Since the second typeclass only matches one instance, we simply add it in as true:
-- `add_class_2_inst_1`
-- Finally, we collect all the variables with all their possible types and encode the condition that exactly one type for each is matched:
-- `'a_int XOR 'a_double`
-- `'b_int XOR 'b_double`
-- If the SAT solver returns SAT, we simply check which one of `'a_?` and `'b_?` is set to true in the resulting model.
-- If the solver returns the model `'a_double /\ 'b_double` and we want to check for any more solutions, we simply add `-('a_double /\ 'b_double)`
-- (`-'a_double \/ -'b_double` in CNF) as a clause and re-run the solver. Once all assignments have been exhausted, we will get UNSAT.
{-# NOINLINE findTypeClassWitnesses #-}
findTypeClassWitnesses :: Set.Set TypeClass -> Maybe Int -> Set.Set TypeClass -> Set.Set TV -> [Subst]
findTypeClassWitnesses :: Set TypeClass -> Maybe Int -> Set TypeClass -> Set TV -> [Subst]
findTypeClassWitnesses Set TypeClass
allClasses Maybe Int
iters Set TypeClass
tyCls Set TV
tvs =
  forall a. IO a -> a
unsafePerformIO forall a b. (a -> b) -> a -> b
$
    forall a. PS a -> IO a
Picosat.evalScopedPicosat forall a b. (a -> b) -> a -> b
$
      [[Int]] -> PS ()
Picosat.addBaseClauses [[Int]]
clauses forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Maybe Int -> StateT PicosatScoped IO [Subst]
getSolutions Maybe Int
iters
  where
    filteredSubs :: Map TV (Set InfernoType)
filteredSubs = Set TypeClass -> [TypeClass] -> Map TV (Set InfernoType)
filteredTypeClassSubstitutions Set TypeClass
allClasses forall a b. (a -> b) -> a -> b
$ forall a. Set a -> [a]
Set.toList Set TypeClass
tyCls
    (Counter
_, Bimap Int (TV, InfernoType)
litMap, [[Int]]
clauses) = forall a b c. (a -> b -> c) -> b -> a -> c
flip forall s a. State s a -> s -> s
execState (Int -> Counter
Counter Int
1, forall a b. Bimap a b
Bimap.empty, []) forall a b. (a -> b) -> a -> b
$ do
      forall s (f :: * -> *).
(MonadState s f, HasType (Bimap Int (TV, InfernoType)) s,
 HasType [[Int]] s, HasType Counter s) =>
Set TypeClass -> Map TV (Set InfernoType) -> [TypeClass] -> f ()
encodeTypeClasses Set TypeClass
allClasses Map TV (Set InfernoType)
filteredSubs forall a b. (a -> b) -> a -> b
$ forall a. Set a -> [a]
Set.toList Set TypeClass
tyCls
      Bimap Int (TV, InfernoType)
lm :: Bimap.Bimap Int (TV, InfernoType) <- forall a s. HasType a s => s -> a
getTyped forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall s (m :: * -> *). MonadState s m => m s
get
      let ls_grouped :: Map TV [Int]
ls_grouped = forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (\(Int
l, (TV
tv, InfernoType
_)) Map TV [Int]
m' -> forall k a.
Ord k =>
(Maybe a -> Maybe a) -> k -> Map k a -> Map k a
Map.alter (forall a. a -> Maybe a
Just forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall b a. b -> (a -> b) -> Maybe a -> b
maybe [Int
l] (Int
l forall a. a -> [a] -> [a]
:)) TV
tv Map TV [Int]
m') forall a. Monoid a => a
mempty forall a b. (a -> b) -> a -> b
$ forall a b. Bimap a b -> [(a, b)]
Bimap.toList forall a b. (a -> b) -> a -> b
$ Bimap Int (TV, InfernoType)
lm
      forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ (forall k a. Map k a -> [a]
Map.elems Map TV [Int]
ls_grouped) forall a b. (a -> b) -> a -> b
$ \[Int]
ls -> forall s (m :: * -> *).
(MonadState s m, HasType [[Int]] s) =>
[Int] -> m ()
xor [Int]
ls

    getSolutions :: Maybe Int -> StateT PicosatScoped IO [Subst]
getSolutions = \case
      Just Int
0 -> forall (f :: * -> *) a. Applicative f => a -> f a
pure []
      Maybe Int
i -> do
        [Int] -> PS Solution
Picosat.scopedSolutionWithAssumptions [] forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
          Picosat.Solution [Int]
ls -> do
            let found :: [(Int, (TV, InfernoType))]
found = forall a. [Maybe a] -> [a]
catMaybes forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map (\Int
l -> (Int
l,) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a b (m :: * -> *).
(Ord a, Ord b, MonadThrow m) =>
a -> Bimap a b -> m b
Bimap.lookup Int
l Bimap Int (TV, InfernoType)
litMap) [Int]
ls
            [[Int]] -> PS ()
Picosat.addBaseClauses [[-Int
l | (Int
l, (TV
tv, InfernoType
_)) <- [(Int, (TV, InfernoType))]
found, TV
tv forall a. Ord a => a -> Set a -> Bool
`Set.member` Set TV
tvs]]
            ((Map TV InfernoType -> Subst
Subst forall a b. (a -> b) -> a -> b
$ forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> b
snd [(Int, (TV, InfernoType))]
found) forall a. a -> [a] -> [a]
:) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe Int -> StateT PicosatScoped IO [Subst]
getSolutions ((\Int
x -> Int
x forall a. Num a => a -> a -> a
- Int
1) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe Int
i)
          Solution
_ -> forall (f :: * -> *) a. Applicative f => a -> f a
pure []

tryMatchPartial :: [InfernoType] -> TypeClass -> Solve (Maybe Subst)
tryMatchPartial :: [InfernoType] -> TypeClass -> Solve (Maybe Subst)
tryMatchPartial [InfernoType]
tys (TypeClass Text
_ [InfernoType]
tys2) =
  ((forall a. a -> Maybe a
Just forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [TypeError SourcePos]
-> [InfernoType] -> [InfernoType] -> Solve Subst
unifyMany [] [InfernoType]
tys [InfernoType]
tys2) forall e (m :: * -> *) a.
MonadError e m =>
m a -> (e -> m a) -> m a
`catchError` (\[TypeError SourcePos]
_ -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a. Maybe a
Nothing))

-- | This is a minor optimisation for the `encodeTypeClasses` function. The `filteredTypeClassSubstitutions` function takes the set of all type class instances,
-- along with the list of all the current classes we want to unify and computes all the matching substitutions.
-- It then recursively merges all the possible substitutions for each class and intersects the merged maps of each class instance.
-- For example, given `{requires addition on 'a 'b producing 'c, requires multiplication on 'c 'd producing 'e}`, we will first compute the merged substitutions
-- `{'a -> {int, double, time, timeDiff, word16, word32, word64}, 'b -> {int, double, time, timeDiff, word16, word32, word64}, 'c -> {int, double, time, timeDiff, word16, word32, word64}}`
-- for the `addition` typeclass, and
-- `{'c -> {int, double}, 'd -> {int, double}, 'e -> {int, double}}` for the `multiplication` one.
-- Then we merge the two maps and obtain
-- `{'a -> {int, double, time, timeDiff, word16, word32, word64}, 'b -> {int, double, time, timeDiff, word16, word32, word64}, 'c -> {int, double}, 'd -> {int, double}, 'e -> {int, double}}`
-- This map represents the set of all possible "consistent" type assingments for the free variables `'a`,`'b`,..,`'e`, such that there may exist matching instances of both typeclasses.
-- Notice that `'c` can only an `int` or a `double`, because there are no typeclass intances of `multiplication` for any other types. Precomputing these constraints reduces the number of
-- SAT solver clauses somewhat, especially for large arithmetic operations, e.g. `fun a b c d e f g h i j -> a + b * (c - d) + e / f / g * (h + i - j)`
filteredTypeClassSubstitutions :: Set.Set TypeClass -> [TypeClass] -> Map.Map TV (Set.Set InfernoType)
filteredTypeClassSubstitutions :: Set TypeClass -> [TypeClass] -> Map TV (Set InfernoType)
filteredTypeClassSubstitutions Set TypeClass
allClasses = \case
  [] -> forall a. Monoid a => a
mempty
  TypeClass Text
nm [InfernoType]
tys : [TypeClass]
tcs -> do
    let possibleMatchingInstances :: [TypeClass]
possibleMatchingInstances = forall a. Set a -> [a]
Set.toList forall a b. (a -> b) -> a -> b
$ forall a. (a -> Bool) -> Set a -> Set a
Set.filter (\(TypeClass Text
nm' [InfernoType]
_) -> Text
nm forall a. Eq a => a -> a -> Bool
== Text
nm') Set TypeClass
allClasses
    case forall a. Identity a -> a
runIdentity forall a b. (a -> b) -> a -> b
$ forall e (m :: * -> *) a. ExceptT e m a -> m (Either e a)
runExceptT forall a b. (a -> b) -> a -> b
$ forall a b c. (a -> b -> c) -> b -> a -> c
flip forall r (m :: * -> *) a. ReaderT r m a -> r -> m a
runReaderT Set TypeClass
allClasses forall a b. (a -> b) -> a -> b
$ (forall a. [Maybe a] -> [a]
catMaybes forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [TypeClass]
possibleMatchingInstances ([InfernoType] -> TypeClass -> Solve (Maybe Subst)
tryMatchPartial [InfernoType]
tys)) of
      Left [TypeError SourcePos]
_ -> Set TypeClass -> [TypeClass] -> Map TV (Set InfernoType)
filteredTypeClassSubstitutions Set TypeClass
allClasses [TypeClass]
tcs
      Right [Subst]
subs' ->
        let subs :: [Map TV InfernoType]
subs = [Map TV InfernoType
su | Subst Map TV InfernoType
su <- [Subst]
subs']
            mergedSubs :: Map TV (Set InfernoType)
mergedSubs = forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (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
Map.merge (forall (f :: * -> *) k x y.
Applicative f =>
(k -> x -> y) -> WhenMissing f k x y
Map.mapMissing forall a b. (a -> b) -> a -> b
$ \TV
_k InfernoType
a -> forall a. a -> Set a
Set.singleton InfernoType
a) forall (f :: * -> *) k x. Applicative f => WhenMissing f k x x
Map.preserveMissing forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) k x y z.
Applicative f =>
(k -> x -> y -> z) -> WhenMatched f k x y z
Map.zipWithMatched forall a b. (a -> b) -> a -> b
$ \TV
_k InfernoType
a Set InfernoType
as -> forall a. Ord a => a -> Set a -> Set a
Set.insert InfernoType
a Set InfernoType
as) forall a. Monoid a => a
mempty [Map TV InfernoType]
subs
            finalMap :: Map TV (Set InfernoType)
finalMap = Set TypeClass -> [TypeClass] -> Map TV (Set InfernoType)
filteredTypeClassSubstitutions Set TypeClass
allClasses [TypeClass]
tcs
         in 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
Map.merge forall (f :: * -> *) k x. Applicative f => WhenMissing f k x x
Map.preserveMissing forall (f :: * -> *) k x. Applicative f => WhenMissing f k x x
Map.preserveMissing (forall (f :: * -> *) k x y z.
Applicative f =>
(k -> x -> y -> z) -> WhenMatched f k x y z
Map.zipWithMatched forall a b. (a -> b) -> a -> b
$ \TV
_k Set InfernoType
as Set InfernoType
bs -> forall a. Ord a => Set a -> Set a -> Set a
Set.intersection Set InfernoType
as Set InfernoType
bs) Map TV (Set InfernoType)
mergedSubs Map TV (Set InfernoType)
finalMap

encodeTypeClasses ::
  (MonadState s f, HasType (Bimap.Bimap Int (TV, InfernoType)) s, HasType [[Int]] s, HasType Counter s) =>
  Set.Set TypeClass ->
  Map.Map TV (Set.Set InfernoType) ->
  [TypeClass] ->
  f ()
encodeTypeClasses :: forall s (f :: * -> *).
(MonadState s f, HasType (Bimap Int (TV, InfernoType)) s,
 HasType [[Int]] s, HasType Counter s) =>
Set TypeClass -> Map TV (Set InfernoType) -> [TypeClass] -> f ()
encodeTypeClasses Set TypeClass
allClasses Map TV (Set InfernoType)
filteredSubs = \case
  [] -> forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
  TypeClass Text
nm [InfernoType]
tys : [TypeClass]
tcs -> do
    let possibleMatchingInstances :: [TypeClass]
possibleMatchingInstances = forall a. Set a -> [a]
Set.toList forall a b. (a -> b) -> a -> b
$ forall a. (a -> Bool) -> Set a -> Set a
Set.filter (\(TypeClass Text
nm' [InfernoType]
_) -> Text
nm forall a. Eq a => a -> a -> Bool
== Text
nm') Set TypeClass
allClasses
    case forall a. Identity a -> a
runIdentity forall a b. (a -> b) -> a -> b
$ forall e (m :: * -> *) a. ExceptT e m a -> m (Either e a)
runExceptT forall a b. (a -> b) -> a -> b
$ forall a b c. (a -> b -> c) -> b -> a -> c
flip forall r (m :: * -> *) a. ReaderT r m a -> r -> m a
runReaderT Set TypeClass
allClasses forall a b. (a -> b) -> a -> b
$ (forall a. [Maybe a] -> [a]
catMaybes forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [TypeClass]
possibleMatchingInstances ([InfernoType] -> TypeClass -> Solve (Maybe Subst)
tryMatchPartial [InfernoType]
tys)) of
      Left [TypeError SourcePos]
_err -> forall s (f :: * -> *).
(MonadState s f, HasType (Bimap Int (TV, InfernoType)) s,
 HasType [[Int]] s, HasType Counter s) =>
Set TypeClass -> Map TV (Set InfernoType) -> [TypeClass] -> f ()
encodeTypeClasses Set TypeClass
allClasses Map TV (Set InfernoType)
filteredSubs [TypeClass]
tcs
      Right [Subst]
subs -> do
        [Int]
insts <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM ([Subst] -> [Subst]
filterSubs [Subst]
subs) forall a b. (a -> b) -> a -> b
$ \(Subst Map TV InfernoType
su) -> do
          [Int]
ls <-
            forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat
              forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ( forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [InfernoType]
tys forall a b. (a -> b) -> a -> b
$ \InfernoType
t ->
                      case InfernoType
t of
                        TVar TV
tv -> do
                          let t' :: InfernoType
t' = Map TV InfernoType
su forall k a. Ord k => Map k a -> k -> a
Map.! TV
tv
                          Int
tvLit <- forall s (m :: * -> *) a.
(MonadState s m, HasType (Bimap Int a) s, HasType Counter s,
 Ord a) =>
a -> m Int
getLit (TV
tv, InfernoType
t')
                          Int
freshLit <- forall s (m :: * -> *).
(MonadState s m, HasType Counter s) =>
m Int
newLit
                          [Int
tvLit] forall {s} {m :: * -> *}.
(MonadState s m, HasType [[Int]] s) =>
[Int] -> Int -> m ()
`iff` Int
freshLit
                          forall (f :: * -> *) a. Applicative f => a -> f a
pure [Int
freshLit]
                        InfernoType
_ -> forall (f :: * -> *) a. Applicative f => a -> f a
pure []
                  )
          Int
freshLit <- forall s (m :: * -> *).
(MonadState s m, HasType Counter s) =>
m Int
newLit
          [Int]
ls forall {s} {m :: * -> *}.
(MonadState s m, HasType [[Int]] s) =>
[Int] -> Int -> m ()
`iff` Int
freshLit
          forall (f :: * -> *) a. Applicative f => a -> f a
pure Int
freshLit
        forall s (m :: * -> *).
(MonadState s m, HasType [[Int]] s) =>
[Int] -> m ()
xor [Int]
insts
        forall s (f :: * -> *).
(MonadState s f, HasType (Bimap Int (TV, InfernoType)) s,
 HasType [[Int]] s, HasType Counter s) =>
Set TypeClass -> Map TV (Set InfernoType) -> [TypeClass] -> f ()
encodeTypeClasses Set TypeClass
allClasses Map TV (Set InfernoType)
filteredSubs [TypeClass]
tcs
  where
    filterSubs :: [Subst] -> [Subst]
filterSubs =
      forall a. (a -> Bool) -> [a] -> [a]
filter forall a b. (a -> b) -> a -> b
$ \(Subst Map TV InfernoType
su) ->
        forall k a b. (k -> a -> b -> b) -> b -> Map k a -> b
Map.foldrWithKey
          ( \TV
k InfernoType
v Bool
cond ->
              Bool
cond Bool -> Bool -> Bool
&& case forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup TV
k Map TV (Set InfernoType)
filteredSubs of
                Maybe (Set InfernoType)
Nothing -> Bool
False
                Just Set InfernoType
vs -> forall a. Ord a => a -> Set a -> Bool
Set.member InfernoType
v Set InfernoType
vs
          )
          Bool
True
          Map TV InfernoType
su

    -- a_1 /\ ... /\ a_n -> b is equivalent to -a_1 \/ ... \/ -a_n \/ b
    impl :: [Int] -> Int -> m ()
impl [Int]
as Int
b = forall s (m :: * -> *).
(MonadState s m, HasType [[Int]] s) =>
[Int] -> m ()
addClause forall a b. (a -> b) -> a -> b
$ Int
b forall a. a -> [a] -> [a]
: forall a b. (a -> b) -> [a] -> [b]
map (\Int
a -> -Int
a) [Int]
as
    -- a_1 /\ ... /\ a_n <-> b is equivalent to (a_1 /\ ... /\ a_n -> b) /\ (b -> a_1) /\ ... /\ (b -> a_n)
    iff :: [Int] -> Int -> m ()
iff [Int]
as Int
b = do
      [Int]
as forall {s} {m :: * -> *}.
(MonadState s m, HasType [[Int]] s) =>
[Int] -> Int -> m ()
`impl` Int
b
      forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ [Int]
as forall a b. (a -> b) -> a -> b
$ \Int
a -> [Int
b] forall {s} {m :: * -> *}.
(MonadState s m, HasType [[Int]] s) =>
[Int] -> Int -> m ()
`impl` Int
a

xor :: (MonadState s m, HasType [[Int]] s) => [Int] -> m ()
xor :: forall s (m :: * -> *).
(MonadState s m, HasType [[Int]] s) =>
[Int] -> m ()
xor [Int]
ls =
  do
    forall s (m :: * -> *).
(MonadState s m, HasType [[Int]] s) =>
[Int] -> m ()
addClause [Int]
ls
    forall {f :: * -> *} {s}.
(MonadState s f, HasType [[Int]] s) =>
[Int] -> f ()
go [Int]
ls
  where
    go :: [Int] -> f ()
go [] = forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
    go (Int
x : [Int]
xs) = do
      forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ [Int]
xs forall a b. (a -> b) -> a -> b
$ \Int
y -> forall s (m :: * -> *).
(MonadState s m, HasType [[Int]] s) =>
[Int] -> m ()
addClause [-Int
x, -Int
y]
      [Int] -> f ()
go [Int]
xs

bind :: [TypeError SourcePos] -> TV -> InfernoType -> Solve Subst
bind :: [TypeError SourcePos] -> TV -> InfernoType -> Solve Subst
bind [TypeError SourcePos]
err TV
a InfernoType
t
  | InfernoType
t forall a. Eq a => a -> a -> Bool
== TV -> InfernoType
TVar TV
a = forall (m :: * -> *) a. Monad m => a -> m a
return Subst
emptySubst
  | forall a. Substitutable a => TV -> a -> Bool
occursCheck TV
a InfernoType
t = forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError [forall a. TV -> InfernoType -> Location a -> TypeError a
InfiniteType TV
a InfernoType
t Location SourcePos
loc | Location SourcePos
loc <- (forall b. [TypeError b] -> [Location b]
getLocFromErrs [TypeError SourcePos]
err)]
  | Bool
otherwise = forall (m :: * -> *) a. Monad m => a -> m a
return (Map TV InfernoType -> Subst
Subst forall a b. (a -> b) -> a -> b
$ forall k a. k -> a -> Map k a
Map.singleton TV
a InfernoType
t)

occursCheck :: Substitutable a => TV -> a -> Bool
occursCheck :: forall a. Substitutable a => TV -> a -> Bool
occursCheck TV
a a
t = TV
a forall a. Ord a => a -> Set a -> Bool
`Set.member` forall a. Substitutable a => a -> Set TV
ftv a
t