{-# LANGUAGE BlockArguments #-}

module Elara.TypeInfer where

import Data.Generics.Product (HasType (typed))
import Data.Graph (SCC, flattenSCC)
import Data.Map qualified as Map
import Data.Set qualified as Set
import Effectful
import Effectful.Error.Static
import Effectful.Reader.Static (runReader)
import Effectful.State.Static.Local
import Effectful.Writer.Static.Local (runWriter)
import Elara.AST.Module qualified as NewModule
import Elara.AST.Name (LowerAlphaName, ModuleName, Name (..), NameLike (nameText), Qualified (..), ToName (..), TypeName, VarName, unqualified)
import Elara.AST.Phase (NoExtension (..))
import Elara.AST.PhaseCoerce (PhaseCoerce (..))
import Elara.AST.Phases.Kinded (KindedType)
import Elara.AST.Phases.Kinded qualified as NewK
import Elara.AST.Phases.Renamed (TypedLambdaParam (..))
import Elara.AST.Phases.Shunted (Shunted)
import Elara.AST.Phases.Shunted qualified as NewS
import Elara.AST.Phases.Typed (Typed, TypedDeclaration, TypedExpr, TypedExpr')
import Elara.AST.Phases.Typed qualified as NewT
import Elara.AST.Region (HasSourceRegion (..), Located (Located), SourceRegion, unlocated, withLocationOf)
import Elara.AST.Types qualified as New
import Elara.AST.VarRef
import Elara.Data.Kind (ElaraKind, KindVar)
import Elara.Data.Kind.Infer (KindInferError, inferKind, inferTypeKind, initialInferState, lookupKindVarMaybe)
import Elara.Data.Kind.Infer qualified as Kind
import Elara.Data.Pretty
import Elara.Data.Unique (Unique)
import Elara.Data.Unique.Effect
import Elara.Error (runErrorOrReport)
import Elara.Logging (StructuredDebug, debug, debugWith, debugWithResult, logDebug, logDebugWith)
import Elara.Query (Query (..), QueryType (..), SupportsQuery)
import Elara.Query.Effects
import Elara.Rules.Generic ()
import Elara.SCC.Type (SCCKey, sccKeyToSCC)
import Elara.Shunt ()
import Elara.Shunt.Error (ShuntError)
import Elara.TypeInfer.ConstraintGeneration
import Elara.TypeInfer.Context (emptyContextStack)
import Elara.TypeInfer.Convert (TypeConvertError, astTypeToGeneralisedInferType, astTypeToInferType, astTypeToInferTypeWithKind)
import Elara.TypeInfer.Environment (InferError, TypeEnvKey (..), TypeEnvironment, addType', emptyLocalTypeEnvironment, emptyTypeEnvironment)
import Elara.TypeInfer.Error (UnifyError (..))
import Elara.TypeInfer.Ftv (Fuv (..))
import Elara.TypeInfer.Generalise
import Elara.TypeInfer.Monad
import Elara.TypeInfer.Type (Constraint (..), Monotype (..), Polytype (..), Substitutable (..), Substitution (..), Type (..), TypeVariable (..), monotypeLoc, simpleEquality, typeLoc)
import Elara.TypeInfer.Unique (UniqueTyVar, makeUniqueTyVar)
import Optics (over, view)
import Relude.Extra (bimapF, fmapToSnd, secondF)
import Rock qualified

-- PhaseCoerce instances for Shunted → Typed (Exposing/Import type families are identical)
instance PhaseCoerce (NewModule.Exposing SourceRegion Shunted) (NewModule.Exposing SourceRegion Typed)

instance PhaseCoerce (NewModule.Exposition SourceRegion Shunted) (NewModule.Exposition SourceRegion Typed)

instance PhaseCoerce (NewModule.Import SourceRegion Shunted) (NewModule.Import SourceRegion Typed)

instance PhaseCoerce (NewModule.Import' SourceRegion Shunted) (NewModule.Import' SourceRegion Typed)

type InferPipelineEffects r =
    ( StructuredDebug :> r
    , State Kind.InferState :> r
    , UniqueGen :> r
    , Error (UnifyError SourceRegion) :> r
    , Error TypeConvertError :> r
    , Error KindInferError :> r
    , Infer SourceRegion r
    )

runGetTypeCheckedModuleQuery ::
    SupportsQuery QueryModuleByName Shunted =>
    ModuleName ->
    Eff
        ( ConsQueryEffects
            '[ Rock.Rock Elara.Query.Query
             ]
        )
        (NewModule.Module SourceRegion Typed)
runGetTypeCheckedModuleQuery :: SupportsQuery QueryModuleByName Shunted =>
ModuleName
-> Eff (ConsQueryEffects '[Rock Query]) (Module SourceRegion Typed)
runGetTypeCheckedModuleQuery ModuleName
mn = do
    shunted <- forall e (r :: [(* -> *) -> * -> *]) a.
(DiagnosticWriter (Doc AnsiStyle) :> r,
 Error SomeReportableError :> r, ReportableError e) =>
Eff (Error e : r) a -> Eff r a
runErrorOrReport @ShuntError (Eff
   (Error ShuntError : ConsQueryEffects '[Rock Query])
   (QueryReturnTypeOf QueryModuleByName Shunted)
 -> Eff
      (ConsQueryEffects '[Rock Query])
      (QueryReturnTypeOf QueryModuleByName Shunted))
-> Eff
     (Error ShuntError : ConsQueryEffects '[Rock Query])
     (QueryReturnTypeOf QueryModuleByName Shunted)
-> Eff
     (ConsQueryEffects '[Rock Query])
     (QueryReturnTypeOf QueryModuleByName Shunted)
forall a b. (a -> b) -> a -> b
$ Query
  (QueryEffectsOf QueryModuleByName Shunted)
  (QueryReturnTypeOf QueryModuleByName Shunted)
-> Eff
     (Error ShuntError : ConsQueryEffects '[Rock Query])
     (QueryReturnTypeOf QueryModuleByName Shunted)
forall (xs :: [(* -> *) -> * -> *]) (es :: [(* -> *) -> * -> *])
       (f :: [(* -> *) -> * -> *] -> * -> *) a.
(Subset xs es, Rock f :> es, HasCallStack,
 StructuredDebug :> xs) =>
f xs a -> Eff es a
Rock.fetch (Query
   (QueryEffectsOf QueryModuleByName Shunted)
   (QueryReturnTypeOf QueryModuleByName Shunted)
 -> Eff
      (Error ShuntError : ConsQueryEffects '[Rock Query])
      (QueryReturnTypeOf QueryModuleByName Shunted))
-> Query
     (QueryEffectsOf QueryModuleByName Shunted)
     (QueryReturnTypeOf QueryModuleByName Shunted)
-> Eff
     (Error ShuntError : ConsQueryEffects '[Rock Query])
     (QueryReturnTypeOf QueryModuleByName Shunted)
forall a b. (a -> b) -> a -> b
$ forall ast.
(Typeable ast, SupportsQuery QueryModuleByName ast,
 HasMinimumQueryEffects (QueryEffectsOf QueryModuleByName ast)) =>
ModuleName
-> Query
     (QueryEffectsOf QueryModuleByName ast)
     (QueryReturnTypeOf QueryModuleByName ast)
Elara.Query.ModuleByName @Shunted ModuleName
mn
    r <- runInferEffects $ evalState initialInferState (inferModule shunted)
    pure (fst r)

-- | Run the 'TypeOf' query to get the type of a term or data constructor
runTypeOfQuery ::
    forall loc.
    loc ~ SourceRegion =>
    (SupportsQuery QueryRequiredDeclarationByName Shunted, SupportsQuery QueryModuleByName Shunted) =>
    TypeEnvKey loc ->
    Eff
        ( ConsQueryEffects
            '[Rock.Rock Elara.Query.Query]
        )
        (Type loc)
runTypeOfQuery :: forall loc.
(loc ~ SourceRegion,
 SupportsQuery QueryRequiredDeclarationByName Shunted,
 SupportsQuery QueryModuleByName Shunted) =>
TypeEnvKey loc -> Eff (ConsQueryEffects '[Rock Query]) (Type loc)
runTypeOfQuery TypeEnvKey loc
key = forall e (r :: [(* -> *) -> * -> *]) a.
(DiagnosticWriter (Doc AnsiStyle) :> r,
 Error SomeReportableError :> r, ReportableError e) =>
Eff (Error e : r) a -> Eff r a
runErrorOrReport @(InferError loc) (Eff
   (Error (InferError loc) : ConsQueryEffects '[Rock Query])
   (Type loc)
 -> Eff (ConsQueryEffects '[Rock Query]) (Type loc))
-> Eff
     (Error (InferError loc) : ConsQueryEffects '[Rock Query])
     (Type loc)
-> Eff (ConsQueryEffects '[Rock Query]) (Type loc)
forall a b. (a -> b) -> a -> b
$
    forall e (r :: [(* -> *) -> * -> *]) a.
(DiagnosticWriter (Doc AnsiStyle) :> r,
 Error SomeReportableError :> r, ReportableError e) =>
Eff (Error e : r) a -> Eff r a
runErrorOrReport @(UnifyError loc) (Eff
   (Error (UnifyError loc)
      : Error (InferError loc) : ConsQueryEffects '[Rock Query])
   (Type loc)
 -> Eff
      (Error (InferError loc) : ConsQueryEffects '[Rock Query])
      (Type loc))
-> Eff
     (Error (UnifyError loc)
        : Error (InferError loc) : ConsQueryEffects '[Rock Query])
     (Type loc)
-> Eff
     (Error (InferError loc) : ConsQueryEffects '[Rock Query])
     (Type loc)
forall a b. (a -> b) -> a -> b
$
        forall e (r :: [(* -> *) -> * -> *]) a.
(DiagnosticWriter (Doc AnsiStyle) :> r,
 Error SomeReportableError :> r, ReportableError e) =>
Eff (Error e : r) a -> Eff r a
runErrorOrReport @KindInferError (Eff
   (Error KindInferError
      : Error (UnifyError loc) : Error (InferError loc)
      : ConsQueryEffects '[Rock Query])
   (Type loc)
 -> Eff
      (Error (UnifyError loc)
         : Error (InferError loc) : ConsQueryEffects '[Rock Query])
      (Type loc))
-> Eff
     (Error KindInferError
        : Error (UnifyError loc) : Error (InferError loc)
        : ConsQueryEffects '[Rock Query])
     (Type loc)
-> Eff
     (Error (UnifyError loc)
        : Error (InferError loc) : ConsQueryEffects '[Rock Query])
     (Type loc)
forall a b. (a -> b) -> a -> b
$
            forall e (r :: [(* -> *) -> * -> *]) a.
(DiagnosticWriter (Doc AnsiStyle) :> r,
 Error SomeReportableError :> r, ReportableError e) =>
Eff (Error e : r) a -> Eff r a
runErrorOrReport @TypeConvertError (Eff
   (Error TypeConvertError
      : Error KindInferError : Error (UnifyError loc)
      : Error (InferError loc) : ConsQueryEffects '[Rock Query])
   (Type loc)
 -> Eff
      (Error KindInferError
         : Error (UnifyError loc) : Error (InferError loc)
         : ConsQueryEffects '[Rock Query])
      (Type loc))
-> Eff
     (Error TypeConvertError
        : Error KindInferError : Error (UnifyError loc)
        : Error (InferError loc) : ConsQueryEffects '[Rock Query])
     (Type loc)
-> Eff
     (Error KindInferError
        : Error (UnifyError loc) : Error (InferError loc)
        : ConsQueryEffects '[Rock Query])
     (Type loc)
forall a b. (a -> b) -> a -> b
$
                LocalTypeEnvironment SourceRegion
-> Eff
     (State (LocalTypeEnvironment SourceRegion)
        : Error TypeConvertError : Error KindInferError
        : Error (UnifyError loc) : Error (InferError loc)
        : ConsQueryEffects '[Rock Query])
     (Type loc)
-> Eff
     (Error TypeConvertError
        : Error KindInferError : Error (UnifyError loc)
        : Error (InferError loc) : ConsQueryEffects '[Rock Query])
     (Type loc)
forall s (es :: [(* -> *) -> * -> *]) a.
HasCallStack =>
s -> Eff (State s : es) a -> Eff es a
evalState LocalTypeEnvironment SourceRegion
forall loc. LocalTypeEnvironment loc
emptyLocalTypeEnvironment (Eff
   (State (LocalTypeEnvironment SourceRegion)
      : Error TypeConvertError : Error KindInferError
      : Error (UnifyError loc) : Error (InferError loc)
      : ConsQueryEffects '[Rock Query])
   (Type loc)
 -> Eff
      (Error TypeConvertError
         : Error KindInferError : Error (UnifyError loc)
         : Error (InferError loc) : ConsQueryEffects '[Rock Query])
      (Type loc))
-> Eff
     (State (LocalTypeEnvironment SourceRegion)
        : Error TypeConvertError : Error KindInferError
        : Error (UnifyError loc) : Error (InferError loc)
        : ConsQueryEffects '[Rock Query])
     (Type loc)
-> Eff
     (Error TypeConvertError
        : Error KindInferError : Error (UnifyError loc)
        : Error (InferError loc) : ConsQueryEffects '[Rock Query])
     (Type loc)
forall a b. (a -> b) -> a -> b
$
                    InferState
-> Eff
     (State InferState
        : State (LocalTypeEnvironment SourceRegion)
        : Error TypeConvertError : Error KindInferError
        : Error (UnifyError loc) : Error (InferError loc)
        : ConsQueryEffects '[Rock Query])
     (Type loc)
-> Eff
     (State (LocalTypeEnvironment SourceRegion)
        : Error TypeConvertError : Error KindInferError
        : Error (UnifyError loc) : Error (InferError loc)
        : ConsQueryEffects '[Rock Query])
     (Type loc)
forall s (es :: [(* -> *) -> * -> *]) a.
HasCallStack =>
s -> Eff (State s : es) a -> Eff es a
evalState InferState
initialInferState (Eff
   (State InferState
      : State (LocalTypeEnvironment SourceRegion)
      : Error TypeConvertError : Error KindInferError
      : Error (UnifyError loc) : Error (InferError loc)
      : ConsQueryEffects '[Rock Query])
   (Type loc)
 -> Eff
      (State (LocalTypeEnvironment SourceRegion)
         : Error TypeConvertError : Error KindInferError
         : Error (UnifyError loc) : Error (InferError loc)
         : ConsQueryEffects '[Rock Query])
      (Type loc))
-> Eff
     (State InferState
        : State (LocalTypeEnvironment SourceRegion)
        : Error TypeConvertError : Error KindInferError
        : Error (UnifyError loc) : Error (InferError loc)
        : ConsQueryEffects '[Rock Query])
     (Type loc)
-> Eff
     (State (LocalTypeEnvironment SourceRegion)
        : Error TypeConvertError : Error KindInferError
        : Error (UnifyError loc) : Error (InferError loc)
        : ConsQueryEffects '[Rock Query])
     (Type loc)
forall a b. (a -> b) -> a -> b
$
                        TypeEnvironment SourceRegion
-> Eff
     (State (TypeEnvironment SourceRegion)
        : State InferState : State (LocalTypeEnvironment SourceRegion)
        : Error TypeConvertError : Error KindInferError
        : Error (UnifyError loc) : Error (InferError loc)
        : ConsQueryEffects '[Rock Query])
     (Type loc)
-> Eff
     (State InferState
        : State (LocalTypeEnvironment SourceRegion)
        : Error TypeConvertError : Error KindInferError
        : Error (UnifyError loc) : Error (InferError loc)
        : ConsQueryEffects '[Rock Query])
     (Type loc)
forall s (es :: [(* -> *) -> * -> *]) a.
HasCallStack =>
s -> Eff (State s : es) a -> Eff es a
evalState TypeEnvironment SourceRegion
forall loc. TypeEnvironment loc
emptyTypeEnvironment (Eff
   (State (TypeEnvironment SourceRegion)
      : State InferState : State (LocalTypeEnvironment SourceRegion)
      : Error TypeConvertError : Error KindInferError
      : Error (UnifyError loc) : Error (InferError loc)
      : ConsQueryEffects '[Rock Query])
   (Type loc)
 -> Eff
      (State InferState
         : State (LocalTypeEnvironment SourceRegion)
         : Error TypeConvertError : Error KindInferError
         : Error (UnifyError loc) : Error (InferError loc)
         : ConsQueryEffects '[Rock Query])
      (Type loc))
-> Eff
     (State (TypeEnvironment SourceRegion)
        : State InferState : State (LocalTypeEnvironment SourceRegion)
        : Error TypeConvertError : Error KindInferError
        : Error (UnifyError loc) : Error (InferError loc)
        : ConsQueryEffects '[Rock Query])
     (Type loc)
-> Eff
     (State InferState
        : State (LocalTypeEnvironment SourceRegion)
        : Error TypeConvertError : Error KindInferError
        : Error (UnifyError loc) : Error (InferError loc)
        : ConsQueryEffects '[Rock Query])
     (Type loc)
forall a b. (a -> b) -> a -> b
$
                            ContextStack
-> Eff
     (Reader ContextStack
        : State (TypeEnvironment SourceRegion) : State InferState
        : State (LocalTypeEnvironment SourceRegion)
        : Error TypeConvertError : Error KindInferError
        : Error (UnifyError loc) : Error (InferError loc)
        : ConsQueryEffects '[Rock Query])
     (Type loc)
-> Eff
     (State (TypeEnvironment SourceRegion)
        : State InferState : State (LocalTypeEnvironment SourceRegion)
        : Error TypeConvertError : Error KindInferError
        : Error (UnifyError loc) : Error (InferError loc)
        : ConsQueryEffects '[Rock Query])
     (Type loc)
forall r (es :: [(* -> *) -> * -> *]) a.
HasCallStack =>
r -> Eff (Reader r : es) a -> Eff es a
runReader ContextStack
emptyContextStack (Eff
   (Reader ContextStack
      : State (TypeEnvironment SourceRegion) : State InferState
      : State (LocalTypeEnvironment SourceRegion)
      : Error TypeConvertError : Error KindInferError
      : Error (UnifyError loc) : Error (InferError loc)
      : ConsQueryEffects '[Rock Query])
   (Type loc)
 -> Eff
      (State (TypeEnvironment SourceRegion)
         : State InferState : State (LocalTypeEnvironment SourceRegion)
         : Error TypeConvertError : Error KindInferError
         : Error (UnifyError loc) : Error (InferError loc)
         : ConsQueryEffects '[Rock Query])
      (Type loc))
-> Eff
     (Reader ContextStack
        : State (TypeEnvironment SourceRegion) : State InferState
        : State (LocalTypeEnvironment SourceRegion)
        : Error TypeConvertError : Error KindInferError
        : Error (UnifyError loc) : Error (InferError loc)
        : ConsQueryEffects '[Rock Query])
     (Type loc)
-> Eff
     (State (TypeEnvironment SourceRegion)
        : State InferState : State (LocalTypeEnvironment SourceRegion)
        : Error TypeConvertError : Error KindInferError
        : Error (UnifyError loc) : Error (InferError loc)
        : ConsQueryEffects '[Rock Query])
     (Type loc)
forall a b. (a -> b) -> a -> b
$
                                case TypeEnvKey loc
key of
                                    TermVarKey Qualified VarName
varName -> Doc AnsiStyle
-> Eff
     (Reader ContextStack
        : State (TypeEnvironment SourceRegion) : State InferState
        : State (LocalTypeEnvironment SourceRegion)
        : Error TypeConvertError : Error KindInferError
        : Error (UnifyError loc) : Error (InferError loc)
        : ConsQueryEffects '[Rock Query])
     (Type loc)
-> Eff
     (Reader ContextStack
        : State (TypeEnvironment SourceRegion) : State InferState
        : State (LocalTypeEnvironment SourceRegion)
        : Error TypeConvertError : Error KindInferError
        : Error (UnifyError loc) : Error (InferError loc)
        : ConsQueryEffects '[Rock Query])
     (Type loc)
forall (r :: [(* -> *) -> * -> *]) a.
(HasCallStack, StructuredDebug :> r) =>
Doc AnsiStyle -> Eff r a -> Eff r a
logDebugWith (Doc AnsiStyle
"TypeOf: " Doc AnsiStyle -> Doc AnsiStyle -> Doc AnsiStyle
forall a. Semigroup a => a -> a -> a
<> Qualified VarName -> Doc AnsiStyle
forall a. Pretty a => a -> Doc AnsiStyle
pretty Qualified VarName
varName) (Eff
   (Reader ContextStack
      : State (TypeEnvironment SourceRegion) : State InferState
      : State (LocalTypeEnvironment SourceRegion)
      : Error TypeConvertError : Error KindInferError
      : Error (UnifyError loc) : Error (InferError loc)
      : ConsQueryEffects '[Rock Query])
   (Type loc)
 -> Eff
      (Reader ContextStack
         : State (TypeEnvironment SourceRegion) : State InferState
         : State (LocalTypeEnvironment SourceRegion)
         : Error TypeConvertError : Error KindInferError
         : Error (UnifyError loc) : Error (InferError loc)
         : ConsQueryEffects '[Rock Query])
      (Type loc))
-> Eff
     (Reader ContextStack
        : State (TypeEnvironment SourceRegion) : State InferState
        : State (LocalTypeEnvironment SourceRegion)
        : Error TypeConvertError : Error KindInferError
        : Error (UnifyError loc) : Error (InferError loc)
        : ConsQueryEffects '[Rock Query])
     (Type loc)
-> Eff
     (Reader ContextStack
        : State (TypeEnvironment SourceRegion) : State InferState
        : State (LocalTypeEnvironment SourceRegion)
        : Error TypeConvertError : Error KindInferError
        : Error (UnifyError loc) : Error (InferError loc)
        : ConsQueryEffects '[Rock Query])
     (Type loc)
forall a b. (a -> b) -> a -> b
$ do
                                        sccs <- Query (Rock Query : ConsQueryEffects '[]) [SCC (Qualified VarName)]
-> Eff
     (Reader ContextStack
        : State (TypeEnvironment SourceRegion) : State InferState
        : State (LocalTypeEnvironment SourceRegion)
        : Error TypeConvertError : Error KindInferError
        : Error (UnifyError loc) : Error (InferError loc)
        : ConsQueryEffects '[Rock Query])
     [SCC (Qualified VarName)]
forall (xs :: [(* -> *) -> * -> *]) (es :: [(* -> *) -> * -> *])
       (f :: [(* -> *) -> * -> *] -> * -> *) a.
(Subset xs es, Rock f :> es, HasCallStack,
 StructuredDebug :> xs) =>
f xs a -> Eff es a
Rock.fetch (Query
   (Rock Query : ConsQueryEffects '[]) [SCC (Qualified VarName)]
 -> Eff
      (Reader ContextStack
         : State (TypeEnvironment SourceRegion) : State InferState
         : State (LocalTypeEnvironment SourceRegion)
         : Error TypeConvertError : Error KindInferError
         : Error (UnifyError loc) : Error (InferError loc)
         : ConsQueryEffects '[Rock Query])
      [SCC (Qualified VarName)])
-> Query
     (Rock Query : ConsQueryEffects '[]) [SCC (Qualified VarName)]
-> Eff
     (Reader ContextStack
        : State (TypeEnvironment SourceRegion) : State InferState
        : State (LocalTypeEnvironment SourceRegion)
        : Error TypeConvertError : Error KindInferError
        : Error (UnifyError loc) : Error (InferError loc)
        : ConsQueryEffects '[Rock Query])
     [SCC (Qualified VarName)]
forall a b. (a -> b) -> a -> b
$ Qualified VarName
-> Query
     (Rock Query : ConsQueryEffects '[]) [SCC (Qualified VarName)]
GetSCCsOf Qualified VarName
varName
                                        logDebug $ "SCCs for " <> pretty varName <> ": " <> pretty (fmap flattenSCC sccs)
                                        -- Infer dependencies first to populate the environment
                                        for_ sccs seedSCC
                                        for_ sccs inferSCC
                                        -- Read from the environment (now populated) without re-querying
                                        lookupType (TermVarKey varName)
                                    DataConKey Qualified TypeName
con -> do
                                        ModuleName
-> Eff
     (Reader ContextStack
        : State (TypeEnvironment SourceRegion) : State InferState
        : State (LocalTypeEnvironment SourceRegion)
        : Error TypeConvertError : Error KindInferError
        : Error (UnifyError loc) : Error (InferError loc)
        : ConsQueryEffects '[Rock Query])
     ()
forall (r :: [(* -> *) -> * -> *]).
(SupportsQuery QueryModuleByName Shunted, HasCallStack,
 Rock Query :> r, DiagnosticWriter (Doc AnsiStyle) :> r,
 Error SomeReportableError :> r, Error KindInferError :> r,
 Error TypeConvertError :> r,
 State (TypeEnvironment SourceRegion) :> r, State InferState :> r,
 Concurrent :> r, UniqueGen :> r, FileSystem :> r,
 StructuredDebug :> r) =>
ModuleName -> Eff r ()
seedConstructorsFor (Qualified TypeName -> ModuleName
forall name. Qualified name -> ModuleName
qualifier Qualified TypeName
con)
                                        -- Read from the environment (now populated) without re-querying
                                        TypeEnvKey loc
-> Eff
     (Reader ContextStack
        : State (TypeEnvironment SourceRegion) : State InferState
        : State (LocalTypeEnvironment SourceRegion)
        : Error TypeConvertError : Error KindInferError
        : Error (UnifyError loc) : Error (InferError loc)
        : ConsQueryEffects '[Rock Query])
     (Type loc)
forall (r :: [(* -> *) -> * -> *]) loc.
(StructuredDebug :> r, QueryEffects r, loc ~ SourceRegion,
 Rock Query :> r, State (TypeEnvironment loc) :> r) =>
TypeEnvKey loc -> Eff r (Type loc)
lookupType (Qualified TypeName -> TypeEnvKey loc
forall {k} (loc :: k). Qualified TypeName -> TypeEnvKey loc
DataConKey Qualified TypeName
con)

runKindOfQuery :: SupportsQuery QueryModuleByName Shunted => Qualified TypeName -> Eff (ConsQueryEffects (Rock.Rock Query : r)) (Maybe KindVar)
runKindOfQuery :: forall (r :: [(* -> *) -> * -> *]).
SupportsQuery QueryModuleByName Shunted =>
Qualified TypeName
-> Eff (ConsQueryEffects (Rock Query : r)) (Maybe KindVar)
runKindOfQuery Qualified TypeName
qtn = ((Maybe KindVar, Constraint SourceRegion) -> Maybe KindVar)
-> Eff
     (ConsQueryEffects (Rock Query : r))
     (Maybe KindVar, Constraint SourceRegion)
-> Eff (ConsQueryEffects (Rock Query : r)) (Maybe KindVar)
forall a b.
(a -> b)
-> Eff (ConsQueryEffects (Rock Query : r)) a
-> Eff (ConsQueryEffects (Rock Query : r)) b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Maybe KindVar, Constraint SourceRegion) -> Maybe KindVar
forall a b. (a, b) -> a
fst (Eff
   (ConsQueryEffects (Rock Query : r))
   (Maybe KindVar, Constraint SourceRegion)
 -> Eff (ConsQueryEffects (Rock Query : r)) (Maybe KindVar))
-> Eff
     (ConsQueryEffects (Rock Query : r))
     (Maybe KindVar, Constraint SourceRegion)
-> Eff (ConsQueryEffects (Rock Query : r)) (Maybe KindVar)
forall a b. (a -> b) -> a -> b
$ Eff
  (InferEffectsCons
     SourceRegion
     (Error (UnifyError SourceRegion)
        : Error KindInferError : Error TypeConvertError
        : ConsQueryEffects (Rock Query : r)))
  (Maybe KindVar)
-> Eff
     (ConsQueryEffects (Rock Query : r))
     (Maybe KindVar, Constraint SourceRegion)
forall (r :: [(* -> *) -> * -> *]) a loc.
(Pretty loc, QueryEffects r, Rock Query :> r, Eq loc,
 loc ~ SourceRegion) =>
Eff
  (InferEffectsCons
     loc
     (Error (UnifyError loc)
        : Error KindInferError : Error TypeConvertError : r))
  a
-> Eff r (a, Constraint loc)
runInferEffects (Eff
   (InferEffectsCons
      SourceRegion
      (Error (UnifyError SourceRegion)
         : Error KindInferError : Error TypeConvertError
         : ConsQueryEffects (Rock Query : r)))
   (Maybe KindVar)
 -> Eff
      (ConsQueryEffects (Rock Query : r))
      (Maybe KindVar, Constraint SourceRegion))
-> Eff
     (InferEffectsCons
        SourceRegion
        (Error (UnifyError SourceRegion)
           : Error KindInferError : Error TypeConvertError
           : ConsQueryEffects (Rock Query : r)))
     (Maybe KindVar)
-> Eff
     (ConsQueryEffects (Rock Query : r))
     (Maybe KindVar, Constraint SourceRegion)
forall a b. (a -> b) -> a -> b
$ InferState
-> Eff
     (State InferState
        : InferEffectsCons
            SourceRegion
            (Error (UnifyError SourceRegion)
               : Error KindInferError : Error TypeConvertError
               : ConsQueryEffects (Rock Query : r)))
     (Maybe KindVar)
-> Eff
     (InferEffectsCons
        SourceRegion
        (Error (UnifyError SourceRegion)
           : Error KindInferError : Error TypeConvertError
           : ConsQueryEffects (Rock Query : r)))
     (Maybe KindVar)
forall s (es :: [(* -> *) -> * -> *]) a.
HasCallStack =>
s -> Eff (State s : es) a -> Eff es a
evalState InferState
initialInferState (Eff
   (State InferState
      : InferEffectsCons
          SourceRegion
          (Error (UnifyError SourceRegion)
             : Error KindInferError : Error TypeConvertError
             : ConsQueryEffects (Rock Query : r)))
   (Maybe KindVar)
 -> Eff
      (InferEffectsCons
         SourceRegion
         (Error (UnifyError SourceRegion)
            : Error KindInferError : Error TypeConvertError
            : ConsQueryEffects (Rock Query : r)))
      (Maybe KindVar))
-> Eff
     (State InferState
        : InferEffectsCons
            SourceRegion
            (Error (UnifyError SourceRegion)
               : Error KindInferError : Error TypeConvertError
               : ConsQueryEffects (Rock Query : r)))
     (Maybe KindVar)
-> Eff
     (InferEffectsCons
        SourceRegion
        (Error (UnifyError SourceRegion)
           : Error KindInferError : Error TypeConvertError
           : ConsQueryEffects (Rock Query : r)))
     (Maybe KindVar)
forall a b. (a -> b) -> a -> b
$ do
    Doc AnsiStyle
-> Eff
     (State InferState
        : InferEffectsCons
            SourceRegion
            (Error (UnifyError SourceRegion)
               : Error KindInferError : Error TypeConvertError
               : ConsQueryEffects (Rock Query : r)))
     ()
forall (r :: [(* -> *) -> * -> *]).
(HasCallStack, StructuredDebug :> r) =>
Doc AnsiStyle -> Eff r ()
logDebug (Doc AnsiStyle
 -> Eff
      (State InferState
         : InferEffectsCons
             SourceRegion
             (Error (UnifyError SourceRegion)
                : Error KindInferError : Error TypeConvertError
                : ConsQueryEffects (Rock Query : r)))
      ())
-> Doc AnsiStyle
-> Eff
     (State InferState
        : InferEffectsCons
            SourceRegion
            (Error (UnifyError SourceRegion)
               : Error KindInferError : Error TypeConvertError
               : ConsQueryEffects (Rock Query : r)))
     ()
forall a b. (a -> b) -> a -> b
$ Doc AnsiStyle
"runKindOfQuery: " Doc AnsiStyle -> Doc AnsiStyle -> Doc AnsiStyle
forall a. Semigroup a => a -> a -> a
<> Qualified TypeName -> Doc AnsiStyle
forall a. Pretty a => a -> Doc AnsiStyle
pretty Qualified TypeName
qtn
    -- First, try to look up the kind variable directly
    -- it might be a primitive type or already inferred
    Either (Qualified TypeName) (Unique LowerAlphaName)
-> Eff
     (State InferState
        : InferEffectsCons
            SourceRegion
            (Error (UnifyError SourceRegion)
               : Error KindInferError : Error TypeConvertError
               : ConsQueryEffects (Rock Query : r)))
     (Maybe KindVar)
forall (r :: [(* -> *) -> * -> *]).
KindInfer r =>
Either (Qualified TypeName) (Unique LowerAlphaName)
-> Eff r (Maybe KindVar)
lookupKindVarMaybe (Qualified TypeName
-> Either (Qualified TypeName) (Unique LowerAlphaName)
forall a b. a -> Either a b
Left Qualified TypeName
qtn) Eff
  (State InferState
     : InferEffectsCons
         SourceRegion
         (Error (UnifyError SourceRegion)
            : Error KindInferError : Error TypeConvertError
            : ConsQueryEffects (Rock Query : r)))
  (Maybe KindVar)
-> (Maybe KindVar
    -> Eff
         (State InferState
            : InferEffectsCons
                SourceRegion
                (Error (UnifyError SourceRegion)
                   : Error KindInferError : Error TypeConvertError
                   : ConsQueryEffects (Rock Query : r)))
         (Maybe KindVar))
-> Eff
     (State InferState
        : InferEffectsCons
            SourceRegion
            (Error (UnifyError SourceRegion)
               : Error KindInferError : Error TypeConvertError
               : ConsQueryEffects (Rock Query : r)))
     (Maybe KindVar)
forall a b.
Eff
  (State InferState
     : InferEffectsCons
         SourceRegion
         (Error (UnifyError SourceRegion)
            : Error KindInferError : Error TypeConvertError
            : ConsQueryEffects (Rock Query : r)))
  a
-> (a
    -> Eff
         (State InferState
            : InferEffectsCons
                SourceRegion
                (Error (UnifyError SourceRegion)
                   : Error KindInferError : Error TypeConvertError
                   : ConsQueryEffects (Rock Query : r)))
         b)
-> Eff
     (State InferState
        : InferEffectsCons
            SourceRegion
            (Error (UnifyError SourceRegion)
               : Error KindInferError : Error TypeConvertError
               : ConsQueryEffects (Rock Query : r)))
     b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
        Just KindVar
kindVar -> Maybe KindVar
-> Eff
     (State InferState
        : InferEffectsCons
            SourceRegion
            (Error (UnifyError SourceRegion)
               : Error KindInferError : Error TypeConvertError
               : ConsQueryEffects (Rock Query : r)))
     (Maybe KindVar)
forall a.
a
-> Eff
     (State InferState
        : InferEffectsCons
            SourceRegion
            (Error (UnifyError SourceRegion)
               : Error KindInferError : Error TypeConvertError
               : ConsQueryEffects (Rock Query : r)))
     a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (KindVar -> Maybe KindVar
forall a. a -> Maybe a
Just KindVar
kindVar)
        Maybe KindVar
Nothing -> do
            Doc AnsiStyle
-> Eff
     (State InferState
        : InferEffectsCons
            SourceRegion
            (Error (UnifyError SourceRegion)
               : Error KindInferError : Error TypeConvertError
               : ConsQueryEffects (Rock Query : r)))
     ()
forall (r :: [(* -> *) -> * -> *]).
(HasCallStack, StructuredDebug :> r) =>
Doc AnsiStyle -> Eff r ()
logDebug (Doc AnsiStyle
 -> Eff
      (State InferState
         : InferEffectsCons
             SourceRegion
             (Error (UnifyError SourceRegion)
                : Error KindInferError : Error TypeConvertError
                : ConsQueryEffects (Rock Query : r)))
      ())
-> Doc AnsiStyle
-> Eff
     (State InferState
        : InferEffectsCons
            SourceRegion
            (Error (UnifyError SourceRegion)
               : Error KindInferError : Error TypeConvertError
               : ConsQueryEffects (Rock Query : r)))
     ()
forall a b. (a -> b) -> a -> b
$ Doc AnsiStyle
"Kind not found for " Doc AnsiStyle -> Doc AnsiStyle -> Doc AnsiStyle
forall a. Semigroup a => a -> a -> a
<> Qualified TypeName -> Doc AnsiStyle
forall a. Pretty a => a -> Doc AnsiStyle
pretty Qualified TypeName
qtn Doc AnsiStyle -> Doc AnsiStyle -> Doc AnsiStyle
forall a. Semigroup a => a -> a -> a
<> Doc AnsiStyle
", seeding whole module"
            -- if we can't find it, seed the whole module and try again
            ModuleName
-> Eff
     (State InferState
        : InferEffectsCons
            SourceRegion
            (Error (UnifyError SourceRegion)
               : Error KindInferError : Error TypeConvertError
               : ConsQueryEffects (Rock Query : r)))
     ()
forall (r :: [(* -> *) -> * -> *]).
(SupportsQuery QueryModuleByName Shunted, HasCallStack,
 Rock Query :> r, DiagnosticWriter (Doc AnsiStyle) :> r,
 Error SomeReportableError :> r, Error KindInferError :> r,
 Error TypeConvertError :> r,
 State (TypeEnvironment SourceRegion) :> r, State InferState :> r,
 Concurrent :> r, UniqueGen :> r, FileSystem :> r,
 StructuredDebug :> r) =>
ModuleName -> Eff r ()
seedConstructorsFor (Qualified TypeName -> ModuleName
forall name. Qualified name -> ModuleName
qualifier Qualified TypeName
qtn)

            -- in theory it should be here now...
            Either (Qualified TypeName) (Unique LowerAlphaName)
-> Eff
     (State InferState
        : InferEffectsCons
            SourceRegion
            (Error (UnifyError SourceRegion)
               : Error KindInferError : Error TypeConvertError
               : ConsQueryEffects (Rock Query : r)))
     (Maybe KindVar)
forall (r :: [(* -> *) -> * -> *]).
KindInfer r =>
Either (Qualified TypeName) (Unique LowerAlphaName)
-> Eff r (Maybe KindVar)
lookupKindVarMaybe (Qualified TypeName
-> Either (Qualified TypeName) (Unique LowerAlphaName)
forall a b. a -> Either a b
Left Qualified TypeName
qtn)

runGetTypeAliasQuery ::
    forall r.
    SupportsQuery QueryModuleByName Shunted =>
    Qualified TypeName ->
    Eff (ConsQueryEffects (Rock.Rock Query : r)) (Maybe ([UniqueTyVar], Type SourceRegion))
runGetTypeAliasQuery :: forall (r :: [(* -> *) -> * -> *]).
SupportsQuery QueryModuleByName Shunted =>
Qualified TypeName
-> Eff
     (ConsQueryEffects (Rock Query : r))
     (Maybe ([UniqueTyVar], Type SourceRegion))
runGetTypeAliasQuery Qualified TypeName
name = do
    let modName :: ModuleName
modName = Qualified TypeName -> ModuleName
forall name. Qualified name -> ModuleName
qualifier Qualified TypeName
name
    mod <- forall e (r :: [(* -> *) -> * -> *]) a.
(DiagnosticWriter (Doc AnsiStyle) :> r,
 Error SomeReportableError :> r, ReportableError e) =>
Eff (Error e : r) a -> Eff r a
runErrorOrReport @ShuntError (Eff
   (Error ShuntError : ConsQueryEffects (Rock Query : r))
   (QueryReturnTypeOf QueryModuleByName Shunted)
 -> Eff
      (ConsQueryEffects (Rock Query : r))
      (QueryReturnTypeOf QueryModuleByName Shunted))
-> Eff
     (Error ShuntError : ConsQueryEffects (Rock Query : r))
     (QueryReturnTypeOf QueryModuleByName Shunted)
-> Eff
     (ConsQueryEffects (Rock Query : r))
     (QueryReturnTypeOf QueryModuleByName Shunted)
forall a b. (a -> b) -> a -> b
$ Query
  (QueryEffectsOf QueryModuleByName Shunted)
  (QueryReturnTypeOf QueryModuleByName Shunted)
-> Eff
     (Error ShuntError : ConsQueryEffects (Rock Query : r))
     (QueryReturnTypeOf QueryModuleByName Shunted)
forall (xs :: [(* -> *) -> * -> *]) (es :: [(* -> *) -> * -> *])
       (f :: [(* -> *) -> * -> *] -> * -> *) a.
(Subset xs es, Rock f :> es, HasCallStack,
 StructuredDebug :> xs) =>
f xs a -> Eff es a
Rock.fetch (Query
   (QueryEffectsOf QueryModuleByName Shunted)
   (QueryReturnTypeOf QueryModuleByName Shunted)
 -> Eff
      (Error ShuntError : ConsQueryEffects (Rock Query : r))
      (QueryReturnTypeOf QueryModuleByName Shunted))
-> Query
     (QueryEffectsOf QueryModuleByName Shunted)
     (QueryReturnTypeOf QueryModuleByName Shunted)
-> Eff
     (Error ShuntError : ConsQueryEffects (Rock Query : r))
     (QueryReturnTypeOf QueryModuleByName Shunted)
forall a b. (a -> b) -> a -> b
$ forall ast.
(Typeable ast, SupportsQuery QueryModuleByName ast,
 HasMinimumQueryEffects (QueryEffectsOf QueryModuleByName ast)) =>
ModuleName
-> Query
     (QueryEffectsOf QueryModuleByName ast)
     (QueryReturnTypeOf QueryModuleByName ast)
Elara.Query.ModuleByName @Shunted ModuleName
modName

    let NewModule.Module _ m' = mod
    let targetTypeName = Qualified TypeName
name Qualified TypeName
-> Optic' A_Lens NoIx (Qualified TypeName) TypeName -> TypeName
forall k s (is :: IxList) a.
Is k A_Getter =>
s -> Optic' k is s a -> a
^. Optic' A_Lens NoIx (Qualified TypeName) TypeName
forall name. Lens' (Qualified name) name
unqualified
    let found = (Declaration SourceRegion Shunted -> Bool)
-> [Declaration SourceRegion Shunted]
-> Maybe (Declaration SourceRegion Shunted)
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Maybe a
find (TypeName -> Declaration SourceRegion Shunted -> Bool
matchesTypeName TypeName
targetTypeName) Module' SourceRegion Shunted
m'.moduleDeclarations

    case found of
        Just (New.Declaration SourceRegion
_ (New.Declaration' Locate SourceRegion ModuleName
_ (New.DeclarationBody SourceRegion
_ DeclarationBody' SourceRegion Shunted
body'))) -> do
            case DeclarationBody' SourceRegion Shunted
body' of
                New.TypeDeclarationBody TopTypeBinder Shunted SourceRegion
_ [TypeVariable Shunted SourceRegion]
typeVars (New.Alias Type SourceRegion Shunted
body) Maybe (Type SourceRegion Shunted)
_ TypeDeclMetadata Shunted SourceRegion
NoExtension
NoExtension [Annotation SourceRegion Shunted]
_ -> do
                    res <- Eff
  (InferEffectsCons
     SourceRegion
     (Error (UnifyError SourceRegion)
        : Error KindInferError : Error TypeConvertError
        : ConsQueryEffects (Rock Query : r)))
  (Maybe ([UniqueTyVar], Type SourceRegion))
-> Eff
     (ConsQueryEffects (Rock Query : r))
     (Maybe ([UniqueTyVar], Type SourceRegion), Constraint SourceRegion)
forall (r :: [(* -> *) -> * -> *]) a loc.
(Pretty loc, QueryEffects r, Rock Query :> r, Eq loc,
 loc ~ SourceRegion) =>
Eff
  (InferEffectsCons
     loc
     (Error (UnifyError loc)
        : Error KindInferError : Error TypeConvertError : r))
  a
-> Eff r (a, Constraint loc)
runInferEffects (Eff
   (InferEffectsCons
      SourceRegion
      (Error (UnifyError SourceRegion)
         : Error KindInferError : Error TypeConvertError
         : ConsQueryEffects (Rock Query : r)))
   (Maybe ([UniqueTyVar], Type SourceRegion))
 -> Eff
      (ConsQueryEffects (Rock Query : r))
      (Maybe ([UniqueTyVar], Type SourceRegion),
       Constraint SourceRegion))
-> Eff
     (InferEffectsCons
        SourceRegion
        (Error (UnifyError SourceRegion)
           : Error KindInferError : Error TypeConvertError
           : ConsQueryEffects (Rock Query : r)))
     (Maybe ([UniqueTyVar], Type SourceRegion))
-> Eff
     (ConsQueryEffects (Rock Query : r))
     (Maybe ([UniqueTyVar], Type SourceRegion), Constraint SourceRegion)
forall a b. (a -> b) -> a -> b
$ InferState
-> Eff
     (State InferState
        : InferEffectsCons
            SourceRegion
            (Error (UnifyError SourceRegion)
               : Error KindInferError : Error TypeConvertError
               : ConsQueryEffects (Rock Query : r)))
     (Maybe ([UniqueTyVar], Type SourceRegion))
-> Eff
     (InferEffectsCons
        SourceRegion
        (Error (UnifyError SourceRegion)
           : Error KindInferError : Error TypeConvertError
           : ConsQueryEffects (Rock Query : r)))
     (Maybe ([UniqueTyVar], Type SourceRegion))
forall s (es :: [(* -> *) -> * -> *]) a.
HasCallStack =>
s -> Eff (State s : es) a -> Eff es a
evalState InferState
initialInferState (Eff
   (State InferState
      : InferEffectsCons
          SourceRegion
          (Error (UnifyError SourceRegion)
             : Error KindInferError : Error TypeConvertError
             : ConsQueryEffects (Rock Query : r)))
   (Maybe ([UniqueTyVar], Type SourceRegion))
 -> Eff
      (InferEffectsCons
         SourceRegion
         (Error (UnifyError SourceRegion)
            : Error KindInferError : Error TypeConvertError
            : ConsQueryEffects (Rock Query : r)))
      (Maybe ([UniqueTyVar], Type SourceRegion)))
-> Eff
     (State InferState
        : InferEffectsCons
            SourceRegion
            (Error (UnifyError SourceRegion)
               : Error KindInferError : Error TypeConvertError
               : ConsQueryEffects (Rock Query : r)))
     (Maybe ([UniqueTyVar], Type SourceRegion))
-> Eff
     (InferEffectsCons
        SourceRegion
        (Error (UnifyError SourceRegion)
           : Error KindInferError : Error TypeConvertError
           : ConsQueryEffects (Rock Query : r)))
     (Maybe ([UniqueTyVar], Type SourceRegion))
forall a b. (a -> b) -> a -> b
$ do
                        -- infer the kind of the alias
                        (_, typedDeclBody) <- Qualified TypeName
-> [Located (Unique LowerAlphaName)]
-> TypeDeclaration SourceRegion Shunted
-> Eff
     (State InferState
        : InferEffectsCons
            SourceRegion
            (Error (UnifyError SourceRegion)
               : Error KindInferError : Error TypeConvertError
               : ConsQueryEffects (Rock Query : r)))
     (ElaraKind, KindedTypeDeclaration)
forall (r :: [(* -> *) -> * -> *]).
(HasCallStack, State InferState :> r, Error KindInferError :> r,
 Error SomeReportableError :> r,
 DiagnosticWriter (Doc AnsiStyle) :> r, Rock Query :> r,
 StructuredDebug :> r, UniqueGen :> r, FileSystem :> r,
 Concurrent :> r) =>
Qualified TypeName
-> [Located (Unique LowerAlphaName)]
-> TypeDeclaration SourceRegion Shunted
-> Eff r (ElaraKind, KindedTypeDeclaration)
inferKind Qualified TypeName
name [Located (Unique LowerAlphaName)]
[TypeVariable Shunted SourceRegion]
typeVars (Type SourceRegion Shunted -> TypeDeclaration SourceRegion Shunted
forall {k} loc (p :: k). Type loc p -> TypeDeclaration loc p
New.Alias Type SourceRegion Shunted
body)

                        case typedDeclBody of
                            New.Alias Type SourceRegion Kinded
typedBody -> do
                                inferBody <- Type SourceRegion Kinded
-> Eff
     (State InferState
        : InferEffectsCons
            SourceRegion
            (Error (UnifyError SourceRegion)
               : Error KindInferError : Error TypeConvertError
               : ConsQueryEffects (Rock Query : r)))
     (Monotype SourceRegion)
forall (r :: [(* -> *) -> * -> *]).
(Error TypeConvertError :> r) =>
Type SourceRegion Kinded -> Eff r (Monotype SourceRegion)
astTypeToInferType Type SourceRegion Kinded
typedBody

                                let uVars = (Located (Unique LowerAlphaName) -> UniqueTyVar)
-> [Located (Unique LowerAlphaName)] -> [UniqueTyVar]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Located (Unique LowerAlphaName) -> UniqueTyVar
createTypeVar [Located (Unique LowerAlphaName)]
[TypeVariable Shunted SourceRegion]
typeVars

                                pure (Just (uVars, Lifted inferBody))
                            KindedTypeDeclaration
_ -> Maybe ([UniqueTyVar], Type SourceRegion)
-> Eff
     (State InferState
        : InferEffectsCons
            SourceRegion
            (Error (UnifyError SourceRegion)
               : Error KindInferError : Error TypeConvertError
               : ConsQueryEffects (Rock Query : r)))
     (Maybe ([UniqueTyVar], Type SourceRegion))
forall a.
a
-> Eff
     (State InferState
        : InferEffectsCons
            SourceRegion
            (Error (UnifyError SourceRegion)
               : Error KindInferError : Error TypeConvertError
               : ConsQueryEffects (Rock Query : r)))
     a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Maybe ([UniqueTyVar], Type SourceRegion)
forall a. Maybe a
Nothing

                    -- Extract the result from the inference pipeline
                    pure (fst res)
                DeclarationBody' SourceRegion Shunted
_ -> Maybe ([UniqueTyVar], Type SourceRegion)
-> Eff
     (ConsQueryEffects (Rock Query : r))
     (Maybe ([UniqueTyVar], Type SourceRegion))
forall a. a -> Eff (ConsQueryEffects (Rock Query : r)) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Maybe ([UniqueTyVar], Type SourceRegion)
forall a. Maybe a
Nothing
        Maybe (Declaration SourceRegion Shunted)
Nothing -> Maybe ([UniqueTyVar], Type SourceRegion)
-> Eff
     (ConsQueryEffects (Rock Query : r))
     (Maybe ([UniqueTyVar], Type SourceRegion))
forall a. a -> Eff (ConsQueryEffects (Rock Query : r)) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Maybe ([UniqueTyVar], Type SourceRegion)
forall a. Maybe a
Nothing
  where
    matchesTypeName :: TypeName -> New.Declaration SourceRegion Shunted -> Bool
    matchesTypeName :: TypeName -> Declaration SourceRegion Shunted -> Bool
matchesTypeName TypeName
tn (New.Declaration SourceRegion
_ (New.Declaration' Locate SourceRegion ModuleName
_ (New.DeclarationBody SourceRegion
_ DeclarationBody' SourceRegion Shunted
body'))) =
        case DeclarationBody' SourceRegion Shunted
body' of
            New.TypeDeclarationBody TopTypeBinder Shunted SourceRegion
n [TypeVariable Shunted SourceRegion]
_ TypeDeclaration SourceRegion Shunted
_ Maybe (Type SourceRegion Shunted)
_ TypeDeclMetadata Shunted SourceRegion
_ [Annotation SourceRegion Shunted]
_ -> (Located (Qualified TypeName)
TopTypeBinder Shunted SourceRegion
n Located (Qualified TypeName)
-> Optic' A_Lens NoIx (Located (Qualified TypeName)) TypeName
-> TypeName
forall k s (is :: IxList) a.
Is k A_Getter =>
s -> Optic' k is s a -> a
^. (Lens
  (Located (Qualified TypeName))
  (Located (Qualified TypeName))
  (Qualified TypeName)
  (Qualified TypeName)
forall a b. Lens (Located a) (Located b) a b
unlocated Lens
  (Located (Qualified TypeName))
  (Located (Qualified TypeName))
  (Qualified TypeName)
  (Qualified TypeName)
-> Optic' A_Lens NoIx (Qualified TypeName) TypeName
-> Optic' A_Lens NoIx (Located (Qualified TypeName)) TypeName
forall k l m (is :: IxList) (js :: IxList) (ks :: IxList) s t u v a
       b.
(JoinKinds k l m, AppendIndices is js ks) =>
Optic k is s t u v -> Optic l js u v a b -> Optic m ks s t a b
% Optic' A_Lens NoIx (Qualified TypeName) TypeName
forall name. Lens' (Qualified name) name
unqualified)) TypeName -> TypeName -> Bool
forall a. Eq a => a -> a -> Bool
== TypeName
tn
            DeclarationBody' SourceRegion Shunted
_ -> Bool
False

seedConstructorsFor :: (SupportsQuery QueryModuleByName Shunted, HasCallStack, _) => ModuleName -> Eff r ()
seedConstructorsFor :: ModuleName -> Eff r ()
seedConstructorsFor ModuleName
moduleName = Doc AnsiStyle -> Eff r () -> Eff r ()
forall (r :: [(* -> *) -> * -> *]) a.
(HasCallStack, StructuredDebug :> r) =>
Doc AnsiStyle -> Eff r a -> Eff r a
debugWith (Doc AnsiStyle
"seedConstructorsFor: " Doc AnsiStyle -> Doc AnsiStyle -> Doc AnsiStyle
forall a. Semigroup a => a -> a -> a
<> ModuleName -> Doc AnsiStyle
forall a. Pretty a => a -> Doc AnsiStyle
pretty ModuleName
moduleName) (Eff r () -> Eff r ()) -> Eff r () -> Eff r ()
forall a b. (a -> b) -> a -> b
$ do
    -- Fetch all declarations in the module
    mod <- forall e (r :: [(* -> *) -> * -> *]) a.
(DiagnosticWriter (Doc AnsiStyle) :> r,
 Error SomeReportableError :> r, ReportableError e) =>
Eff (Error e : r) a -> Eff r a
runErrorOrReport @ShuntError (Eff
   (Error ShuntError : r)
   (QueryReturnTypeOf QueryModuleByName Shunted)
 -> Eff r (QueryReturnTypeOf QueryModuleByName Shunted))
-> Eff
     (Error ShuntError : r)
     (QueryReturnTypeOf QueryModuleByName Shunted)
-> Eff r (QueryReturnTypeOf QueryModuleByName Shunted)
forall a b. (a -> b) -> a -> b
$ Query
  (QueryEffectsOf QueryModuleByName Shunted)
  (QueryReturnTypeOf QueryModuleByName Shunted)
-> Eff
     (Error ShuntError : r)
     (QueryReturnTypeOf QueryModuleByName Shunted)
forall (xs :: [(* -> *) -> * -> *]) (es :: [(* -> *) -> * -> *])
       (f :: [(* -> *) -> * -> *] -> * -> *) a.
(Subset xs es, Rock f :> es, HasCallStack,
 StructuredDebug :> xs) =>
f xs a -> Eff es a
Rock.fetch (Query
   (QueryEffectsOf QueryModuleByName Shunted)
   (QueryReturnTypeOf QueryModuleByName Shunted)
 -> Eff
      (Error ShuntError : r)
      (QueryReturnTypeOf QueryModuleByName Shunted))
-> Query
     (QueryEffectsOf QueryModuleByName Shunted)
     (QueryReturnTypeOf QueryModuleByName Shunted)
-> Eff
     (Error ShuntError : r)
     (QueryReturnTypeOf QueryModuleByName Shunted)
forall a b. (a -> b) -> a -> b
$ forall ast.
(Typeable ast, SupportsQuery QueryModuleByName ast,
 HasMinimumQueryEffects (QueryEffectsOf QueryModuleByName ast)) =>
ModuleName
-> Query
     (QueryEffectsOf QueryModuleByName ast)
     (QueryReturnTypeOf QueryModuleByName ast)
Elara.Query.ModuleByName @Shunted ModuleName
moduleName
    let NewModule.Module _ m' = mod

    -- Extract type declarations
    let typeDecls = (Declaration SourceRegion Shunted
 -> Maybe
      (Located (Qualified TypeName), [Located (Unique LowerAlphaName)],
       TypeDeclaration SourceRegion Shunted,
       [Annotation SourceRegion Shunted]))
-> [Declaration SourceRegion Shunted]
-> [(Located (Qualified TypeName),
     [Located (Unique LowerAlphaName)],
     TypeDeclaration SourceRegion Shunted,
     [Annotation SourceRegion Shunted])]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe Declaration SourceRegion Shunted
-> Maybe
     (Located (Qualified TypeName), [Located (Unique LowerAlphaName)],
      TypeDeclaration SourceRegion Shunted,
      [Annotation SourceRegion Shunted])
extractTypeDecl Module' SourceRegion Shunted
m'.moduleDeclarations

    for_ typeDecls $ \(Located (Qualified TypeName)
name, [Located (Unique LowerAlphaName)]
_, TypeDeclaration SourceRegion Shunted
_, [Annotation SourceRegion Shunted]
_) -> Qualified TypeName -> Eff r ()
forall (r :: [(* -> *) -> * -> *]).
(State InferState :> r, UniqueGen :> r, HasCallStack) =>
Qualified TypeName -> Eff r ()
Kind.preRegisterType (Located (Qualified TypeName)
name Located (Qualified TypeName)
-> Lens
     (Located (Qualified TypeName))
     (Located (Qualified TypeName))
     (Qualified TypeName)
     (Qualified TypeName)
-> Qualified TypeName
forall k s (is :: IxList) a.
Is k A_Getter =>
s -> Optic' k is s a -> a
^. Lens
  (Located (Qualified TypeName))
  (Located (Qualified TypeName))
  (Qualified TypeName)
  (Qualified TypeName)
forall a b. Lens (Located a) (Located b) a b
unlocated)

    -- For each type declaration, add its constructors to the environment
    for_ typeDecls $ \(Located (Qualified TypeName)
name, [Located (Unique LowerAlphaName)]
typeVars, TypeDeclaration SourceRegion Shunted
declBody, [Annotation SourceRegion Shunted]
_anns) -> Doc AnsiStyle -> Eff r () -> Eff r ()
forall (r :: [(* -> *) -> * -> *]) a.
(HasCallStack, StructuredDebug :> r) =>
Doc AnsiStyle -> Eff r a -> Eff r a
debugWith (Doc AnsiStyle
"Seeding declaration: " Doc AnsiStyle -> Doc AnsiStyle -> Doc AnsiStyle
forall a. Semigroup a => a -> a -> a
<> Located (Qualified TypeName) -> Doc AnsiStyle
forall a. Pretty a => a -> Doc AnsiStyle
pretty Located (Qualified TypeName)
name) (Eff r () -> Eff r ()) -> Eff r () -> Eff r ()
forall a b. (a -> b) -> a -> b
$ do
        (_, decl') <- Qualified TypeName
-> [Located (Unique LowerAlphaName)]
-> TypeDeclaration SourceRegion Shunted
-> Eff r (ElaraKind, KindedTypeDeclaration)
forall (r :: [(* -> *) -> * -> *]).
(HasCallStack, State InferState :> r, Error KindInferError :> r,
 Error SomeReportableError :> r,
 DiagnosticWriter (Doc AnsiStyle) :> r, Rock Query :> r,
 StructuredDebug :> r, UniqueGen :> r, FileSystem :> r,
 Concurrent :> r) =>
Qualified TypeName
-> [Located (Unique LowerAlphaName)]
-> TypeDeclaration SourceRegion Shunted
-> Eff r (ElaraKind, KindedTypeDeclaration)
inferKind (Located (Qualified TypeName)
name Located (Qualified TypeName)
-> Lens
     (Located (Qualified TypeName))
     (Located (Qualified TypeName))
     (Qualified TypeName)
     (Qualified TypeName)
-> Qualified TypeName
forall k s (is :: IxList) a.
Is k A_Getter =>
s -> Optic' k is s a -> a
^. Lens
  (Located (Qualified TypeName))
  (Located (Qualified TypeName))
  (Qualified TypeName)
  (Qualified TypeName)
forall a b. Lens (Located a) (Located b) a b
unlocated) [Located (Unique LowerAlphaName)]
typeVars TypeDeclaration SourceRegion Shunted
declBody
        case decl' of
            New.Alias Type SourceRegion Kinded
t -> do
                Doc AnsiStyle -> Eff r ()
forall (r :: [(* -> *) -> * -> *]).
(HasCallStack, StructuredDebug :> r) =>
Doc AnsiStyle -> Eff r ()
logDebug (Doc AnsiStyle -> Eff r ()) -> Doc AnsiStyle -> Eff r ()
forall a b. (a -> b) -> a -> b
$ Doc AnsiStyle
"Seeding alias type: " Doc AnsiStyle -> Doc AnsiStyle -> Doc AnsiStyle
forall a. Semigroup a => a -> a -> a
<> Located (Qualified TypeName) -> Doc AnsiStyle
forall a. Pretty a => a -> Doc AnsiStyle
pretty Located (Qualified TypeName)
name
                _ <- Type SourceRegion Kinded -> Eff r (Monotype SourceRegion)
forall (r :: [(* -> *) -> * -> *]).
(Error TypeConvertError :> r) =>
Type SourceRegion Kinded -> Eff r (Monotype SourceRegion)
astTypeToInferType Type SourceRegion Kinded
t
                pass -- we don't need to do anything with an alias i think
            New.ADT NonEmpty
  (ConstructorBinder Kinded SourceRegion, [Type SourceRegion Kinded])
ctors -> do
                let tyVars' :: [UniqueTyVar]
tyVars' = (Located (Unique LowerAlphaName) -> UniqueTyVar)
-> [Located (Unique LowerAlphaName)] -> [UniqueTyVar]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Located (Unique LowerAlphaName) -> UniqueTyVar
createTypeVar [Located (Unique LowerAlphaName)]
typeVars
                let typeConstructorType :: Monotype SourceRegion
typeConstructorType = SourceRegion
-> Qualified TypeName
-> [Monotype SourceRegion]
-> Monotype SourceRegion
forall loc.
loc -> Qualified TypeName -> [Monotype loc] -> Monotype loc
TypeConstructor (Located (Qualified TypeName)
name Located (Qualified TypeName)
-> Optic' A_Lens NoIx (Located (Qualified TypeName)) SourceRegion
-> SourceRegion
forall k s (is :: IxList) a.
Is k A_Getter =>
s -> Optic' k is s a -> a
^. Optic' A_Lens NoIx (Located (Qualified TypeName)) SourceRegion
forall a. HasSourceRegion a => Lens' a SourceRegion
sourceRegion) (Located (Qualified TypeName)
name Located (Qualified TypeName)
-> Lens
     (Located (Qualified TypeName))
     (Located (Qualified TypeName))
     (Qualified TypeName)
     (Qualified TypeName)
-> Qualified TypeName
forall k s (is :: IxList) a.
Is k A_Getter =>
s -> Optic' k is s a -> a
^. Lens
  (Located (Qualified TypeName))
  (Located (Qualified TypeName))
  (Qualified TypeName)
  (Qualified TypeName)
forall a b. Lens (Located a) (Located b) a b
unlocated) ((UniqueTyVar -> Monotype SourceRegion)
-> [UniqueTyVar] -> [Monotype SourceRegion]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (SourceRegion -> TypeVariable -> Monotype SourceRegion
forall loc. loc -> TypeVariable -> Monotype loc
TypeVar (Located (Qualified TypeName)
name Located (Qualified TypeName)
-> Optic' A_Lens NoIx (Located (Qualified TypeName)) SourceRegion
-> SourceRegion
forall k s (is :: IxList) a.
Is k A_Getter =>
s -> Optic' k is s a -> a
^. Optic' A_Lens NoIx (Located (Qualified TypeName)) SourceRegion
forall a. HasSourceRegion a => Lens' a SourceRegion
sourceRegion) (TypeVariable -> Monotype SourceRegion)
-> (UniqueTyVar -> TypeVariable)
-> UniqueTyVar
-> Monotype SourceRegion
forall b c a. (b -> c) -> (a -> b) -> a -> c
. UniqueTyVar -> TypeVariable
UnificationVar) [UniqueTyVar]
tyVars')

                let inferCtor :: (Located (Qualified TypeName), [Type SourceRegion Kinded])
-> Eff
     r
     (Located (Qualified TypeName),
      [(Monotype SourceRegion, ElaraKind)])
inferCtor (Located (Qualified TypeName)
ctorName, [Type SourceRegion Kinded]
t :: [KindedType]) = do
                        t' <- (Type SourceRegion Kinded
 -> Eff r (Monotype SourceRegion, ElaraKind))
-> [Type SourceRegion Kinded]
-> Eff r [(Monotype SourceRegion, ElaraKind)]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> [a] -> f [b]
traverse Type SourceRegion Kinded
-> Eff r (Monotype SourceRegion, ElaraKind)
forall (r :: [(* -> *) -> * -> *]).
(Error TypeConvertError :> r) =>
Type SourceRegion Kinded
-> Eff r (Monotype SourceRegion, ElaraKind)
astTypeToInferTypeWithKind [Type SourceRegion Kinded]
t
                        let ctorType =
                                ((Monotype SourceRegion, ElaraKind)
 -> Monotype SourceRegion -> Monotype SourceRegion)
-> Monotype SourceRegion
-> [(Monotype SourceRegion, ElaraKind)]
-> Monotype SourceRegion
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (SourceRegion
-> Monotype SourceRegion
-> Monotype SourceRegion
-> Monotype SourceRegion
forall loc. loc -> Monotype loc -> Monotype loc -> Monotype loc
Function (Located (Qualified TypeName)
name Located (Qualified TypeName)
-> Optic' A_Lens NoIx (Located (Qualified TypeName)) SourceRegion
-> SourceRegion
forall k s (is :: IxList) a.
Is k A_Getter =>
s -> Optic' k is s a -> a
^. Optic' A_Lens NoIx (Located (Qualified TypeName)) SourceRegion
forall a. HasSourceRegion a => Lens' a SourceRegion
sourceRegion) (Monotype SourceRegion
 -> Monotype SourceRegion -> Monotype SourceRegion)
-> ((Monotype SourceRegion, ElaraKind) -> Monotype SourceRegion)
-> (Monotype SourceRegion, ElaraKind)
-> Monotype SourceRegion
-> Monotype SourceRegion
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Monotype SourceRegion, ElaraKind) -> Monotype SourceRegion
forall a b. (a, b) -> a
fst) Monotype SourceRegion
typeConstructorType [(Monotype SourceRegion, ElaraKind)]
t'
                        addType' (DataConKey (ctorName ^. unlocated)) (Polytype (Forall (name ^. sourceRegion) tyVars' (EmptyConstraint (monotypeLoc ctorType)) ctorType))

                        pure (ctorName, t')

                NonEmpty (Located (Qualified TypeName), [Type SourceRegion Kinded])
-> ((Located (Qualified TypeName), [Type SourceRegion Kinded])
    -> Eff
         r
         (Located (Qualified TypeName),
          [(Monotype SourceRegion, ElaraKind)]))
-> Eff r ()
forall (t :: * -> *) (f :: * -> *) a b.
(Foldable t, Applicative f) =>
t a -> (a -> f b) -> f ()
for_ NonEmpty (Located (Qualified TypeName), [Type SourceRegion Kinded])
NonEmpty
  (ConstructorBinder Kinded SourceRegion, [Type SourceRegion Kinded])
ctors (Located (Qualified TypeName), [Type SourceRegion Kinded])
-> Eff
     r
     (Located (Qualified TypeName),
      [(Monotype SourceRegion, ElaraKind)])
inferCtor
  where
    extractTypeDecl :: New.Declaration SourceRegion Shunted -> Maybe (Located (Qualified TypeName), [Located (Unique LowerAlphaName)], New.TypeDeclaration SourceRegion Shunted, [New.Annotation SourceRegion Shunted])
    extractTypeDecl :: Declaration SourceRegion Shunted
-> Maybe
     (Located (Qualified TypeName), [Located (Unique LowerAlphaName)],
      TypeDeclaration SourceRegion Shunted,
      [Annotation SourceRegion Shunted])
extractTypeDecl (New.Declaration SourceRegion
_ (New.Declaration' Locate SourceRegion ModuleName
_ (New.DeclarationBody SourceRegion
_ DeclarationBody' SourceRegion Shunted
body'))) =
        case DeclarationBody' SourceRegion Shunted
body' of
            New.TypeDeclarationBody TopTypeBinder Shunted SourceRegion
name [TypeVariable Shunted SourceRegion]
typeVars TypeDeclaration SourceRegion Shunted
declBody Maybe (Type SourceRegion Shunted)
_ TypeDeclMetadata Shunted SourceRegion
_ [Annotation SourceRegion Shunted]
anns -> (Located (Qualified TypeName), [Located (Unique LowerAlphaName)],
 TypeDeclaration SourceRegion Shunted,
 [Annotation SourceRegion Shunted])
-> Maybe
     (Located (Qualified TypeName), [Located (Unique LowerAlphaName)],
      TypeDeclaration SourceRegion Shunted,
      [Annotation SourceRegion Shunted])
forall a. a -> Maybe a
Just (Located (Qualified TypeName)
TopTypeBinder Shunted SourceRegion
name, [Located (Unique LowerAlphaName)]
[TypeVariable Shunted SourceRegion]
typeVars, TypeDeclaration SourceRegion Shunted
declBody, [Annotation SourceRegion Shunted]
anns)
            DeclarationBody' SourceRegion Shunted
_ -> Maybe
  (Located (Qualified TypeName), [Located (Unique LowerAlphaName)],
   TypeDeclaration SourceRegion Shunted,
   [Annotation SourceRegion Shunted])
forall a. Maybe a
Nothing

runInferEffects ::
    forall r a loc.
    Pretty loc =>
    QueryEffects r =>
    Rock.Rock Query :> r =>
    Eq loc =>
    loc ~ SourceRegion =>
    Eff
        ( InferEffectsCons
            loc
            ( Error (UnifyError loc)
                ': Error KindInferError
                ': Error TypeConvertError
                ': r
            )
        )
        a ->
    Eff r (a, Constraint loc)
runInferEffects :: forall (r :: [(* -> *) -> * -> *]) a loc.
(Pretty loc, QueryEffects r, Rock Query :> r, Eq loc,
 loc ~ SourceRegion) =>
Eff
  (InferEffectsCons
     loc
     (Error (UnifyError loc)
        : Error KindInferError : Error TypeConvertError : r))
  a
-> Eff r (a, Constraint loc)
runInferEffects =
    forall e (r :: [(* -> *) -> * -> *]) a.
(DiagnosticWriter (Doc AnsiStyle) :> r,
 Error SomeReportableError :> r, ReportableError e) =>
Eff (Error e : r) a -> Eff r a
runErrorOrReport @(InferError _)
        (Eff (Error (InferError SourceRegion) : r) (a, Constraint loc)
 -> Eff r (a, Constraint loc))
-> (Eff
      (InferEffectsCons
         loc
         (Error (UnifyError loc)
            : Error KindInferError : Error TypeConvertError : r))
      a
    -> Eff (Error (InferError SourceRegion) : r) (a, Constraint loc))
-> Eff
     (InferEffectsCons
        loc
        (Error (UnifyError loc)
           : Error KindInferError : Error TypeConvertError : r))
     a
-> Eff r (a, Constraint loc)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall e (r :: [(* -> *) -> * -> *]) a.
(DiagnosticWriter (Doc AnsiStyle) :> r,
 Error SomeReportableError :> r, ReportableError e) =>
Eff (Error e : r) a -> Eff r a
runErrorOrReport @(UnifyError _)
        (Eff
   (Error (UnifyError SourceRegion)
      : Error (InferError SourceRegion) : r)
   (a, Constraint loc)
 -> Eff (Error (InferError SourceRegion) : r) (a, Constraint loc))
-> (Eff
      (InferEffectsCons
         loc
         (Error (UnifyError loc)
            : Error KindInferError : Error TypeConvertError : r))
      a
    -> Eff
         (Error (UnifyError SourceRegion)
            : Error (InferError SourceRegion) : r)
         (a, Constraint loc))
-> Eff
     (InferEffectsCons
        loc
        (Error (UnifyError loc)
           : Error KindInferError : Error TypeConvertError : r))
     a
-> Eff (Error (InferError SourceRegion) : r) (a, Constraint loc)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall e (r :: [(* -> *) -> * -> *]) a.
(DiagnosticWriter (Doc AnsiStyle) :> r,
 Error SomeReportableError :> r, ReportableError e) =>
Eff (Error e : r) a -> Eff r a
runErrorOrReport @KindInferError
        (Eff
   (Error KindInferError
      : Error (UnifyError SourceRegion) : Error (InferError SourceRegion)
      : r)
   (a, Constraint loc)
 -> Eff
      (Error (UnifyError SourceRegion)
         : Error (InferError SourceRegion) : r)
      (a, Constraint loc))
-> (Eff
      (InferEffectsCons
         loc
         (Error (UnifyError loc)
            : Error KindInferError : Error TypeConvertError : r))
      a
    -> Eff
         (Error KindInferError
            : Error (UnifyError SourceRegion) : Error (InferError SourceRegion)
            : r)
         (a, Constraint loc))
-> Eff
     (InferEffectsCons
        loc
        (Error (UnifyError loc)
           : Error KindInferError : Error TypeConvertError : r))
     a
-> Eff
     (Error (UnifyError SourceRegion)
        : Error (InferError SourceRegion) : r)
     (a, Constraint loc)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall e (r :: [(* -> *) -> * -> *]) a.
(DiagnosticWriter (Doc AnsiStyle) :> r,
 Error SomeReportableError :> r, ReportableError e) =>
Eff (Error e : r) a -> Eff r a
runErrorOrReport @TypeConvertError
        (Eff
   (Error TypeConvertError
      : Error KindInferError : Error (UnifyError SourceRegion)
      : Error (InferError SourceRegion) : r)
   (a, Constraint loc)
 -> Eff
      (Error KindInferError
         : Error (UnifyError SourceRegion) : Error (InferError SourceRegion)
         : r)
      (a, Constraint loc))
-> (Eff
      (InferEffectsCons
         loc
         (Error (UnifyError loc)
            : Error KindInferError : Error TypeConvertError : r))
      a
    -> Eff
         (Error TypeConvertError
            : Error KindInferError : Error (UnifyError SourceRegion)
            : Error (InferError SourceRegion) : r)
         (a, Constraint loc))
-> Eff
     (InferEffectsCons
        loc
        (Error (UnifyError loc)
           : Error KindInferError : Error TypeConvertError : r))
     a
-> Eff
     (Error KindInferError
        : Error (UnifyError SourceRegion) : Error (InferError SourceRegion)
        : r)
     (a, Constraint loc)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TypeEnvironment SourceRegion
-> Eff
     (State (TypeEnvironment SourceRegion)
        : Error TypeConvertError : Error KindInferError
        : Error (UnifyError SourceRegion) : Error (InferError SourceRegion)
        : r)
     (a, Constraint loc)
-> Eff
     (Error TypeConvertError
        : Error KindInferError : Error (UnifyError SourceRegion)
        : Error (InferError SourceRegion) : r)
     (a, Constraint loc)
forall s (es :: [(* -> *) -> * -> *]) a.
HasCallStack =>
s -> Eff (State s : es) a -> Eff es a
evalState TypeEnvironment SourceRegion
forall loc. TypeEnvironment loc
emptyTypeEnvironment
        (Eff
   (State (TypeEnvironment SourceRegion)
      : Error TypeConvertError : Error KindInferError
      : Error (UnifyError SourceRegion) : Error (InferError SourceRegion)
      : r)
   (a, Constraint loc)
 -> Eff
      (Error TypeConvertError
         : Error KindInferError : Error (UnifyError SourceRegion)
         : Error (InferError SourceRegion) : r)
      (a, Constraint loc))
-> (Eff
      (InferEffectsCons
         loc
         (Error (UnifyError loc)
            : Error KindInferError : Error TypeConvertError : r))
      a
    -> Eff
         (State (TypeEnvironment SourceRegion)
            : Error TypeConvertError : Error KindInferError
            : Error (UnifyError SourceRegion) : Error (InferError SourceRegion)
            : r)
         (a, Constraint loc))
-> Eff
     (InferEffectsCons
        loc
        (Error (UnifyError loc)
           : Error KindInferError : Error TypeConvertError : r))
     a
-> Eff
     (Error TypeConvertError
        : Error KindInferError : Error (UnifyError SourceRegion)
        : Error (InferError SourceRegion) : r)
     (a, Constraint loc)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. LocalTypeEnvironment SourceRegion
-> Eff
     (State (LocalTypeEnvironment SourceRegion)
        : State (TypeEnvironment SourceRegion) : Error TypeConvertError
        : Error KindInferError : Error (UnifyError SourceRegion)
        : Error (InferError SourceRegion) : r)
     (a, Constraint loc)
-> Eff
     (State (TypeEnvironment SourceRegion)
        : Error TypeConvertError : Error KindInferError
        : Error (UnifyError SourceRegion) : Error (InferError SourceRegion)
        : r)
     (a, Constraint loc)
forall s (es :: [(* -> *) -> * -> *]) a.
HasCallStack =>
s -> Eff (State s : es) a -> Eff es a
evalState LocalTypeEnvironment SourceRegion
forall loc. LocalTypeEnvironment loc
emptyLocalTypeEnvironment
        (Eff
   (State (LocalTypeEnvironment SourceRegion)
      : State (TypeEnvironment SourceRegion) : Error TypeConvertError
      : Error KindInferError : Error (UnifyError SourceRegion)
      : Error (InferError SourceRegion) : r)
   (a, Constraint loc)
 -> Eff
      (State (TypeEnvironment SourceRegion)
         : Error TypeConvertError : Error KindInferError
         : Error (UnifyError SourceRegion) : Error (InferError SourceRegion)
         : r)
      (a, Constraint loc))
-> (Eff
      (InferEffectsCons
         loc
         (Error (UnifyError loc)
            : Error KindInferError : Error TypeConvertError : r))
      a
    -> Eff
         (State (LocalTypeEnvironment SourceRegion)
            : State (TypeEnvironment SourceRegion) : Error TypeConvertError
            : Error KindInferError : Error (UnifyError SourceRegion)
            : Error (InferError SourceRegion) : r)
         (a, Constraint loc))
-> Eff
     (InferEffectsCons
        loc
        (Error (UnifyError loc)
           : Error KindInferError : Error TypeConvertError : r))
     a
-> Eff
     (State (TypeEnvironment SourceRegion)
        : Error TypeConvertError : Error KindInferError
        : Error (UnifyError SourceRegion) : Error (InferError SourceRegion)
        : r)
     (a, Constraint loc)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall w (es :: [(* -> *) -> * -> *]) a.
(HasCallStack, Monoid w) =>
Eff (Writer w : es) a -> Eff es (a, w)
runWriter @(Constraint SourceRegion)
        (Eff
   (Writer (Constraint SourceRegion)
      : State (LocalTypeEnvironment SourceRegion)
      : State (TypeEnvironment SourceRegion) : Error TypeConvertError
      : Error KindInferError : Error (UnifyError SourceRegion)
      : Error (InferError SourceRegion) : r)
   a
 -> Eff
      (State (LocalTypeEnvironment SourceRegion)
         : State (TypeEnvironment SourceRegion) : Error TypeConvertError
         : Error KindInferError : Error (UnifyError SourceRegion)
         : Error (InferError SourceRegion) : r)
      (a, Constraint loc))
-> (Eff
      (InferEffectsCons
         loc
         (Error (UnifyError loc)
            : Error KindInferError : Error TypeConvertError : r))
      a
    -> Eff
         (Writer (Constraint SourceRegion)
            : State (LocalTypeEnvironment SourceRegion)
            : State (TypeEnvironment SourceRegion) : Error TypeConvertError
            : Error KindInferError : Error (UnifyError SourceRegion)
            : Error (InferError SourceRegion) : r)
         a)
-> Eff
     (InferEffectsCons
        loc
        (Error (UnifyError loc)
           : Error KindInferError : Error TypeConvertError : r))
     a
-> Eff
     (State (LocalTypeEnvironment SourceRegion)
        : State (TypeEnvironment SourceRegion) : Error TypeConvertError
        : Error KindInferError : Error (UnifyError SourceRegion)
        : Error (InferError SourceRegion) : r)
     (a, Constraint loc)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ContextStack
-> Eff
     (Reader ContextStack
        : Writer (Constraint SourceRegion)
        : State (LocalTypeEnvironment SourceRegion)
        : State (TypeEnvironment SourceRegion) : Error TypeConvertError
        : Error KindInferError : Error (UnifyError SourceRegion)
        : Error (InferError SourceRegion) : r)
     a
-> Eff
     (Writer (Constraint SourceRegion)
        : State (LocalTypeEnvironment SourceRegion)
        : State (TypeEnvironment SourceRegion) : Error TypeConvertError
        : Error KindInferError : Error (UnifyError SourceRegion)
        : Error (InferError SourceRegion) : r)
     a
forall r (es :: [(* -> *) -> * -> *]) a.
HasCallStack =>
r -> Eff (Reader r : es) a -> Eff es a
runReader ContextStack
emptyContextStack
        (Eff
   (Reader ContextStack
      : Writer (Constraint SourceRegion)
      : State (LocalTypeEnvironment SourceRegion)
      : State (TypeEnvironment SourceRegion) : Error TypeConvertError
      : Error KindInferError : Error (UnifyError SourceRegion)
      : Error (InferError SourceRegion) : r)
   a
 -> Eff
      (Writer (Constraint SourceRegion)
         : State (LocalTypeEnvironment SourceRegion)
         : State (TypeEnvironment SourceRegion) : Error TypeConvertError
         : Error KindInferError : Error (UnifyError SourceRegion)
         : Error (InferError SourceRegion) : r)
      a)
-> (Eff
      (InferEffectsCons
         loc
         (Error (UnifyError loc)
            : Error KindInferError : Error TypeConvertError : r))
      a
    -> Eff
         (Reader ContextStack
            : Writer (Constraint SourceRegion)
            : State (LocalTypeEnvironment SourceRegion)
            : State (TypeEnvironment SourceRegion) : Error TypeConvertError
            : Error KindInferError : Error (UnifyError SourceRegion)
            : Error (InferError SourceRegion) : r)
         a)
-> Eff
     (InferEffectsCons
        loc
        (Error (UnifyError loc)
           : Error KindInferError : Error TypeConvertError : r))
     a
-> Eff
     (Writer (Constraint SourceRegion)
        : State (LocalTypeEnvironment SourceRegion)
        : State (TypeEnvironment SourceRegion) : Error TypeConvertError
        : Error KindInferError : Error (UnifyError SourceRegion)
        : Error (InferError SourceRegion) : r)
     a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Eff
  (InferEffectsCons
     loc
     (Error (UnifyError loc)
        : Error KindInferError : Error TypeConvertError : r))
  a
-> Eff
     (Reader ContextStack
        : Writer (Constraint SourceRegion)
        : State (LocalTypeEnvironment SourceRegion)
        : State (TypeEnvironment SourceRegion) : Error TypeConvertError
        : Error KindInferError : Error (UnifyError SourceRegion)
        : Error (InferError SourceRegion) : r)
     a
forall (subEs :: [(* -> *) -> * -> *]) (es :: [(* -> *) -> * -> *])
       a.
Subset subEs es =>
Eff subEs a -> Eff es a
inject

runInferSCCQuery ::
    SupportsQuery QueryRequiredDeclarationByName Shunted =>
    SCCKey ->
    Eff
        (ConsQueryEffects (Rock.Rock Query : r))
        (Map (Qualified VarName) (Polytype SourceRegion))
runInferSCCQuery :: forall (r :: [(* -> *) -> * -> *]).
SupportsQuery QueryRequiredDeclarationByName Shunted =>
SCCKey
-> Eff
     (ConsQueryEffects (Rock Query : r))
     (Map (Qualified VarName) (Polytype SourceRegion))
runInferSCCQuery SCCKey
key = (Map (Qualified VarName) (Polytype SourceRegion),
 Constraint SourceRegion)
-> Map (Qualified VarName) (Polytype SourceRegion)
forall a b. (a, b) -> a
fst ((Map (Qualified VarName) (Polytype SourceRegion),
  Constraint SourceRegion)
 -> Map (Qualified VarName) (Polytype SourceRegion))
-> Eff
     (ConsQueryEffects (Rock Query : r))
     (Map (Qualified VarName) (Polytype SourceRegion),
      Constraint SourceRegion)
-> Eff
     (ConsQueryEffects (Rock Query : r))
     (Map (Qualified VarName) (Polytype SourceRegion))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Eff
  (InferEffectsCons
     SourceRegion
     (Error (UnifyError SourceRegion)
        : Error KindInferError : Error TypeConvertError
        : ConsQueryEffects (Rock Query : r)))
  (Map (Qualified VarName) (Polytype SourceRegion))
-> Eff
     (ConsQueryEffects (Rock Query : r))
     (Map (Qualified VarName) (Polytype SourceRegion),
      Constraint SourceRegion)
forall (r :: [(* -> *) -> * -> *]) a loc.
(Pretty loc, QueryEffects r, Rock Query :> r, Eq loc,
 loc ~ SourceRegion) =>
Eff
  (InferEffectsCons
     loc
     (Error (UnifyError loc)
        : Error KindInferError : Error TypeConvertError : r))
  a
-> Eff r (a, Constraint loc)
runInferEffects (InferState
-> Eff
     (State InferState
        : InferEffectsCons
            SourceRegion
            (Error (UnifyError SourceRegion)
               : Error KindInferError : Error TypeConvertError
               : ConsQueryEffects (Rock Query : r)))
     (Map (Qualified VarName) (Polytype SourceRegion))
-> Eff
     (InferEffectsCons
        SourceRegion
        (Error (UnifyError SourceRegion)
           : Error KindInferError : Error TypeConvertError
           : ConsQueryEffects (Rock Query : r)))
     (Map (Qualified VarName) (Polytype SourceRegion))
forall s (es :: [(* -> *) -> * -> *]) a.
HasCallStack =>
s -> Eff (State s : es) a -> Eff es a
evalState InferState
initialInferState (Eff
   (State InferState
      : InferEffectsCons
          SourceRegion
          (Error (UnifyError SourceRegion)
             : Error KindInferError : Error TypeConvertError
             : ConsQueryEffects (Rock Query : r)))
   (Map (Qualified VarName) (Polytype SourceRegion))
 -> Eff
      (InferEffectsCons
         SourceRegion
         (Error (UnifyError SourceRegion)
            : Error KindInferError : Error TypeConvertError
            : ConsQueryEffects (Rock Query : r)))
      (Map (Qualified VarName) (Polytype SourceRegion)))
-> Eff
     (State InferState
        : InferEffectsCons
            SourceRegion
            (Error (UnifyError SourceRegion)
               : Error KindInferError : Error TypeConvertError
               : ConsQueryEffects (Rock Query : r)))
     (Map (Qualified VarName) (Polytype SourceRegion))
-> Eff
     (InferEffectsCons
        SourceRegion
        (Error (UnifyError SourceRegion)
           : Error KindInferError : Error TypeConvertError
           : ConsQueryEffects (Rock Query : r)))
     (Map (Qualified VarName) (Polytype SourceRegion))
forall a b. (a -> b) -> a -> b
$ SCC (Qualified VarName)
-> Eff
     (State InferState
        : InferEffectsCons
            SourceRegion
            (Error (UnifyError SourceRegion)
               : Error KindInferError : Error TypeConvertError
               : ConsQueryEffects (Rock Query : r)))
     (Map (Qualified VarName) (Polytype SourceRegion))
forall (r :: [(* -> *) -> * -> *]).
(SupportsQuery QueryRequiredDeclarationByName Shunted,
 DiagnosticWriter (Doc AnsiStyle) :> r, Rock Query :> r,
 Error (InferError SourceRegion) :> r,
 Error (UnifyError SourceRegion) :> r,
 Error SomeReportableError :> r,
 State (TypeEnvironment SourceRegion) :> r,
 State (LocalTypeEnvironment SourceRegion) :> r,
 Reader ContextStack :> r, StructuredDebug :> r, FileSystem :> r,
 UniqueGen :> r, Concurrent :> r) =>
SCC (Qualified VarName)
-> Eff r (Map (Qualified VarName) (Polytype SourceRegion))
inferSCC (SCCKey -> SCC (Qualified VarName)
sccKeyToSCC SCCKey
key))

seedSCC :: (SupportsQuery QueryRequiredDeclarationByName Shunted, _) => SCC (Qualified VarName) -> Eff r ()
seedSCC :: SCC (Qualified VarName) -> Eff r ()
seedSCC SCC (Qualified VarName)
scc = do
    Doc AnsiStyle -> Eff r ()
forall (r :: [(* -> *) -> * -> *]).
(HasCallStack, StructuredDebug :> r) =>
Doc AnsiStyle -> Eff r ()
logDebug (Doc AnsiStyle -> Eff r ()) -> Doc AnsiStyle -> Eff r ()
forall a b. (a -> b) -> a -> b
$ Doc AnsiStyle
"Seeding SCC: " Doc AnsiStyle -> Doc AnsiStyle -> Doc AnsiStyle
forall a. Semigroup a => a -> a -> a
<> [Qualified VarName] -> Doc AnsiStyle
forall a. Pretty a => a -> Doc AnsiStyle
pretty (SCC (Qualified VarName) -> [Qualified VarName]
forall vertex. SCC vertex -> [vertex]
flattenSCC SCC (Qualified VarName)
scc)
    SCC (Qualified VarName)
-> (Qualified VarName -> Eff r ()) -> Eff r ()
forall (t :: * -> *) (f :: * -> *) a b.
(Foldable t, Applicative f) =>
t a -> (a -> f b) -> f ()
for_ SCC (Qualified VarName)
scc ((Qualified VarName -> Eff r ()) -> Eff r ())
-> (Qualified VarName -> Eff r ()) -> Eff r ()
forall a b. (a -> b) -> a -> b
$ \Qualified VarName
component -> do
        decl <- forall e (r :: [(* -> *) -> * -> *]) a.
(DiagnosticWriter (Doc AnsiStyle) :> r,
 Error SomeReportableError :> r, ReportableError e) =>
Eff (Error e : r) a -> Eff r a
runErrorOrReport @ShuntError (Eff
   (Error ShuntError : r)
   (QueryReturnTypeOf QueryRequiredDeclarationByName Shunted)
 -> Eff
      r (QueryReturnTypeOf QueryRequiredDeclarationByName Shunted))
-> Eff
     (Error ShuntError : r)
     (QueryReturnTypeOf QueryRequiredDeclarationByName Shunted)
-> Eff r (QueryReturnTypeOf QueryRequiredDeclarationByName Shunted)
forall a b. (a -> b) -> a -> b
$ Query
  (QueryEffectsOf QueryRequiredDeclarationByName Shunted)
  (QueryReturnTypeOf QueryRequiredDeclarationByName Shunted)
-> Eff
     (Error ShuntError : r)
     (QueryReturnTypeOf QueryRequiredDeclarationByName Shunted)
forall (xs :: [(* -> *) -> * -> *]) (es :: [(* -> *) -> * -> *])
       (f :: [(* -> *) -> * -> *] -> * -> *) a.
(Subset xs es, Rock f :> es, HasCallStack,
 StructuredDebug :> xs) =>
f xs a -> Eff es a
Rock.fetch (Query
   (QueryEffectsOf QueryRequiredDeclarationByName Shunted)
   (QueryReturnTypeOf QueryRequiredDeclarationByName Shunted)
 -> Eff
      (Error ShuntError : r)
      (QueryReturnTypeOf QueryRequiredDeclarationByName Shunted))
-> Query
     (QueryEffectsOf QueryRequiredDeclarationByName Shunted)
     (QueryReturnTypeOf QueryRequiredDeclarationByName Shunted)
-> Eff
     (Error ShuntError : r)
     (QueryReturnTypeOf QueryRequiredDeclarationByName Shunted)
forall a b. (a -> b) -> a -> b
$ forall ast.
(Typeable ast, SupportsQuery QueryRequiredDeclarationByName ast) =>
QueryArgsOf QueryRequiredDeclarationByName ast
-> Query
     (QueryEffectsOf QueryRequiredDeclarationByName ast)
     (QueryReturnTypeOf QueryRequiredDeclarationByName ast)
Elara.Query.RequiredDeclarationByName @Shunted (VarName -> Name
NVarName (VarName -> Name) -> Qualified VarName -> Qualified Name
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Qualified VarName
component)
        seedDeclaration decl

inferSCC ::
    ( SupportsQuery QueryRequiredDeclarationByName Shunted
    , _
    ) =>
    SCC (Qualified VarName) -> Eff r (Map (Qualified VarName) (Polytype SourceRegion))
inferSCC :: SCC (Qualified VarName)
-> Eff r (Map (Qualified VarName) (Polytype SourceRegion))
inferSCC SCC (Qualified VarName)
scc = do
    prettyState <- TypeEnvironment SourceRegion -> Doc AnsiStyle
forall a. Pretty a => a -> Doc AnsiStyle
pretty (TypeEnvironment SourceRegion -> Doc AnsiStyle)
-> Eff r (TypeEnvironment SourceRegion) -> Eff r (Doc AnsiStyle)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall s (es :: [(* -> *) -> * -> *]).
(HasCallStack, State s :> es) =>
Eff es s
get @(TypeEnvironment SourceRegion)
    logDebug $ "Seeding SCC complete. Environment:\n" <> prettyState
    inferred <- for scc $ \Qualified VarName
component -> do
        decl <- forall e (r :: [(* -> *) -> * -> *]) a.
(DiagnosticWriter (Doc AnsiStyle) :> r,
 Error SomeReportableError :> r, ReportableError e) =>
Eff (Error e : r) a -> Eff r a
runErrorOrReport @ShuntError (Eff
   (Error ShuntError : r)
   (QueryReturnTypeOf QueryRequiredDeclarationByName Shunted)
 -> Eff
      r (QueryReturnTypeOf QueryRequiredDeclarationByName Shunted))
-> Eff
     (Error ShuntError : r)
     (QueryReturnTypeOf QueryRequiredDeclarationByName Shunted)
-> Eff r (QueryReturnTypeOf QueryRequiredDeclarationByName Shunted)
forall a b. (a -> b) -> a -> b
$ Query
  (QueryEffectsOf QueryRequiredDeclarationByName Shunted)
  (QueryReturnTypeOf QueryRequiredDeclarationByName Shunted)
-> Eff
     (Error ShuntError : r)
     (QueryReturnTypeOf QueryRequiredDeclarationByName Shunted)
forall (xs :: [(* -> *) -> * -> *]) (es :: [(* -> *) -> * -> *])
       (f :: [(* -> *) -> * -> *] -> * -> *) a.
(Subset xs es, Rock f :> es, HasCallStack,
 StructuredDebug :> xs) =>
f xs a -> Eff es a
Rock.fetch (Query
   (QueryEffectsOf QueryRequiredDeclarationByName Shunted)
   (QueryReturnTypeOf QueryRequiredDeclarationByName Shunted)
 -> Eff
      (Error ShuntError : r)
      (QueryReturnTypeOf QueryRequiredDeclarationByName Shunted))
-> Query
     (QueryEffectsOf QueryRequiredDeclarationByName Shunted)
     (QueryReturnTypeOf QueryRequiredDeclarationByName Shunted)
-> Eff
     (Error ShuntError : r)
     (QueryReturnTypeOf QueryRequiredDeclarationByName Shunted)
forall a b. (a -> b) -> a -> b
$ forall ast.
(Typeable ast, SupportsQuery QueryRequiredDeclarationByName ast) =>
QueryArgsOf QueryRequiredDeclarationByName ast
-> Query
     (QueryEffectsOf QueryRequiredDeclarationByName ast)
     (QueryReturnTypeOf QueryRequiredDeclarationByName ast)
Elara.Query.RequiredDeclarationByName @Shunted (VarName -> Name
NVarName (VarName -> Name) -> Qualified VarName -> Qualified Name
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Qualified VarName
component)
        inferred <- inferDeclarationScheme decl
        pure (component, inferred)

    pure $ fromList @(Map _ _) (toList inferred)

runTypeCheckedExprQuery :: Qualified VarName -> Eff (ConsQueryEffects (Rock.Rock Query : r)) TypedExpr
runTypeCheckedExprQuery :: forall (r :: [(* -> *) -> * -> *]).
Qualified VarName
-> Eff (ConsQueryEffects (Rock Query : r)) TypedExpr
runTypeCheckedExprQuery Qualified VarName
name = do
    mod <- Query
  (Rock Query : ConsQueryEffects '[]) (Module SourceRegion Typed)
-> Eff
     (ConsQueryEffects (Rock Query : r)) (Module SourceRegion Typed)
forall (xs :: [(* -> *) -> * -> *]) (es :: [(* -> *) -> * -> *])
       (f :: [(* -> *) -> * -> *] -> * -> *) a.
(Subset xs es, Rock f :> es, HasCallStack,
 StructuredDebug :> xs) =>
f xs a -> Eff es a
Rock.fetch (Query
   (Rock Query : ConsQueryEffects '[]) (Module SourceRegion Typed)
 -> Eff
      (ConsQueryEffects (Rock Query : r)) (Module SourceRegion Typed))
-> Query
     (Rock Query : ConsQueryEffects '[]) (Module SourceRegion Typed)
-> Eff
     (ConsQueryEffects (Rock Query : r)) (Module SourceRegion Typed)
forall a b. (a -> b) -> a -> b
$ ModuleName
-> Query
     (Rock Query : ConsQueryEffects '[]) (Module SourceRegion Typed)
TypeCheckedModule (Qualified VarName -> ModuleName
forall name. Qualified name -> ModuleName
qualifier Qualified VarName
name)
    let NewModule.Module _ m' = mod
    case find (matchesValueName name) m'.moduleDeclarations of
        Just (New.Declaration SourceRegion
_ (New.Declaration' Locate SourceRegion ModuleName
_ (New.DeclarationBody SourceRegion
_ (New.ValueDeclaration TopValueBinder Typed SourceRegion
_ TypedExpr
e ValueDeclPatterns Typed SourceRegion
_ ValueDeclTypeAnnotation Typed SourceRegion
_ ValueDeclMetadata Typed SourceRegion
_ [Annotation SourceRegion Typed]
_)))) -> TypedExpr -> Eff (ConsQueryEffects (Rock Query : r)) TypedExpr
forall a. a -> Eff (ConsQueryEffects (Rock Query : r)) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure TypedExpr
e
        Maybe (Declaration SourceRegion Typed)
_ -> Text -> Eff (ConsQueryEffects (Rock Query : r)) TypedExpr
forall a t. (HasCallStack, IsText t) => t -> a
error (Text -> Eff (ConsQueryEffects (Rock Query : r)) TypedExpr)
-> Text -> Eff (ConsQueryEffects (Rock Query : r)) TypedExpr
forall a b. (a -> b) -> a -> b
$ Text
"could not find declaration for " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Qualified VarName -> Text
forall b a. (Show a, IsString b) => a -> b
show Qualified VarName
name
  where
    matchesValueName :: Qualified VarName -> New.Declaration SourceRegion Typed -> Bool
    matchesValueName :: Qualified VarName -> Declaration SourceRegion Typed -> Bool
matchesValueName Qualified VarName
qn (New.Declaration SourceRegion
_ (New.Declaration' Locate SourceRegion ModuleName
_ (New.DeclarationBody SourceRegion
_ DeclarationBody' SourceRegion Typed
body'))) =
        case DeclarationBody' SourceRegion Typed
body' of
            New.ValueDeclaration TopValueBinder Typed SourceRegion
n TypedExpr
_ ValueDeclPatterns Typed SourceRegion
_ ValueDeclTypeAnnotation Typed SourceRegion
_ ValueDeclMetadata Typed SourceRegion
_ [Annotation SourceRegion Typed]
_ -> Located (Qualified VarName)
TopValueBinder Typed SourceRegion
n Located (Qualified VarName)
-> Optic'
     A_Lens NoIx (Located (Qualified VarName)) (Qualified VarName)
-> Qualified VarName
forall k s (is :: IxList) a.
Is k A_Getter =>
s -> Optic' k is s a -> a
^. Optic'
  A_Lens NoIx (Located (Qualified VarName)) (Qualified VarName)
forall a b. Lens (Located a) (Located b) a b
unlocated Qualified VarName -> Qualified VarName -> Bool
forall a. Eq a => a -> a -> Bool
== Qualified VarName
qn
            DeclarationBody' SourceRegion Typed
_ -> Bool
False

runTypeCheckedDeclarationQuery :: Qualified Name -> Eff (ConsQueryEffects (Rock.Rock Query : r)) TypedDeclaration
runTypeCheckedDeclarationQuery :: forall (r :: [(* -> *) -> * -> *]).
Qualified Name
-> Eff
     (ConsQueryEffects (Rock Query : r))
     (Declaration SourceRegion Typed)
runTypeCheckedDeclarationQuery Qualified Name
name = do
    shuntedDecl <- forall e (r :: [(* -> *) -> * -> *]) a.
(DiagnosticWriter (Doc AnsiStyle) :> r,
 Error SomeReportableError :> r, ReportableError e) =>
Eff (Error e : r) a -> Eff r a
runErrorOrReport @ShuntError (Eff
   (Error ShuntError : ConsQueryEffects (Rock Query : r))
   (Declaration SourceRegion Shunted)
 -> Eff
      (ConsQueryEffects (Rock Query : r))
      (Declaration SourceRegion Shunted))
-> Eff
     (Error ShuntError : ConsQueryEffects (Rock Query : r))
     (Declaration SourceRegion Shunted)
-> Eff
     (ConsQueryEffects (Rock Query : r))
     (Declaration SourceRegion Shunted)
forall a b. (a -> b) -> a -> b
$ Query
  (WithRock (ConsQueryEffects '[Error ShuntError]))
  (Declaration SourceRegion Shunted)
-> Eff
     (Error ShuntError : ConsQueryEffects (Rock Query : r))
     (Declaration SourceRegion Shunted)
forall (xs :: [(* -> *) -> * -> *]) (es :: [(* -> *) -> * -> *])
       (f :: [(* -> *) -> * -> *] -> * -> *) a.
(Subset xs es, Rock f :> es, HasCallStack,
 StructuredDebug :> xs) =>
f xs a -> Eff es a
Rock.fetch (forall ast.
(Typeable ast, SupportsQuery QueryRequiredDeclarationByName ast) =>
QueryArgsOf QueryRequiredDeclarationByName ast
-> Query
     (QueryEffectsOf QueryRequiredDeclarationByName ast)
     (QueryReturnTypeOf QueryRequiredDeclarationByName ast)
Elara.Query.RequiredDeclarationByName @Shunted Qualified Name
QueryArgsOf QueryRequiredDeclarationByName Shunted
name)
    let New.Declaration _ (New.Declaration' _ (New.DeclarationBody _ shuntedBody')) = shuntedDecl
    (typedDecl, _) <- runInferEffects $ evalState initialInferState $ case shuntedBody' of
        New.ValueDeclaration TopValueBinder Shunted SourceRegion
valueName Expr SourceRegion Shunted
expr ValueDeclPatterns Shunted SourceRegion
_ ValueDeclTypeAnnotation Shunted SourceRegion
_ ValueDeclMetadata Shunted SourceRegion
_ [Annotation SourceRegion Shunted]
_ -> do
            let varName :: Qualified VarName
varName = Located (Qualified VarName)
TopValueBinder Shunted SourceRegion
valueName Located (Qualified VarName)
-> Optic'
     A_Lens NoIx (Located (Qualified VarName)) (Qualified VarName)
-> Qualified VarName
forall k s (is :: IxList) a.
Is k A_Getter =>
s -> Optic' k is s a -> a
^. Optic'
  A_Lens NoIx (Located (Qualified VarName)) (Qualified VarName)
forall a b. Lens (Located a) (Located b) a b
unlocated

            deps <- Query
  (Rock Query : ConsQueryEffects '[]) (HashSet (Qualified VarName))
-> Eff
     (State InferState
        : InferEffectsCons
            SourceRegion
            (Error (UnifyError SourceRegion)
               : Error KindInferError : Error TypeConvertError
               : ConsQueryEffects (Rock Query : r)))
     (HashSet (Qualified VarName))
forall (xs :: [(* -> *) -> * -> *]) (es :: [(* -> *) -> * -> *])
       (f :: [(* -> *) -> * -> *] -> * -> *) a.
(Subset xs es, Rock f :> es, HasCallStack,
 StructuredDebug :> xs) =>
f xs a -> Eff es a
Rock.fetch (Qualified VarName
-> Query
     (Rock Query : ConsQueryEffects '[]) (HashSet (Qualified VarName))
Elara.Query.FreeVarsOf Qualified VarName
varName)
            sccKey <- Rock.fetch (Elara.Query.SCCKeyOf varName)
            let scc = SCCKey -> SCC (Qualified VarName)
sccKeyToSCC SCCKey
sccKey
            let sccSet = [Qualified VarName] -> Set (Qualified VarName)
forall a. Ord a => [a] -> Set a
Set.fromList (SCC (Qualified VarName) -> [Qualified VarName]
forall vertex. SCC vertex -> [vertex]
flattenSCC SCC (Qualified VarName)
scc)

            for_ deps $ \Qualified VarName
dep -> do
                -- Only seed if it's not part of the current recursive cycle
                Bool
-> Eff
     (State InferState
        : InferEffectsCons
            SourceRegion
            (Error (UnifyError SourceRegion)
               : Error KindInferError : Error TypeConvertError
               : ConsQueryEffects (Rock Query : r)))
     ()
-> Eff
     (State InferState
        : InferEffectsCons
            SourceRegion
            (Error (UnifyError SourceRegion)
               : Error KindInferError : Error TypeConvertError
               : ConsQueryEffects (Rock Query : r)))
     ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Qualified VarName
dep Qualified VarName -> Set (Qualified VarName) -> Bool
forall a. Ord a => a -> Set a -> Bool
`Set.member` Set (Qualified VarName)
sccSet) (Eff
   (State InferState
      : InferEffectsCons
          SourceRegion
          (Error (UnifyError SourceRegion)
             : Error KindInferError : Error TypeConvertError
             : ConsQueryEffects (Rock Query : r)))
   ()
 -> Eff
      (State InferState
         : InferEffectsCons
             SourceRegion
             (Error (UnifyError SourceRegion)
                : Error KindInferError : Error TypeConvertError
                : ConsQueryEffects (Rock Query : r)))
      ())
-> Eff
     (State InferState
        : InferEffectsCons
            SourceRegion
            (Error (UnifyError SourceRegion)
               : Error KindInferError : Error TypeConvertError
               : ConsQueryEffects (Rock Query : r)))
     ()
-> Eff
     (State InferState
        : InferEffectsCons
            SourceRegion
            (Error (UnifyError SourceRegion)
               : Error KindInferError : Error TypeConvertError
               : ConsQueryEffects (Rock Query : r)))
     ()
forall a b. (a -> b) -> a -> b
$ do
                    -- Fetch the type from Rock (cached)
                    t <- Query (Rock Query : ConsQueryEffects '[]) (Type SourceRegion)
-> Eff
     (State InferState
        : InferEffectsCons
            SourceRegion
            (Error (UnifyError SourceRegion)
               : Error KindInferError : Error TypeConvertError
               : ConsQueryEffects (Rock Query : r)))
     (Type SourceRegion)
forall (xs :: [(* -> *) -> * -> *]) (es :: [(* -> *) -> * -> *])
       (f :: [(* -> *) -> * -> *] -> * -> *) a.
(Subset xs es, Rock f :> es, HasCallStack,
 StructuredDebug :> xs) =>
f xs a -> Eff es a
Rock.fetch (TypeEnvKey SourceRegion
-> Query (Rock Query : ConsQueryEffects '[]) (Type SourceRegion)
forall loc.
(loc ~ SourceRegion) =>
TypeEnvKey loc
-> Query (Rock Query : ConsQueryEffects '[]) (Type loc)
Elara.Query.TypeOf (Qualified VarName -> TypeEnvKey SourceRegion
forall {k} (loc :: k). Qualified VarName -> TypeEnvKey loc
TermVarKey Qualified VarName
dep))
                    -- Add to the local inference state
                    addType' (TermVarKey dep) t

            -- Values might use constructors,
            -- so we need to ensure their types are in the environment.
            let usedConstructors = Expr SourceRegion Shunted -> [Qualified TypeName]
collectConstructors Expr SourceRegion Shunted
expr

            for_ usedConstructors $ \Qualified TypeName
ctorName -> do
                -- This helper fetches the module defining the Ctor and registers types
                ModuleName
-> Eff
     (State InferState
        : InferEffectsCons
            SourceRegion
            (Error (UnifyError SourceRegion)
               : Error KindInferError : Error TypeConvertError
               : ConsQueryEffects (Rock Query : r)))
     ()
forall (r :: [(* -> *) -> * -> *]).
(SupportsQuery QueryModuleByName Shunted, HasCallStack,
 Rock Query :> r, DiagnosticWriter (Doc AnsiStyle) :> r,
 Error SomeReportableError :> r, Error KindInferError :> r,
 Error TypeConvertError :> r,
 State (TypeEnvironment SourceRegion) :> r, State InferState :> r,
 Concurrent :> r, UniqueGen :> r, FileSystem :> r,
 StructuredDebug :> r) =>
ModuleName -> Eff r ()
seedConstructorsFor (Qualified TypeName -> ModuleName
forall name. Qualified name -> ModuleName
qualifier Qualified TypeName
ctorName)

            -- infer the entire SCC together to solve mutual recursion constraints.
            inferredDecls <- for scc $ \Qualified VarName
sccMemberName -> do
                -- Fetch member source
                memberDecl <- forall e (r :: [(* -> *) -> * -> *]) a.
(DiagnosticWriter (Doc AnsiStyle) :> r,
 Error SomeReportableError :> r, ReportableError e) =>
Eff (Error e : r) a -> Eff r a
runErrorOrReport @ShuntError (Eff
   (Error ShuntError
      : State InferState
      : InferEffectsCons
          SourceRegion
          (Error (UnifyError SourceRegion)
             : Error KindInferError : Error TypeConvertError
             : ConsQueryEffects (Rock Query : r)))
   (Declaration SourceRegion Shunted)
 -> Eff
      (State InferState
         : InferEffectsCons
             SourceRegion
             (Error (UnifyError SourceRegion)
                : Error KindInferError : Error TypeConvertError
                : ConsQueryEffects (Rock Query : r)))
      (Declaration SourceRegion Shunted))
-> Eff
     (Error ShuntError
        : State InferState
        : InferEffectsCons
            SourceRegion
            (Error (UnifyError SourceRegion)
               : Error KindInferError : Error TypeConvertError
               : ConsQueryEffects (Rock Query : r)))
     (Declaration SourceRegion Shunted)
-> Eff
     (State InferState
        : InferEffectsCons
            SourceRegion
            (Error (UnifyError SourceRegion)
               : Error KindInferError : Error TypeConvertError
               : ConsQueryEffects (Rock Query : r)))
     (Declaration SourceRegion Shunted)
forall a b. (a -> b) -> a -> b
$ Query
  (WithRock (ConsQueryEffects '[Error ShuntError]))
  (Declaration SourceRegion Shunted)
-> Eff
     (Error ShuntError
        : State InferState
        : InferEffectsCons
            SourceRegion
            (Error (UnifyError SourceRegion)
               : Error KindInferError : Error TypeConvertError
               : ConsQueryEffects (Rock Query : r)))
     (Declaration SourceRegion Shunted)
forall (xs :: [(* -> *) -> * -> *]) (es :: [(* -> *) -> * -> *])
       (f :: [(* -> *) -> * -> *] -> * -> *) a.
(Subset xs es, Rock f :> es, HasCallStack,
 StructuredDebug :> xs) =>
f xs a -> Eff es a
Rock.fetch (forall ast.
(Typeable ast, SupportsQuery QueryRequiredDeclarationByName ast) =>
QueryArgsOf QueryRequiredDeclarationByName ast
-> Query
     (QueryEffectsOf QueryRequiredDeclarationByName ast)
     (QueryReturnTypeOf QueryRequiredDeclarationByName ast)
Elara.Query.RequiredDeclarationByName @Shunted (VarName -> Name
NVarName (VarName -> Name) -> Qualified VarName -> Qualified Name
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Qualified VarName
sccMemberName))
                inferDeclaration memberDecl

            case find (\Declaration SourceRegion Typed
d -> Declaration SourceRegion Typed -> Name
declarationName Declaration SourceRegion Typed
d Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== (Qualified Name
name Qualified Name -> Optic' A_Lens NoIx (Qualified Name) Name -> Name
forall k s (is :: IxList) a.
Is k A_Getter =>
s -> Optic' k is s a -> a
^. Optic' A_Lens NoIx (Qualified Name) Name
forall name. Lens' (Qualified name) name
unqualified)) inferredDecls of
                Just Declaration SourceRegion Typed
d -> Declaration SourceRegion Typed
-> Eff
     (State InferState
        : InferEffectsCons
            SourceRegion
            (Error (UnifyError SourceRegion)
               : Error KindInferError : Error TypeConvertError
               : ConsQueryEffects (Rock Query : r)))
     (Declaration SourceRegion Typed)
forall a.
a
-> Eff
     (State InferState
        : InferEffectsCons
            SourceRegion
            (Error (UnifyError SourceRegion)
               : Error KindInferError : Error TypeConvertError
               : ConsQueryEffects (Rock Query : r)))
     a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Declaration SourceRegion Typed
d
                Maybe (Declaration SourceRegion Typed)
Nothing -> Text
-> Eff
     (State InferState
        : InferEffectsCons
            SourceRegion
            (Error (UnifyError SourceRegion)
               : Error KindInferError : Error TypeConvertError
               : ConsQueryEffects (Rock Query : r)))
     (Declaration SourceRegion Typed)
forall a t. (HasCallStack, IsText t) => t -> a
error (Text
 -> Eff
      (State InferState
         : InferEffectsCons
             SourceRegion
             (Error (UnifyError SourceRegion)
                : Error KindInferError : Error TypeConvertError
                : ConsQueryEffects (Rock Query : r)))
      (Declaration SourceRegion Typed))
-> Text
-> Eff
     (State InferState
        : InferEffectsCons
            SourceRegion
            (Error (UnifyError SourceRegion)
               : Error KindInferError : Error TypeConvertError
               : ConsQueryEffects (Rock Query : r)))
     (Declaration SourceRegion Typed)
forall a b. (a -> b) -> a -> b
$ Text
"Impossible: Declaration " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Qualified Name -> Text
forall b a. (Show a, IsString b) => a -> b
show Qualified Name
name Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
" not found in its own SCC"
        New.TypeDeclarationBody{} -> do
            ModuleName
-> Eff
     (State InferState
        : InferEffectsCons
            SourceRegion
            (Error (UnifyError SourceRegion)
               : Error KindInferError : Error TypeConvertError
               : ConsQueryEffects (Rock Query : r)))
     ()
forall (r :: [(* -> *) -> * -> *]).
(SupportsQuery QueryModuleByName Shunted, HasCallStack,
 Rock Query :> r, DiagnosticWriter (Doc AnsiStyle) :> r,
 Error SomeReportableError :> r, Error KindInferError :> r,
 Error TypeConvertError :> r,
 State (TypeEnvironment SourceRegion) :> r, State InferState :> r,
 Concurrent :> r, UniqueGen :> r, FileSystem :> r,
 StructuredDebug :> r) =>
ModuleName -> Eff r ()
seedConstructorsFor (Qualified Name -> ModuleName
forall name. Qualified name -> ModuleName
qualifier Qualified Name
name)
            Declaration SourceRegion Shunted
-> Eff
     (State InferState
        : InferEffectsCons
            SourceRegion
            (Error (UnifyError SourceRegion)
               : Error KindInferError : Error TypeConvertError
               : ConsQueryEffects (Rock Query : r)))
     (Declaration SourceRegion Typed)
forall (r :: [(* -> *) -> * -> *]).
(HasCallStack, InferPipelineEffects r, Infer SourceRegion r) =>
Declaration SourceRegion Shunted
-> Eff r (Declaration SourceRegion Typed)
inferDeclaration Declaration SourceRegion Shunted
shuntedDecl
        New.DeclBodyExtension DeclBodyExtension Shunted SourceRegion
v -> Void
-> Eff
     (State InferState
        : InferEffectsCons
            SourceRegion
            (Error (UnifyError SourceRegion)
               : Error KindInferError : Error TypeConvertError
               : ConsQueryEffects (Rock Query : r)))
     (Declaration SourceRegion Typed)
forall a. Void -> a
absurd Void
DeclBodyExtension Shunted SourceRegion
v

    pure typedDecl

-- | Get the name from a typed declaration
declarationName :: New.Declaration SourceRegion Typed -> Name
declarationName :: Declaration SourceRegion Typed -> Name
declarationName (New.Declaration SourceRegion
_ (New.Declaration' Locate SourceRegion ModuleName
_ (New.DeclarationBody SourceRegion
_ DeclarationBody' SourceRegion Typed
body'))) =
    case DeclarationBody' SourceRegion Typed
body' of
        New.ValueDeclaration TopValueBinder Typed SourceRegion
n TypedExpr
_ ValueDeclPatterns Typed SourceRegion
_ ValueDeclTypeAnnotation Typed SourceRegion
_ ValueDeclMetadata Typed SourceRegion
_ [Annotation SourceRegion Typed]
_ -> Qualified VarName -> Name
forall name. ToName name => name -> Name
toName (Located (Qualified VarName)
TopValueBinder Typed SourceRegion
n Located (Qualified VarName)
-> Optic'
     A_Lens NoIx (Located (Qualified VarName)) (Qualified VarName)
-> Qualified VarName
forall k s (is :: IxList) a.
Is k A_Getter =>
s -> Optic' k is s a -> a
^. Optic'
  A_Lens NoIx (Located (Qualified VarName)) (Qualified VarName)
forall a b. Lens (Located a) (Located b) a b
unlocated)
        New.TypeDeclarationBody TopTypeBinder Typed SourceRegion
n [TypeVariable Typed SourceRegion]
_ TypeDeclaration SourceRegion Typed
_ Maybe (Type SourceRegion Typed)
_ TypeDeclMetadata Typed SourceRegion
_ [Annotation SourceRegion Typed]
_ -> Qualified TypeName -> Name
forall name. ToName name => name -> Name
toName (Located (Qualified TypeName)
TopTypeBinder Typed SourceRegion
n Located (Qualified TypeName)
-> Lens
     (Located (Qualified TypeName))
     (Located (Qualified TypeName))
     (Qualified TypeName)
     (Qualified TypeName)
-> Qualified TypeName
forall k s (is :: IxList) a.
Is k A_Getter =>
s -> Optic' k is s a -> a
^. Lens
  (Located (Qualified TypeName))
  (Located (Qualified TypeName))
  (Qualified TypeName)
  (Qualified TypeName)
forall a b. Lens (Located a) (Located b) a b
unlocated)
        New.DeclBodyExtension DeclBodyExtension Typed SourceRegion
v -> Void -> Name
forall a. Void -> a
absurd Void
DeclBodyExtension Typed SourceRegion
v

-- | Collect all constructor references from a shunted expression
collectConstructors :: NewS.ShuntedExpr -> [Qualified TypeName]
collectConstructors :: Expr SourceRegion Shunted -> [Qualified TypeName]
collectConstructors (New.Expr SourceRegion
_ ExpressionMeta Shunted SourceRegion
_ Expr' SourceRegion Shunted
e') = case Expr' SourceRegion Shunted
e' of
    New.ECon ConstructorNodeExtension Shunted
_ (Located SourceRegion
_ Qualified TypeName
qtn) -> [Qualified TypeName
qtn]
    New.EVar VariableExtension Shunted
_ ValueOccurrence Shunted SourceRegion
_ -> []
    New.EInt Integer
_ -> []
    New.EFloat Double
_ -> []
    New.EString Text
_ -> []
    New.EChar Char
_ -> []
    Expr' SourceRegion Shunted
New.EUnit -> []
    New.ELam LambdaExtension Shunted
_ LambdaBinder Shunted SourceRegion
_ Expr SourceRegion Shunted
body -> Expr SourceRegion Shunted -> [Qualified TypeName]
collectConstructors Expr SourceRegion Shunted
body
    New.EApp ApplicationExtension Shunted
_ Expr SourceRegion Shunted
f Expr SourceRegion Shunted
x -> Expr SourceRegion Shunted -> [Qualified TypeName]
collectConstructors Expr SourceRegion Shunted
f [Qualified TypeName]
-> [Qualified TypeName] -> [Qualified TypeName]
forall a. Semigroup a => a -> a -> a
<> Expr SourceRegion Shunted -> [Qualified TypeName]
collectConstructors Expr SourceRegion Shunted
x
    New.ETyApp Expr SourceRegion Shunted
e Type SourceRegion Shunted
_ -> Expr SourceRegion Shunted -> [Qualified TypeName]
collectConstructors Expr SourceRegion Shunted
e
    New.EIf Expr SourceRegion Shunted
c Expr SourceRegion Shunted
t Expr SourceRegion Shunted
f -> Expr SourceRegion Shunted -> [Qualified TypeName]
collectConstructors Expr SourceRegion Shunted
c [Qualified TypeName]
-> [Qualified TypeName] -> [Qualified TypeName]
forall a. Semigroup a => a -> a -> a
<> Expr SourceRegion Shunted -> [Qualified TypeName]
collectConstructors Expr SourceRegion Shunted
t [Qualified TypeName]
-> [Qualified TypeName] -> [Qualified TypeName]
forall a. Semigroup a => a -> a -> a
<> Expr SourceRegion Shunted -> [Qualified TypeName]
collectConstructors Expr SourceRegion Shunted
f
    New.EMatch Expr SourceRegion Shunted
e [(Pattern SourceRegion Shunted, Expr SourceRegion Shunted)]
cases -> Expr SourceRegion Shunted -> [Qualified TypeName]
collectConstructors Expr SourceRegion Shunted
e [Qualified TypeName]
-> [Qualified TypeName] -> [Qualified TypeName]
forall a. Semigroup a => a -> a -> a
<> ((Pattern SourceRegion Shunted, Expr SourceRegion Shunted)
 -> [Qualified TypeName])
-> [(Pattern SourceRegion Shunted, Expr SourceRegion Shunted)]
-> [Qualified TypeName]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (\(Pattern SourceRegion Shunted
p, Expr SourceRegion Shunted
b) -> Pattern SourceRegion Shunted -> [Qualified TypeName]
collectPatternConstructors Pattern SourceRegion Shunted
p [Qualified TypeName]
-> [Qualified TypeName] -> [Qualified TypeName]
forall a. Semigroup a => a -> a -> a
<> Expr SourceRegion Shunted -> [Qualified TypeName]
collectConstructors Expr SourceRegion Shunted
b) [(Pattern SourceRegion Shunted, Expr SourceRegion Shunted)]
cases
    New.ELetIn LetExtension Shunted
_ ValueBinder Shunted SourceRegion
_ Expr SourceRegion Shunted
e1 Expr SourceRegion Shunted
e2 -> Expr SourceRegion Shunted -> [Qualified TypeName]
collectConstructors Expr SourceRegion Shunted
e1 [Qualified TypeName]
-> [Qualified TypeName] -> [Qualified TypeName]
forall a. Semigroup a => a -> a -> a
<> Expr SourceRegion Shunted -> [Qualified TypeName]
collectConstructors Expr SourceRegion Shunted
e2
    New.ELet LetExtension Shunted
_ ValueBinder Shunted SourceRegion
_ Expr SourceRegion Shunted
e1 -> Expr SourceRegion Shunted -> [Qualified TypeName]
collectConstructors Expr SourceRegion Shunted
e1
    New.EBlock NonEmpty (Expr SourceRegion Shunted)
exprs -> (Expr SourceRegion Shunted -> [Qualified TypeName])
-> [Expr SourceRegion Shunted] -> [Qualified TypeName]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Expr SourceRegion Shunted -> [Qualified TypeName]
collectConstructors (NonEmpty (Expr SourceRegion Shunted) -> [Expr SourceRegion Shunted]
forall a. NonEmpty a -> [a]
forall (t :: * -> *) a. Foldable t => t a -> [a]
toList NonEmpty (Expr SourceRegion Shunted)
exprs)
    New.EAnn Expr SourceRegion Shunted
e Type SourceRegion Shunted
_ -> Expr SourceRegion Shunted -> [Qualified TypeName]
collectConstructors Expr SourceRegion Shunted
e
    New.EExtension ExpressionExtension Shunted SourceRegion
v -> Void -> [Qualified TypeName]
forall a. Void -> a
absurd Void
ExpressionExtension Shunted SourceRegion
v

-- | Collect constructor references from a shunted pattern
collectPatternConstructors :: NewS.ShuntedPattern -> [Qualified TypeName]
collectPatternConstructors :: Pattern SourceRegion Shunted -> [Qualified TypeName]
collectPatternConstructors (New.Pattern SourceRegion
_ PatternMeta Shunted SourceRegion
_ Pattern' SourceRegion Shunted
p') = case Pattern' SourceRegion Shunted
p' of
    New.PCon (Located SourceRegion
_ Qualified TypeName
qtn) [Pattern SourceRegion Shunted]
pats -> Qualified TypeName
qtn Qualified TypeName -> [Qualified TypeName] -> [Qualified TypeName]
forall a. a -> [a] -> [a]
: (Pattern SourceRegion Shunted -> [Qualified TypeName])
-> [Pattern SourceRegion Shunted] -> [Qualified TypeName]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Pattern SourceRegion Shunted -> [Qualified TypeName]
collectPatternConstructors [Pattern SourceRegion Shunted]
pats
    Pattern' SourceRegion Shunted
_ -> []

inferModule ::
    forall r.
    (InferPipelineEffects r, Infer SourceRegion r) =>
    NewModule.Module SourceRegion Shunted ->
    Eff r (NewModule.Module SourceRegion Typed)
inferModule :: forall (r :: [(* -> *) -> * -> *]).
(InferPipelineEffects r, Infer SourceRegion r) =>
Module SourceRegion Shunted -> Eff r (Module SourceRegion Typed)
inferModule (NewModule.Module SourceRegion
loc Module' SourceRegion Shunted
m') = do
    typedDecls <- (Declaration SourceRegion Shunted
 -> Eff r (Declaration SourceRegion Typed))
-> [Declaration SourceRegion Shunted]
-> Eff r [Declaration SourceRegion Typed]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> [a] -> f [b]
traverse Declaration SourceRegion Shunted
-> Eff r (Declaration SourceRegion Typed)
forall (r :: [(* -> *) -> * -> *]).
(HasCallStack, InferPipelineEffects r, Infer SourceRegion r) =>
Declaration SourceRegion Shunted
-> Eff r (Declaration SourceRegion Typed)
inferDeclaration Module' SourceRegion Shunted
m'.moduleDeclarations
    let typedExposing = Exposing SourceRegion Shunted -> Exposing SourceRegion Typed
forall a b. PhaseCoerce a b => a -> b
phaseCoerce Module' SourceRegion Shunted
m'.moduleExposing :: NewModule.Exposing SourceRegion Typed
        typedImports = [Import SourceRegion Shunted] -> [Import SourceRegion Typed]
forall a b. PhaseCoerce a b => a -> b
phaseCoerce Module' SourceRegion Shunted
m'.moduleImports :: [NewModule.Import SourceRegion Typed]
    pure $ NewModule.Module loc $ NewModule.Module' m'.moduleName typedExposing typedImports typedDecls

-- | Add's a declaration's name and expected type to the type environment
seedDeclaration ::
    _ =>
    New.Declaration SourceRegion Shunted -> Eff r ()
seedDeclaration :: Declaration SourceRegion Shunted -> Eff r ()
seedDeclaration (New.Declaration SourceRegion
_ (New.Declaration' Locate SourceRegion ModuleName
_ (New.DeclarationBody SourceRegion
_ DeclarationBody' SourceRegion Shunted
body'))) =
    case DeclarationBody' SourceRegion Shunted
body' of
        New.ValueDeclaration TopValueBinder Shunted SourceRegion
valueName Expr SourceRegion Shunted
_ ValueDeclPatterns Shunted SourceRegion
_ ValueDeclTypeAnnotation Shunted SourceRegion
_ ValueDeclMetadata Shunted SourceRegion
valueType [Annotation SourceRegion Shunted]
_ -> Doc AnsiStyle -> Eff r () -> Eff r ()
forall (r :: [(* -> *) -> * -> *]) a.
(HasCallStack, StructuredDebug :> r) =>
Doc AnsiStyle -> Eff r a -> Eff r a
logDebugWith (Doc AnsiStyle
"seedDeclaration: Value " Doc AnsiStyle -> Doc AnsiStyle -> Doc AnsiStyle
forall a. Semigroup a => a -> a -> a
<> Located (Qualified VarName) -> Doc AnsiStyle
forall a. Pretty a => a -> Doc AnsiStyle
pretty Located (Qualified VarName)
TopValueBinder Shunted SourceRegion
valueName) (Eff r () -> Eff r ()) -> Eff r () -> Eff r ()
forall a b. (a -> b) -> a -> b
$ do
            expectedType <- (Type SourceRegion Shunted -> Eff r (Type SourceRegion))
-> Maybe (Type SourceRegion Shunted)
-> Eff r (Maybe (Type SourceRegion))
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Maybe a -> f (Maybe b)
traverse (Type SourceRegion Shunted -> Eff r (Type SourceRegion Kinded)
forall (r :: [(* -> *) -> * -> *]).
KindInfer r =>
Type SourceRegion Shunted -> Eff r (Type SourceRegion Kinded)
inferTypeKind (Type SourceRegion Shunted -> Eff r (Type SourceRegion Kinded))
-> (Type SourceRegion Kinded -> Eff r (Type SourceRegion))
-> Type SourceRegion Shunted
-> Eff r (Type SourceRegion)
forall (m :: * -> *) a b c.
Monad m =>
(a -> m b) -> (b -> m c) -> a -> m c
>=> Type SourceRegion Kinded -> Eff r (Type SourceRegion)
forall (r :: [(* -> *) -> * -> *]).
(Error TypeConvertError :> r) =>
Type SourceRegion Kinded -> Eff r (Type SourceRegion)
astTypeToGeneralisedInferType) Maybe (Type SourceRegion Shunted)
ValueDeclMetadata Shunted SourceRegion
valueType
            logDebug $ "Expected type for " <> pretty valueName <> ": " <> pretty expectedType
            expected <- case expectedType of
                Just Type SourceRegion
t -> Type SourceRegion -> Eff r (Type SourceRegion)
forall a. a -> Eff r a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Type SourceRegion
t
                Maybe (Type SourceRegion)
Nothing -> Monotype SourceRegion -> Type SourceRegion
forall loc. Monotype loc -> Type loc
Lifted (Monotype SourceRegion -> Type SourceRegion)
-> (UniqueTyVar -> Monotype SourceRegion)
-> UniqueTyVar
-> Type SourceRegion
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SourceRegion -> TypeVariable -> Monotype SourceRegion
forall loc. loc -> TypeVariable -> Monotype loc
TypeVar (Located (Qualified VarName)
TopValueBinder Shunted SourceRegion
valueName Located (Qualified VarName)
-> Optic' A_Lens NoIx (Located (Qualified VarName)) SourceRegion
-> SourceRegion
forall k s (is :: IxList) a.
Is k A_Getter =>
s -> Optic' k is s a -> a
^. Optic' A_Lens NoIx (Located (Qualified VarName)) SourceRegion
forall a. HasSourceRegion a => Lens' a SourceRegion
sourceRegion) (TypeVariable -> Monotype SourceRegion)
-> (UniqueTyVar -> TypeVariable)
-> UniqueTyVar
-> Monotype SourceRegion
forall b c a. (b -> c) -> (a -> b) -> a -> c
. UniqueTyVar -> TypeVariable
UnificationVar (UniqueTyVar -> Type SourceRegion)
-> Eff r UniqueTyVar -> Eff r (Type SourceRegion)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Eff r UniqueTyVar
forall (r :: [(* -> *) -> * -> *]).
(UniqueGen :> r) =>
Eff r UniqueTyVar
makeUniqueTyVar
            -- When we have an expected type (e.g., from a user annotation), skolemise
            -- its quantified variables so they cannot unify with concrete types.
            expectedAsMono <- skolemise expected
            logDebug $ "Skolemised expected type of" <+> pretty valueName <+> ": " <> pretty expectedAsMono
            addType' (TermVarKey (valueName ^. unlocated)) expected
        DeclarationBody' SourceRegion Shunted
_ -> Eff r ()
forall (f :: * -> *). Applicative f => f ()
pass -- TODO

inferDeclarationScheme :: _ => New.Declaration SourceRegion Shunted -> Eff r (Polytype SourceRegion)
inferDeclarationScheme :: Declaration SourceRegion Shunted -> Eff r (Polytype SourceRegion)
inferDeclarationScheme (New.Declaration SourceRegion
_ (New.Declaration' Locate SourceRegion ModuleName
_ (New.DeclarationBody SourceRegion
_ DeclarationBody' SourceRegion Shunted
body'))) = case DeclarationBody' SourceRegion Shunted
body' of
    New.ValueDeclaration TopValueBinder Shunted SourceRegion
valueName Expr SourceRegion Shunted
valueExpr ValueDeclPatterns Shunted SourceRegion
_ ValueDeclTypeAnnotation Shunted SourceRegion
_ ValueDeclMetadata Shunted SourceRegion
_ [Annotation SourceRegion Shunted]
_ -> Doc AnsiStyle
-> Eff r (Polytype SourceRegion) -> Eff r (Polytype SourceRegion)
forall (r :: [(* -> *) -> * -> *]) a.
(HasCallStack, StructuredDebug :> r) =>
Doc AnsiStyle -> Eff r a -> Eff r a
logDebugWith (Doc AnsiStyle
"inferDeclarationScheme: " Doc AnsiStyle -> Doc AnsiStyle -> Doc AnsiStyle
forall a. Semigroup a => a -> a -> a
<> Located (Qualified VarName) -> Doc AnsiStyle
forall a. Pretty a => a -> Doc AnsiStyle
pretty Located (Qualified VarName)
TopValueBinder Shunted SourceRegion
valueName) (Eff r (Polytype SourceRegion) -> Eff r (Polytype SourceRegion))
-> Eff r (Polytype SourceRegion) -> Eff r (Polytype SourceRegion)
forall a b. (a -> b) -> a -> b
$ do
        expectedType <- TypeEnvKey SourceRegion -> Eff r (Type SourceRegion)
forall (r :: [(* -> *) -> * -> *]) loc.
(StructuredDebug :> r, QueryEffects r, loc ~ SourceRegion,
 Rock Query :> r, State (TypeEnvironment loc) :> r) =>
TypeEnvKey loc -> Eff r (Type loc)
lookupType (Qualified VarName -> TypeEnvKey SourceRegion
forall {k} (loc :: k). Qualified VarName -> TypeEnvKey loc
TermVarKey (Located (Qualified VarName)
TopValueBinder Shunted SourceRegion
valueName Located (Qualified VarName)
-> Optic'
     A_Lens NoIx (Located (Qualified VarName)) (Qualified VarName)
-> Qualified VarName
forall k s (is :: IxList) a.
Is k A_Getter =>
s -> Optic' k is s a -> a
^. Optic'
  A_Lens NoIx (Located (Qualified VarName)) (Qualified VarName)
forall a b. Lens (Located a) (Located b) a b
unlocated))
        (_, polytype) <- inferValue (valueName ^. unlocated) valueExpr (Just expectedType)
        addType' (TermVarKey (valueName ^. unlocated)) (Polytype polytype)
        logDebug $ "Inferred type for " <> pretty valueName <> ": " <> pretty polytype
        pure polytype
    DeclarationBody' SourceRegion Shunted
_ -> Text -> Eff r (Polytype SourceRegion)
forall a t. (HasCallStack, IsText t) => t -> a
error Text
"only value declarations are supported currently"

inferDeclaration ::
    forall r.
    (HasCallStack, InferPipelineEffects r, Infer SourceRegion r) =>
    New.Declaration SourceRegion Shunted ->
    Eff r (New.Declaration SourceRegion Typed)
inferDeclaration :: forall (r :: [(* -> *) -> * -> *]).
(HasCallStack, InferPipelineEffects r, Infer SourceRegion r) =>
Declaration SourceRegion Shunted
-> Eff r (Declaration SourceRegion Typed)
inferDeclaration (New.Declaration SourceRegion
dloc (New.Declaration' Locate SourceRegion ModuleName
mn (New.DeclarationBody SourceRegion
bloc DeclarationBody' SourceRegion Shunted
body'))) = do
    typedBody' <- HasCallStack =>
DeclarationBody' SourceRegion Shunted
-> Eff r (DeclarationBody' SourceRegion Typed)
DeclarationBody' SourceRegion Shunted
-> Eff r (DeclarationBody' SourceRegion Typed)
inferDeclarationBody' DeclarationBody' SourceRegion Shunted
body'
    pure $ New.Declaration dloc (New.Declaration' mn (New.DeclarationBody bloc typedBody'))
  where
    inferDeclarationBody' ::
        HasCallStack =>
        New.DeclarationBody' SourceRegion Shunted ->
        Eff r (New.DeclarationBody' SourceRegion Typed)
    inferDeclarationBody' :: HasCallStack =>
DeclarationBody' SourceRegion Shunted
-> Eff r (DeclarationBody' SourceRegion Typed)
inferDeclarationBody' = \case
        New.ValueDeclaration TopValueBinder Shunted SourceRegion
name Expr SourceRegion Shunted
e () () ValueDeclMetadata Shunted SourceRegion
_valueTypeMeta [Annotation SourceRegion Shunted]
anns -> do
            expectedType <- (Type SourceRegion Shunted -> Eff r (Type SourceRegion))
-> Maybe (Type SourceRegion Shunted)
-> Eff r (Maybe (Type SourceRegion))
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Maybe a -> f (Maybe b)
traverse (Type SourceRegion Shunted -> Eff r (Type SourceRegion Kinded)
forall (r :: [(* -> *) -> * -> *]).
KindInfer r =>
Type SourceRegion Shunted -> Eff r (Type SourceRegion Kinded)
inferTypeKind (Type SourceRegion Shunted -> Eff r (Type SourceRegion Kinded))
-> (Type SourceRegion Kinded -> Eff r (Type SourceRegion))
-> Type SourceRegion Shunted
-> Eff r (Type SourceRegion)
forall (m :: * -> *) a b c.
Monad m =>
(a -> m b) -> (b -> m c) -> a -> m c
>=> Type SourceRegion Kinded -> Eff r (Type SourceRegion)
forall (r :: [(* -> *) -> * -> *]).
(Error TypeConvertError :> r) =>
Type SourceRegion Kinded -> Eff r (Type SourceRegion)
astTypeToGeneralisedInferType) Maybe (Type SourceRegion Shunted)
ValueDeclMetadata Shunted SourceRegion
_valueTypeMeta
            logDebug $ "Expected type for " <> pretty name <> ": " <> pretty expectedType
            (typedExpr, polytype) <- inferValue (name ^. unlocated) e expectedType
            logDebug $ "Inferred type for " <> pretty name <> ": " <> pretty polytype
            addType' (TermVarKey (name ^. unlocated)) (Polytype polytype)
            typedAnns <- traverse inferAnnotation anns

            pure (New.ValueDeclaration name typedExpr () () (Polytype polytype) typedAnns)
        New.TypeDeclarationBody TopTypeBinder Shunted SourceRegion
name [TypeVariable Shunted SourceRegion]
tyVars TypeDeclaration SourceRegion Shunted
bodyDecl Maybe (Type SourceRegion Shunted)
_mKind TypeDeclMetadata Shunted SourceRegion
NoExtension
NoExtension [Annotation SourceRegion Shunted]
anns -> do
            (kind, decl') <- Qualified TypeName
-> [Located (Unique LowerAlphaName)]
-> TypeDeclaration SourceRegion Shunted
-> Eff r (ElaraKind, KindedTypeDeclaration)
forall (r :: [(* -> *) -> * -> *]).
(HasCallStack, State InferState :> r, Error KindInferError :> r,
 Error SomeReportableError :> r,
 DiagnosticWriter (Doc AnsiStyle) :> r, Rock Query :> r,
 StructuredDebug :> r, UniqueGen :> r, FileSystem :> r,
 Concurrent :> r) =>
Qualified TypeName
-> [Located (Unique LowerAlphaName)]
-> TypeDeclaration SourceRegion Shunted
-> Eff r (ElaraKind, KindedTypeDeclaration)
inferKind (Located (Qualified TypeName)
TopTypeBinder Shunted SourceRegion
name Located (Qualified TypeName)
-> Lens
     (Located (Qualified TypeName))
     (Located (Qualified TypeName))
     (Qualified TypeName)
     (Qualified TypeName)
-> Qualified TypeName
forall k s (is :: IxList) a.
Is k A_Getter =>
s -> Optic' k is s a -> a
^. Lens
  (Located (Qualified TypeName))
  (Located (Qualified TypeName))
  (Qualified TypeName)
  (Qualified TypeName)
forall a b. Lens (Located a) (Located b) a b
unlocated) [Located (Unique LowerAlphaName)]
[TypeVariable Shunted SourceRegion]
tyVars TypeDeclaration SourceRegion Shunted
bodyDecl
            case decl' of
                New.Alias Type SourceRegion Kinded
t -> do
                    _ <- Type SourceRegion Kinded
-> Eff r (Monotype SourceRegion, ElaraKind)
forall (r :: [(* -> *) -> * -> *]).
(Error TypeConvertError :> r) =>
Type SourceRegion Kinded
-> Eff r (Monotype SourceRegion, ElaraKind)
astTypeToInferTypeWithKind Type SourceRegion Kinded
t
                    let tyVars' = (Located (Unique LowerAlphaName) -> UniqueTyVar)
-> [Located (Unique LowerAlphaName)]
-> [(Located (Unique LowerAlphaName), UniqueTyVar)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f (a, b)
fmapToSnd Located (Unique LowerAlphaName) -> UniqueTyVar
createTypeVar [Located (Unique LowerAlphaName)]
[TypeVariable Shunted SourceRegion]
tyVars

                    typedAnns <- traverse inferAnnotation anns

                    pure
                        ( New.TypeDeclarationBody
                            name
                            (zipWith (<$) (snd <$> tyVars') tyVars)
                            (kindedToTypedTypeDecl decl')
                            Nothing -- TODO: kind
                            kind
                            typedAnns
                        )
                New.ADT NonEmpty
  (ConstructorBinder Kinded SourceRegion, [Type SourceRegion Kinded])
ctors -> do
                    let tyVars' :: [(Located (Unique LowerAlphaName), UniqueTyVar)]
tyVars' = (Located (Unique LowerAlphaName) -> UniqueTyVar)
-> [Located (Unique LowerAlphaName)]
-> [(Located (Unique LowerAlphaName), UniqueTyVar)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f (a, b)
fmapToSnd Located (Unique LowerAlphaName) -> UniqueTyVar
createTypeVar [Located (Unique LowerAlphaName)]
[TypeVariable Shunted SourceRegion]
tyVars
                    let typeConstructorType :: Monotype SourceRegion
typeConstructorType = SourceRegion
-> Qualified TypeName
-> [Monotype SourceRegion]
-> Monotype SourceRegion
forall loc.
loc -> Qualified TypeName -> [Monotype loc] -> Monotype loc
TypeConstructor (Located (Qualified TypeName)
TopTypeBinder Shunted SourceRegion
name Located (Qualified TypeName)
-> Optic' A_Lens NoIx (Located (Qualified TypeName)) SourceRegion
-> SourceRegion
forall k s (is :: IxList) a.
Is k A_Getter =>
s -> Optic' k is s a -> a
^. Optic' A_Lens NoIx (Located (Qualified TypeName)) SourceRegion
forall a. HasSourceRegion a => Lens' a SourceRegion
sourceRegion) (Located (Qualified TypeName)
TopTypeBinder Shunted SourceRegion
name Located (Qualified TypeName)
-> Lens
     (Located (Qualified TypeName))
     (Located (Qualified TypeName))
     (Qualified TypeName)
     (Qualified TypeName)
-> Qualified TypeName
forall k s (is :: IxList) a.
Is k A_Getter =>
s -> Optic' k is s a -> a
^. Lens
  (Located (Qualified TypeName))
  (Located (Qualified TypeName))
  (Qualified TypeName)
  (Qualified TypeName)
forall a b. Lens (Located a) (Located b) a b
unlocated) (((Located (Unique LowerAlphaName), UniqueTyVar)
 -> Monotype SourceRegion)
-> [(Located (Unique LowerAlphaName), UniqueTyVar)]
-> [Monotype SourceRegion]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\(Located (Unique LowerAlphaName)
tyVarLocation, UniqueTyVar
tyVar) -> SourceRegion -> TypeVariable -> Monotype SourceRegion
forall loc. loc -> TypeVariable -> Monotype loc
TypeVar (Located (Unique LowerAlphaName)
tyVarLocation Located (Unique LowerAlphaName)
-> Optic'
     A_Lens NoIx (Located (Unique LowerAlphaName)) SourceRegion
-> SourceRegion
forall k s (is :: IxList) a.
Is k A_Getter =>
s -> Optic' k is s a -> a
^. Optic' A_Lens NoIx (Located (Unique LowerAlphaName)) SourceRegion
forall a. HasSourceRegion a => Lens' a SourceRegion
sourceRegion) (TypeVariable -> Monotype SourceRegion)
-> TypeVariable -> Monotype SourceRegion
forall a b. (a -> b) -> a -> b
$ UniqueTyVar -> TypeVariable
UnificationVar UniqueTyVar
tyVar) [(Located (Unique LowerAlphaName), UniqueTyVar)]
tyVars')

                    let inferCtor :: (Located (Qualified TypeName), [Type SourceRegion Kinded])
-> Eff
     r
     (Located (Qualified TypeName),
      [(Monotype SourceRegion, ElaraKind)])
inferCtor (Located (Qualified TypeName)
ctorName, [Type SourceRegion Kinded]
t :: [KindedType]) = do
                            t' <- (Type SourceRegion Kinded
 -> Eff r (Monotype SourceRegion, ElaraKind))
-> [Type SourceRegion Kinded]
-> Eff r [(Monotype SourceRegion, ElaraKind)]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> [a] -> f [b]
traverse Type SourceRegion Kinded
-> Eff r (Monotype SourceRegion, ElaraKind)
forall (r :: [(* -> *) -> * -> *]).
(Error TypeConvertError :> r) =>
Type SourceRegion Kinded
-> Eff r (Monotype SourceRegion, ElaraKind)
astTypeToInferTypeWithKind [Type SourceRegion Kinded]
t
                            let ctorType =
                                    ((Monotype SourceRegion, ElaraKind)
 -> Monotype SourceRegion -> Monotype SourceRegion)
-> Monotype SourceRegion
-> [(Monotype SourceRegion, ElaraKind)]
-> Monotype SourceRegion
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (SourceRegion
-> Monotype SourceRegion
-> Monotype SourceRegion
-> Monotype SourceRegion
forall loc. loc -> Monotype loc -> Monotype loc -> Monotype loc
Function (Located (Qualified TypeName)
ctorName Located (Qualified TypeName)
-> Optic' A_Lens NoIx (Located (Qualified TypeName)) SourceRegion
-> SourceRegion
forall k s (is :: IxList) a.
Is k A_Getter =>
s -> Optic' k is s a -> a
^. Optic' A_Lens NoIx (Located (Qualified TypeName)) SourceRegion
forall a. HasSourceRegion a => Lens' a SourceRegion
sourceRegion) (Monotype SourceRegion
 -> Monotype SourceRegion -> Monotype SourceRegion)
-> ((Monotype SourceRegion, ElaraKind) -> Monotype SourceRegion)
-> (Monotype SourceRegion, ElaraKind)
-> Monotype SourceRegion
-> Monotype SourceRegion
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Monotype SourceRegion, ElaraKind) -> Monotype SourceRegion
forall a b. (a, b) -> a
fst) Monotype SourceRegion
typeConstructorType [(Monotype SourceRegion, ElaraKind)]
t'
                            addType' (DataConKey (ctorName ^. unlocated)) (Polytype (Forall (ctorName ^. sourceRegion) (snd <$> tyVars') (EmptyConstraint (monotypeLoc ctorType)) ctorType))

                            pure (ctorName, t')

                    ((Located (Qualified TypeName), [Type SourceRegion Kinded])
 -> Eff
      r
      (Located (Qualified TypeName),
       [(Monotype SourceRegion, ElaraKind)]))
-> NonEmpty
     (Located (Qualified TypeName), [Type SourceRegion Kinded])
-> Eff r ()
forall (t :: * -> *) (f :: * -> *) a b.
(Foldable t, Applicative f) =>
(a -> f b) -> t a -> f ()
traverse_ (Located (Qualified TypeName), [Type SourceRegion Kinded])
-> Eff
     r
     (Located (Qualified TypeName),
      [(Monotype SourceRegion, ElaraKind)])
inferCtor NonEmpty (Located (Qualified TypeName), [Type SourceRegion Kinded])
NonEmpty
  (ConstructorBinder Kinded SourceRegion, [Type SourceRegion Kinded])
ctors
                    typedAnns <- (Annotation SourceRegion Shunted
 -> Eff r (Annotation SourceRegion Typed))
-> [Annotation SourceRegion Shunted]
-> Eff r [Annotation SourceRegion Typed]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> [a] -> f [b]
traverse Annotation SourceRegion Shunted
-> Eff r (Annotation SourceRegion Typed)
forall (r :: [(* -> *) -> * -> *]).
(Error (UnifyError SourceRegion) :> r,
 Error (InferError SourceRegion) :> r,
 Error SomeReportableError :> r,
 DiagnosticWriter (Doc AnsiStyle) :> r, Rock Query :> r,
 State (TypeEnvironment SourceRegion) :> r,
 State (LocalTypeEnvironment SourceRegion) :> r,
 Reader ContextStack :> r, StructuredDebug :> r, UniqueGen :> r,
 Concurrent :> r, FileSystem :> r) =>
Annotation SourceRegion Shunted
-> Eff r (Annotation SourceRegion Typed)
inferAnnotation [Annotation SourceRegion Shunted]
anns

                    pure
                        ( New.TypeDeclarationBody
                            name
                            (zipWith (<$) (snd <$> tyVars') tyVars)
                            (kindedToTypedTypeDecl decl')
                            Nothing -- TODO: kind
                            kind
                            typedAnns
                        )
        New.DeclBodyExtension DeclBodyExtension Shunted SourceRegion
v -> Void -> Eff r (DeclarationBody' SourceRegion Typed)
forall a. Void -> a
absurd Void
DeclBodyExtension Shunted SourceRegion
v

createTypeVar :: Located (Unique LowerAlphaName) -> UniqueTyVar
createTypeVar :: Located (Unique LowerAlphaName) -> UniqueTyVar
createTypeVar (Located SourceRegion
_ Unique LowerAlphaName
u) = (LowerAlphaName -> Maybe Text)
-> Unique LowerAlphaName -> UniqueTyVar
forall a b. (a -> b) -> Unique a -> Unique b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Text -> Maybe Text
forall a. a -> Maybe a
Just (Text -> Maybe Text)
-> (LowerAlphaName -> Text) -> LowerAlphaName -> Maybe Text
forall b c a. (b -> c) -> (a -> b) -> a -> c
. LowerAlphaName -> Text
forall name. NameLike name => name -> Text
nameText) Unique LowerAlphaName
u

{- | Convert a kinded type declaration to a typed type declaration
The only difference is the TypeVariable: Kinded uses Located (Unique LowerAlphaName),
Typed uses Located UniqueTyVar. TypeMeta and ConstructorBinder are the same.
-}
kindedToTypedTypeDecl :: New.TypeDeclaration SourceRegion NewK.Kinded -> New.TypeDeclaration SourceRegion Typed
kindedToTypedTypeDecl :: KindedTypeDeclaration -> TypeDeclaration SourceRegion Typed
kindedToTypedTypeDecl (New.ADT NonEmpty
  (ConstructorBinder Kinded SourceRegion, [Type SourceRegion Kinded])
ctors) = NonEmpty
  (ConstructorBinder Typed SourceRegion, [Type SourceRegion Typed])
-> TypeDeclaration SourceRegion Typed
forall {k} loc (p :: k).
NonEmpty (ConstructorBinder p loc, [Type loc p])
-> TypeDeclaration loc p
New.ADT (([Type SourceRegion Kinded] -> [Type SourceRegion Typed])
-> NonEmpty
     (Located (Qualified TypeName), [Type SourceRegion Kinded])
-> NonEmpty
     (Located (Qualified TypeName), [Type SourceRegion Typed])
forall (f :: * -> *) (p :: * -> * -> *) b d a.
(Functor f, Bifunctor p) =>
(b -> d) -> f (p a b) -> f (p a d)
secondF ((Type SourceRegion Kinded -> Type SourceRegion Typed)
-> [Type SourceRegion Kinded] -> [Type SourceRegion Typed]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Type SourceRegion Kinded -> Type SourceRegion Typed
kindedToTypedType) NonEmpty (Located (Qualified TypeName), [Type SourceRegion Kinded])
NonEmpty
  (ConstructorBinder Kinded SourceRegion, [Type SourceRegion Kinded])
ctors)
kindedToTypedTypeDecl (New.Alias Type SourceRegion Kinded
t) = Type SourceRegion Typed -> TypeDeclaration SourceRegion Typed
forall {k} loc (p :: k). Type loc p -> TypeDeclaration loc p
New.Alias (Type SourceRegion Kinded -> Type SourceRegion Typed
kindedToTypedType Type SourceRegion Kinded
t)

kindedToTypedType :: New.Type SourceRegion NewK.Kinded -> New.Type SourceRegion Typed
kindedToTypedType :: Type SourceRegion Kinded -> Type SourceRegion Typed
kindedToTypedType (New.Type SourceRegion
loc TypeMeta Kinded SourceRegion
meta Type' SourceRegion Kinded
t') = SourceRegion
-> TypeMeta Typed SourceRegion
-> Type' SourceRegion Typed
-> Type SourceRegion Typed
forall {k} loc (p :: k).
loc -> TypeMeta p loc -> Type' loc p -> Type loc p
New.Type SourceRegion
loc TypeMeta Kinded SourceRegion
TypeMeta Typed SourceRegion
meta (Type' SourceRegion Kinded -> Type' SourceRegion Typed
kindedToTypedType' Type' SourceRegion Kinded
t')

kindedToTypedType' :: New.Type' SourceRegion NewK.Kinded -> New.Type' SourceRegion Typed
kindedToTypedType' :: Type' SourceRegion Kinded -> Type' SourceRegion Typed
kindedToTypedType' = \case
    New.TVar TypeVariable Kinded SourceRegion
v -> TypeVariable Typed SourceRegion -> Type' SourceRegion Typed
forall {k} loc (p :: k). TypeVariable p loc -> Type' loc p
New.TVar ((Text -> Maybe Text
forall a. a -> Maybe a
Just (Text -> Maybe Text)
-> (LowerAlphaName -> Text) -> LowerAlphaName -> Maybe Text
forall b c a. (b -> c) -> (a -> b) -> a -> c
. LowerAlphaName -> Text
forall name. NameLike name => name -> Text
nameText) (LowerAlphaName -> Maybe Text)
-> Located (Unique LowerAlphaName) -> Located UniqueTyVar
forall (f :: * -> *) (g :: * -> *) a b.
(Functor f, Functor g) =>
(a -> b) -> f (g a) -> f (g b)
<<$>> Located (Unique LowerAlphaName)
TypeVariable Kinded SourceRegion
v)
    New.TFun Type SourceRegion Kinded
t1 Type SourceRegion Kinded
t2 -> Type SourceRegion Typed
-> Type SourceRegion Typed -> Type' SourceRegion Typed
forall {k} loc (p :: k). Type loc p -> Type loc p -> Type' loc p
New.TFun (Type SourceRegion Kinded -> Type SourceRegion Typed
kindedToTypedType Type SourceRegion Kinded
t1) (Type SourceRegion Kinded -> Type SourceRegion Typed
kindedToTypedType Type SourceRegion Kinded
t2)
    Type' SourceRegion Kinded
New.TUnit -> Type' SourceRegion Typed
forall {k} loc (p :: k). Type' loc p
New.TUnit
    New.TApp Type SourceRegion Kinded
t1 Type SourceRegion Kinded
t2 -> Type SourceRegion Typed
-> Type SourceRegion Typed -> Type' SourceRegion Typed
forall {k} loc (p :: k). Type loc p -> Type loc p -> Type' loc p
New.TApp (Type SourceRegion Kinded -> Type SourceRegion Typed
kindedToTypedType Type SourceRegion Kinded
t1) (Type SourceRegion Kinded -> Type SourceRegion Typed
kindedToTypedType Type SourceRegion Kinded
t2)
    New.TUserDefined TypeOccurrence Kinded SourceRegion
n -> TypeOccurrence Typed SourceRegion -> Type' SourceRegion Typed
forall {k} loc (p :: k). TypeOccurrence p loc -> Type' loc p
New.TUserDefined TypeOccurrence Kinded SourceRegion
TypeOccurrence Typed SourceRegion
n
    New.TRecord NonEmpty
  (Locate SourceRegion LowerAlphaName, Type SourceRegion Kinded)
fields -> NonEmpty
  (Locate SourceRegion LowerAlphaName, Type SourceRegion Typed)
-> Type' SourceRegion Typed
forall {k} loc (p :: k).
NonEmpty (Locate loc LowerAlphaName, Type loc p) -> Type' loc p
New.TRecord ((Type SourceRegion Kinded -> Type SourceRegion Typed)
-> NonEmpty (Located LowerAlphaName, Type SourceRegion Kinded)
-> NonEmpty (Located LowerAlphaName, Type SourceRegion Typed)
forall (f :: * -> *) (p :: * -> * -> *) b d a.
(Functor f, Bifunctor p) =>
(b -> d) -> f (p a b) -> f (p a d)
secondF Type SourceRegion Kinded -> Type SourceRegion Typed
kindedToTypedType NonEmpty (Located LowerAlphaName, Type SourceRegion Kinded)
NonEmpty
  (Locate SourceRegion LowerAlphaName, Type SourceRegion Kinded)
fields)
    New.TList Type SourceRegion Kinded
t -> Type SourceRegion Typed -> Type' SourceRegion Typed
forall {k} loc (p :: k). Type loc p -> Type' loc p
New.TList (Type SourceRegion Kinded -> Type SourceRegion Typed
kindedToTypedType Type SourceRegion Kinded
t)
    New.TExtension TypeSyntaxExtension Kinded SourceRegion
v -> Void -> Type' SourceRegion Typed
forall a. Void -> a
absurd Void
TypeSyntaxExtension Kinded SourceRegion
v

inferAnnotation :: _ => New.Annotation SourceRegion Shunted -> Eff r (New.Annotation SourceRegion Typed)
inferAnnotation :: Annotation SourceRegion Shunted
-> Eff r (Annotation SourceRegion Typed)
inferAnnotation (New.Annotation TypeOccurrence Shunted SourceRegion
name [AnnotationArg SourceRegion Shunted]
args) = do
    args' <-
        (AnnotationArg SourceRegion Shunted
 -> Eff r (AnnotationArg SourceRegion Typed))
-> [AnnotationArg SourceRegion Shunted]
-> Eff r [AnnotationArg SourceRegion Typed]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> [a] -> f [b]
traverse
            AnnotationArg SourceRegion Shunted
-> Eff r (AnnotationArg SourceRegion Typed)
forall (r :: [(* -> *) -> * -> *]).
(Error (UnifyError SourceRegion) :> r,
 Error (InferError SourceRegion) :> r,
 Error SomeReportableError :> r,
 DiagnosticWriter (Doc AnsiStyle) :> r, Rock Query :> r,
 State (TypeEnvironment SourceRegion) :> r,
 State (LocalTypeEnvironment SourceRegion) :> r,
 Reader ContextStack :> r, StructuredDebug :> r, UniqueGen :> r,
 Concurrent :> r, FileSystem :> r) =>
AnnotationArg SourceRegion Shunted
-> Eff r (AnnotationArg SourceRegion Typed)
inferAnnotationArg
            [AnnotationArg SourceRegion Shunted]
args
    pure (New.Annotation name args')

inferAnnotationArg ::
    _ =>
    New.AnnotationArg SourceRegion Shunted ->
    Eff r (New.AnnotationArg SourceRegion Typed)
inferAnnotationArg :: AnnotationArg SourceRegion Shunted
-> Eff r (AnnotationArg SourceRegion Typed)
inferAnnotationArg (New.AnnotationArg Expr SourceRegion Shunted
e) = do
    -- We don't have an expected type for annotation arguments since they are unnamed
    ((typedExpr, t), constraint) <- Eff
  (Writer (Constraint SourceRegion) : r)
  (TypedExpr, Monotype SourceRegion)
-> Eff
     r ((TypedExpr, Monotype SourceRegion), Constraint SourceRegion)
forall w (es :: [(* -> *) -> * -> *]) a.
(HasCallStack, Monoid w) =>
Eff (Writer w : es) a -> Eff es (a, w)
runWriter (Eff
   (Writer (Constraint SourceRegion) : r)
   (TypedExpr, Monotype SourceRegion)
 -> Eff
      r ((TypedExpr, Monotype SourceRegion), Constraint SourceRegion))
-> Eff
     (Writer (Constraint SourceRegion) : r)
     (TypedExpr, Monotype SourceRegion)
-> Eff
     r ((TypedExpr, Monotype SourceRegion), Constraint SourceRegion)
forall a b. (a -> b) -> a -> b
$ Expr SourceRegion Shunted
-> Eff
     (Writer (Constraint SourceRegion) : r)
     (TypedExpr, Monotype SourceRegion)
forall (r :: [(* -> *) -> * -> *]) loc.
ConstraintGenEffects r loc =>
Expr SourceRegion Shunted -> Eff r (TypedExpr, Monotype loc)
generateConstraints Expr SourceRegion Shunted
e

    (finalConstraint, subst) <- solveConstraint mempty (fuv t <> fuv constraint) constraint
    case finalConstraint of
        EmptyConstraint SourceRegion
_ -> Eff r ()
forall (f :: * -> *). Applicative f => f ()
pass
        Constraint SourceRegion
_ -> UnifyError SourceRegion -> Eff r ()
forall e (es :: [(* -> *) -> * -> *]) a.
(HasCallStack, Error e :> es, Show e) =>
e -> Eff es a
throwError (UnifyError SourceRegion -> Eff r ())
-> UnifyError SourceRegion -> Eff r ()
forall a b. (a -> b) -> a -> b
$ Qualified VarName
-> Constraint SourceRegion -> UnifyError SourceRegion
forall loc. Qualified VarName -> Constraint loc -> UnifyError loc
UnresolvedConstraint Qualified VarName
forall a. HasCallStack => a
undefined Constraint SourceRegion
finalConstraint

    pure $ New.AnnotationArg (getExpr (substituteAll subst (SubstitutableExpr typedExpr)))

inferValue ::
    forall r.
    (Error (UnifyError SourceRegion) :> r, _) =>
    Qualified VarName ->
    NewS.ShuntedExpr ->
    Maybe (Type SourceRegion) ->
    Eff r (TypedExpr, Polytype SourceRegion)
inferValue :: Qualified VarName
-> Expr SourceRegion Shunted
-> Maybe (Type SourceRegion)
-> Eff r (TypedExpr, Polytype SourceRegion)
inferValue Qualified VarName
valueName Expr SourceRegion Shunted
valueExpr Maybe (Type SourceRegion)
expectedType = do
    -- generate
    let exprLoc :: SourceRegion
exprLoc = Expr SourceRegion Shunted -> SourceRegion
forall {k} loc (p :: k). Expr loc p -> loc
exprLocation Expr SourceRegion Shunted
valueExpr
    expected <- case Maybe (Type SourceRegion)
expectedType of
        Just Type SourceRegion
t -> Type SourceRegion -> Eff r (Type SourceRegion)
forall a. a -> Eff r a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Type SourceRegion
t
        Maybe (Type SourceRegion)
Nothing -> Monotype SourceRegion -> Type SourceRegion
forall loc. Monotype loc -> Type loc
Lifted (Monotype SourceRegion -> Type SourceRegion)
-> (UniqueTyVar -> Monotype SourceRegion)
-> UniqueTyVar
-> Type SourceRegion
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SourceRegion -> TypeVariable -> Monotype SourceRegion
forall loc. loc -> TypeVariable -> Monotype loc
TypeVar SourceRegion
exprLoc (TypeVariable -> Monotype SourceRegion)
-> (UniqueTyVar -> TypeVariable)
-> UniqueTyVar
-> Monotype SourceRegion
forall b c a. (b -> c) -> (a -> b) -> a -> c
. UniqueTyVar -> TypeVariable
UnificationVar (UniqueTyVar -> Type SourceRegion)
-> Eff r UniqueTyVar -> Eff r (Type SourceRegion)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Eff r UniqueTyVar
forall (r :: [(* -> *) -> * -> *]).
(UniqueGen :> r) =>
Eff r UniqueTyVar
makeUniqueTyVar
    -- When we have an expected type (e.g., from a user annotation), skolemise
    -- its quantified variables so they cannot unify with concrete types.
    expectedAsMono <- skolemise expected
    addType' (TermVarKey valueName) expected
    ((typedExpr, t), constraint) <- runWriter $ generateConstraints valueExpr

    let constraint' = Constraint SourceRegion
constraint Constraint SourceRegion
-> Constraint SourceRegion -> Constraint SourceRegion
forall a. Semigroup a => a -> a -> a
<> SourceRegion
-> Monotype SourceRegion
-> Monotype SourceRegion
-> Constraint SourceRegion
forall loc. loc -> Monotype loc -> Monotype loc -> Constraint loc
simpleEquality (Type SourceRegion -> SourceRegion
forall loc. Type loc -> loc
typeLoc Type SourceRegion
expected) Monotype SourceRegion
expectedAsMono Monotype SourceRegion
t
    let tch = Monotype SourceRegion -> Set UniqueTyVar
forall a. Fuv a => a -> Set UniqueTyVar
fuv Monotype SourceRegion
t Set UniqueTyVar -> Set UniqueTyVar -> Set UniqueTyVar
forall a. Semigroup a => a -> a -> a
<> Constraint SourceRegion -> Set UniqueTyVar
forall a. Fuv a => a -> Set UniqueTyVar
fuv Constraint SourceRegion
constraint'
    logDebug $ "Generated constraints: " <> pretty constraint' <> " for " <> pretty valueName
    logDebug $ "Type: " <> pretty t

    (finalConstraint, subst) <- solveConstraint mempty tch constraint'

    case finalConstraint of
        EmptyConstraint SourceRegion
_ -> Eff r ()
forall (f :: * -> *). Applicative f => f ()
pass
        Constraint SourceRegion
_ -> UnifyError SourceRegion -> Eff r ()
forall e (es :: [(* -> *) -> * -> *]) a.
(HasCallStack, Error e :> es, Show e) =>
e -> Eff es a
throwError (UnifyError SourceRegion -> Eff r ())
-> UnifyError SourceRegion -> Eff r ()
forall a b. (a -> b) -> a -> b
$ Qualified VarName
-> Constraint SourceRegion -> UnifyError SourceRegion
forall loc. Qualified VarName -> Constraint loc -> UnifyError loc
UnresolvedConstraint Qualified VarName
valueName Constraint SourceRegion
finalConstraint

    let newType = Substitution SourceRegion
-> Monotype SourceRegion -> Monotype SourceRegion
forall (a :: * -> *) loc.
(Substitutable a loc, Eq (a loc)) =>
Substitution loc -> a loc -> a loc
substituteAll Substitution SourceRegion
subst Monotype SourceRegion
t

    logDebug $ "Substituted type: " <> pretty newType <> " from " <> pretty t <> " with " <> pretty subst

    generalized <- generalise (removeSkolems newType)

    logDebug $ "Generalized type: " <> pretty generalized <> " from " <> pretty newType

    pure (getExpr (substituteAll subst (SubstitutableExpr typedExpr)), generalized)

-- | Get the location of an expression
exprLocation :: New.Expr loc p -> loc
exprLocation :: forall {k} loc (p :: k). Expr loc p -> loc
exprLocation (New.Expr loc
loc ExpressionMeta p loc
_ Expr' loc p
_) = loc
loc

-- Replace all quantified variables in a type scheme with rigid skolem variables.
-- This prevents ill-typed programs from unifying annotated polymorphic variables
-- with concrete types during checking.
skolemise :: forall r. Type SourceRegion -> Eff r (Monotype SourceRegion)
skolemise :: forall (r :: [(* -> *) -> * -> *]).
Type SourceRegion -> Eff r (Monotype SourceRegion)
skolemise = \case
    Lifted Monotype SourceRegion
t -> Monotype SourceRegion -> Eff r (Monotype SourceRegion)
forall a. a -> Eff r a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Monotype SourceRegion
t
    Polytype (Forall SourceRegion
loc [UniqueTyVar]
tyVars Constraint SourceRegion
_ Monotype SourceRegion
t) -> do
        -- Build a substitution mapping each quantified variable α to a rigid skolem #α
        let pairs :: [(UniqueTyVar, Monotype SourceRegion)]
pairs = [UniqueTyVar]
-> [Monotype SourceRegion]
-> [(UniqueTyVar, Monotype SourceRegion)]
forall a b. [a] -> [b] -> [(a, b)]
zip ((UniqueTyVar -> UniqueTyVar) -> [UniqueTyVar] -> [UniqueTyVar]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Optic' A_Lens NoIx UniqueTyVar UniqueTyVar
-> UniqueTyVar -> UniqueTyVar
forall k (is :: IxList) s a.
Is k A_Getter =>
Optic' k is s a -> s -> a
view Optic' A_Lens NoIx UniqueTyVar UniqueTyVar
forall a s. HasType a s => Lens s s a a
typed) [UniqueTyVar]
tyVars) (SourceRegion -> TypeVariable -> Monotype SourceRegion
forall loc. loc -> TypeVariable -> Monotype loc
TypeVar SourceRegion
loc (TypeVariable -> Monotype SourceRegion)
-> (UniqueTyVar -> TypeVariable)
-> UniqueTyVar
-> Monotype SourceRegion
forall b c a. (b -> c) -> (a -> b) -> a -> c
. UniqueTyVar -> TypeVariable
SkolemVar (UniqueTyVar -> Monotype SourceRegion)
-> [UniqueTyVar] -> [Monotype SourceRegion]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [UniqueTyVar]
tyVars)
            subst :: Substitution SourceRegion
subst = Map UniqueTyVar (Monotype SourceRegion)
-> Substitution SourceRegion
forall loc. Map UniqueTyVar (Monotype loc) -> Substitution loc
Substitution (Map UniqueTyVar (Monotype SourceRegion)
 -> Substitution SourceRegion)
-> Map UniqueTyVar (Monotype SourceRegion)
-> Substitution SourceRegion
forall a b. (a -> b) -> a -> b
$ forall l. IsList l => [Item l] -> l
fromList @(Map _ _) [(UniqueTyVar, Monotype SourceRegion)]
[Item (Map UniqueTyVar (Monotype SourceRegion))]
pairs
        Monotype SourceRegion -> Eff r (Monotype SourceRegion)
forall a. a -> Eff r a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Monotype SourceRegion -> Eff r (Monotype SourceRegion))
-> Monotype SourceRegion -> Eff r (Monotype SourceRegion)
forall a b. (a -> b) -> a -> b
$ Substitution SourceRegion
-> Monotype SourceRegion -> Monotype SourceRegion
forall (a :: * -> *) loc.
(Substitutable a loc, Eq (a loc)) =>
Substitution loc -> a loc -> a loc
substituteAll Substitution SourceRegion
subst Monotype SourceRegion
t

newtype SubstitutableExpr loc = SubstitutableExpr {forall {k} (loc :: k). SubstitutableExpr loc -> TypedExpr
getExpr :: TypedExpr} deriving (Int -> SubstitutableExpr loc -> ShowS
[SubstitutableExpr loc] -> ShowS
SubstitutableExpr loc -> String
(Int -> SubstitutableExpr loc -> ShowS)
-> (SubstitutableExpr loc -> String)
-> ([SubstitutableExpr loc] -> ShowS)
-> Show (SubstitutableExpr loc)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall k (loc :: k). Int -> SubstitutableExpr loc -> ShowS
forall k (loc :: k). [SubstitutableExpr loc] -> ShowS
forall k (loc :: k). SubstitutableExpr loc -> String
$cshowsPrec :: forall k (loc :: k). Int -> SubstitutableExpr loc -> ShowS
showsPrec :: Int -> SubstitutableExpr loc -> ShowS
$cshow :: forall k (loc :: k). SubstitutableExpr loc -> String
show :: SubstitutableExpr loc -> String
$cshowList :: forall k (loc :: k). [SubstitutableExpr loc] -> ShowS
showList :: [SubstitutableExpr loc] -> ShowS
Show, SubstitutableExpr loc -> SubstitutableExpr loc -> Bool
(SubstitutableExpr loc -> SubstitutableExpr loc -> Bool)
-> (SubstitutableExpr loc -> SubstitutableExpr loc -> Bool)
-> Eq (SubstitutableExpr loc)
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
forall k (loc :: k).
SubstitutableExpr loc -> SubstitutableExpr loc -> Bool
$c== :: forall k (loc :: k).
SubstitutableExpr loc -> SubstitutableExpr loc -> Bool
== :: SubstitutableExpr loc -> SubstitutableExpr loc -> Bool
$c/= :: forall k (loc :: k).
SubstitutableExpr loc -> SubstitutableExpr loc -> Bool
/= :: SubstitutableExpr loc -> SubstitutableExpr loc -> Bool
Eq, Eq (SubstitutableExpr loc)
Eq (SubstitutableExpr loc) =>
(SubstitutableExpr loc -> SubstitutableExpr loc -> Ordering)
-> (SubstitutableExpr loc -> SubstitutableExpr loc -> Bool)
-> (SubstitutableExpr loc -> SubstitutableExpr loc -> Bool)
-> (SubstitutableExpr loc -> SubstitutableExpr loc -> Bool)
-> (SubstitutableExpr loc -> SubstitutableExpr loc -> Bool)
-> (SubstitutableExpr loc
    -> SubstitutableExpr loc -> SubstitutableExpr loc)
-> (SubstitutableExpr loc
    -> SubstitutableExpr loc -> SubstitutableExpr loc)
-> Ord (SubstitutableExpr loc)
SubstitutableExpr loc -> SubstitutableExpr loc -> Bool
SubstitutableExpr loc -> SubstitutableExpr loc -> Ordering
SubstitutableExpr loc
-> SubstitutableExpr loc -> SubstitutableExpr loc
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
forall k (loc :: k). Eq (SubstitutableExpr loc)
forall k (loc :: k).
SubstitutableExpr loc -> SubstitutableExpr loc -> Bool
forall k (loc :: k).
SubstitutableExpr loc -> SubstitutableExpr loc -> Ordering
forall k (loc :: k).
SubstitutableExpr loc
-> SubstitutableExpr loc -> SubstitutableExpr loc
$ccompare :: forall k (loc :: k).
SubstitutableExpr loc -> SubstitutableExpr loc -> Ordering
compare :: SubstitutableExpr loc -> SubstitutableExpr loc -> Ordering
$c< :: forall k (loc :: k).
SubstitutableExpr loc -> SubstitutableExpr loc -> Bool
< :: SubstitutableExpr loc -> SubstitutableExpr loc -> Bool
$c<= :: forall k (loc :: k).
SubstitutableExpr loc -> SubstitutableExpr loc -> Bool
<= :: SubstitutableExpr loc -> SubstitutableExpr loc -> Bool
$c> :: forall k (loc :: k).
SubstitutableExpr loc -> SubstitutableExpr loc -> Bool
> :: SubstitutableExpr loc -> SubstitutableExpr loc -> Bool
$c>= :: forall k (loc :: k).
SubstitutableExpr loc -> SubstitutableExpr loc -> Bool
>= :: SubstitutableExpr loc -> SubstitutableExpr loc -> Bool
$cmax :: forall k (loc :: k).
SubstitutableExpr loc
-> SubstitutableExpr loc -> SubstitutableExpr loc
max :: SubstitutableExpr loc
-> SubstitutableExpr loc -> SubstitutableExpr loc
$cmin :: forall k (loc :: k).
SubstitutableExpr loc
-> SubstitutableExpr loc -> SubstitutableExpr loc
min :: SubstitutableExpr loc
-> SubstitutableExpr loc -> SubstitutableExpr loc
Ord)

instance Substitutable SubstitutableExpr SourceRegion where
    substitute :: UniqueTyVar
-> Monotype SourceRegion
-> SubstitutableExpr SourceRegion
-> SubstitutableExpr SourceRegion
substitute UniqueTyVar
tv Monotype SourceRegion
t (SubstitutableExpr TypedExpr
expr) =
        let New.Expr SourceRegion
loc ExpressionMeta Typed SourceRegion
meta Expr' SourceRegion Typed
e' = TypedExpr
expr
            meta' :: Monotype SourceRegion
meta' = UniqueTyVar
-> Monotype SourceRegion
-> Monotype SourceRegion
-> Monotype SourceRegion
forall (a :: * -> *) loc.
Substitutable a loc =>
UniqueTyVar -> Monotype loc -> a loc -> a loc
substitute UniqueTyVar
tv Monotype SourceRegion
t ExpressionMeta Typed SourceRegion
Monotype SourceRegion
meta
            e'' :: Expr' SourceRegion Typed
e'' = UniqueTyVar
-> Monotype SourceRegion
-> Expr' SourceRegion Typed
-> Expr' SourceRegion Typed
substituteExpr' UniqueTyVar
tv Monotype SourceRegion
t Expr' SourceRegion Typed
e'
         in TypedExpr -> SubstitutableExpr SourceRegion
forall {k} (loc :: k). TypedExpr -> SubstitutableExpr loc
SubstitutableExpr (SourceRegion
-> ExpressionMeta Typed SourceRegion
-> Expr' SourceRegion Typed
-> TypedExpr
forall {k} loc (p :: k).
loc -> ExpressionMeta p loc -> Expr' loc p -> Expr loc p
New.Expr SourceRegion
loc ExpressionMeta Typed SourceRegion
Monotype SourceRegion
meta' Expr' SourceRegion Typed
e'')

    -- overridden default for performance (provides a > 300% speedup by avoiding repeated traversals over potentially large expressions)
    substituteAll :: Eq (SubstitutableExpr SourceRegion) =>
Substitution SourceRegion
-> SubstitutableExpr SourceRegion -> SubstitutableExpr SourceRegion
substituteAll Substitution SourceRegion
s (SubstitutableExpr TypedExpr
expr) =
        let New.Expr SourceRegion
loc ExpressionMeta Typed SourceRegion
meta Expr' SourceRegion Typed
e' = TypedExpr
expr
            meta' :: Monotype SourceRegion
meta' = Substitution SourceRegion
-> Monotype SourceRegion -> Monotype SourceRegion
forall (a :: * -> *) loc.
(Substitutable a loc, Eq (a loc)) =>
Substitution loc -> a loc -> a loc
substituteAll Substitution SourceRegion
s ExpressionMeta Typed SourceRegion
Monotype SourceRegion
meta
            e'' :: Expr' SourceRegion Typed
e'' = Substitution SourceRegion
-> Expr' SourceRegion Typed -> Expr' SourceRegion Typed
substituteAllExpr' Substitution SourceRegion
s Expr' SourceRegion Typed
e'
         in TypedExpr -> SubstitutableExpr SourceRegion
forall {k} (loc :: k). TypedExpr -> SubstitutableExpr loc
SubstitutableExpr (SourceRegion
-> ExpressionMeta Typed SourceRegion
-> Expr' SourceRegion Typed
-> TypedExpr
forall {k} loc (p :: k).
loc -> ExpressionMeta p loc -> Expr' loc p -> Expr loc p
New.Expr SourceRegion
loc ExpressionMeta Typed SourceRegion
Monotype SourceRegion
meta' Expr' SourceRegion Typed
e'')

-- | Substitute a type variable in an expression body
substituteExpr' :: UniqueTyVar -> Monotype SourceRegion -> TypedExpr' -> TypedExpr'
substituteExpr' :: UniqueTyVar
-> Monotype SourceRegion
-> Expr' SourceRegion Typed
-> Expr' SourceRegion Typed
substituteExpr' UniqueTyVar
tv Monotype SourceRegion
t = \case
    New.EInt Integer
i -> Integer -> Expr' SourceRegion Typed
forall {k} loc (p :: k). Integer -> Expr' loc p
New.EInt Integer
i
    New.EFloat Double
f -> Double -> Expr' SourceRegion Typed
forall {k} loc (p :: k). Double -> Expr' loc p
New.EFloat Double
f
    New.EString Text
s -> Text -> Expr' SourceRegion Typed
forall {k} loc (p :: k). Text -> Expr' loc p
New.EString Text
s
    New.EChar Char
c -> Char -> Expr' SourceRegion Typed
forall {k} loc (p :: k). Char -> Expr' loc p
New.EChar Char
c
    Expr' SourceRegion Typed
New.EUnit -> Expr' SourceRegion Typed
forall {k} loc (p :: k). Expr' loc p
New.EUnit
    New.EVar VariableExtension Typed
vt ValueOccurrence Typed SourceRegion
v -> VariableExtension Typed
-> ValueOccurrence Typed SourceRegion -> Expr' SourceRegion Typed
forall {k} loc (p :: k).
VariableExtension p -> ValueOccurrence p loc -> Expr' loc p
New.EVar (UniqueTyVar
-> Monotype SourceRegion -> Type SourceRegion -> Type SourceRegion
forall (a :: * -> *) loc.
Substitutable a loc =>
UniqueTyVar -> Monotype loc -> a loc -> a loc
substitute UniqueTyVar
tv Monotype SourceRegion
t VariableExtension Typed
Type SourceRegion
vt) ValueOccurrence Typed SourceRegion
v
    New.ECon ConstructorNodeExtension Typed
ext ConstructorOccurrence Typed SourceRegion
v -> ConstructorNodeExtension Typed
-> ConstructorOccurrence Typed SourceRegion
-> Expr' SourceRegion Typed
forall {k} loc (p :: k).
ConstructorNodeExtension p
-> ConstructorOccurrence p loc -> Expr' loc p
New.ECon ConstructorNodeExtension Typed
ext ConstructorOccurrence Typed SourceRegion
v
    New.ELam LambdaExtension Typed
ext LambdaBinder Typed SourceRegion
binder TypedExpr
body -> LambdaExtension Typed
-> LambdaBinder Typed SourceRegion
-> TypedExpr
-> Expr' SourceRegion Typed
forall {k} loc (p :: k).
LambdaExtension p
-> LambdaBinder p loc -> Expr loc p -> Expr' loc p
New.ELam LambdaExtension Typed
ext (UniqueTyVar
-> Monotype SourceRegion
-> TypedLambdaParam (Unique VarName) SourceRegion Typed
-> TypedLambdaParam (Unique VarName) SourceRegion Typed
substituteLambdaBinder UniqueTyVar
tv Monotype SourceRegion
t LambdaBinder Typed SourceRegion
TypedLambdaParam (Unique VarName) SourceRegion Typed
binder) (UniqueTyVar -> Monotype SourceRegion -> TypedExpr -> TypedExpr
substituteExpr UniqueTyVar
tv Monotype SourceRegion
t TypedExpr
body)
    New.EApp ApplicationExtension Typed
ext TypedExpr
f TypedExpr
x -> ApplicationExtension Typed
-> TypedExpr -> TypedExpr -> Expr' SourceRegion Typed
forall {k} loc (p :: k).
ApplicationExtension p -> Expr loc p -> Expr loc p -> Expr' loc p
New.EApp ApplicationExtension Typed
ext (UniqueTyVar -> Monotype SourceRegion -> TypedExpr -> TypedExpr
substituteExpr UniqueTyVar
tv Monotype SourceRegion
t TypedExpr
f) (UniqueTyVar -> Monotype SourceRegion -> TypedExpr -> TypedExpr
substituteExpr UniqueTyVar
tv Monotype SourceRegion
t TypedExpr
x)
    New.ETyApp TypedExpr
e Type SourceRegion Typed
ty -> TypedExpr -> Type SourceRegion Typed -> Expr' SourceRegion Typed
forall {k} loc (p :: k). Expr loc p -> Type loc p -> Expr' loc p
New.ETyApp (UniqueTyVar -> Monotype SourceRegion -> TypedExpr -> TypedExpr
substituteExpr UniqueTyVar
tv Monotype SourceRegion
t TypedExpr
e) (UniqueTyVar
-> Monotype SourceRegion
-> Type SourceRegion Typed
-> Type SourceRegion Typed
substituteAstType UniqueTyVar
tv Monotype SourceRegion
t Type SourceRegion Typed
ty)
    New.EIf TypedExpr
c TypedExpr
th TypedExpr
el -> TypedExpr -> TypedExpr -> TypedExpr -> Expr' SourceRegion Typed
forall {k} loc (p :: k).
Expr loc p -> Expr loc p -> Expr loc p -> Expr' loc p
New.EIf (UniqueTyVar -> Monotype SourceRegion -> TypedExpr -> TypedExpr
substituteExpr UniqueTyVar
tv Monotype SourceRegion
t TypedExpr
c) (UniqueTyVar -> Monotype SourceRegion -> TypedExpr -> TypedExpr
substituteExpr UniqueTyVar
tv Monotype SourceRegion
t TypedExpr
th) (UniqueTyVar -> Monotype SourceRegion -> TypedExpr -> TypedExpr
substituteExpr UniqueTyVar
tv Monotype SourceRegion
t TypedExpr
el)
    New.EMatch TypedExpr
e [(Pattern SourceRegion Typed, TypedExpr)]
cases -> TypedExpr
-> [(Pattern SourceRegion Typed, TypedExpr)]
-> Expr' SourceRegion Typed
forall {k} loc (p :: k).
Expr loc p -> [(Pattern loc p, Expr loc p)] -> Expr' loc p
New.EMatch (UniqueTyVar -> Monotype SourceRegion -> TypedExpr -> TypedExpr
substituteExpr UniqueTyVar
tv Monotype SourceRegion
t TypedExpr
e) ((Pattern SourceRegion Typed -> Pattern SourceRegion Typed)
-> (TypedExpr -> TypedExpr)
-> [(Pattern SourceRegion Typed, TypedExpr)]
-> [(Pattern SourceRegion Typed, TypedExpr)]
forall (f :: * -> *) (p :: * -> * -> *) a c b d.
(Functor f, Bifunctor p) =>
(a -> c) -> (b -> d) -> f (p a b) -> f (p c d)
bimapF (UniqueTyVar
-> Monotype SourceRegion
-> Pattern SourceRegion Typed
-> Pattern SourceRegion Typed
substitutePattern UniqueTyVar
tv Monotype SourceRegion
t) (UniqueTyVar -> Monotype SourceRegion -> TypedExpr -> TypedExpr
substituteExpr UniqueTyVar
tv Monotype SourceRegion
t) [(Pattern SourceRegion Typed, TypedExpr)]
cases)
    New.ELetIn LetExtension Typed
ext ValueBinder Typed SourceRegion
binder TypedExpr
e1 TypedExpr
e2 -> LetExtension Typed
-> ValueBinder Typed SourceRegion
-> TypedExpr
-> TypedExpr
-> Expr' SourceRegion Typed
forall {k} loc (p :: k).
LetExtension p
-> ValueBinder p loc -> Expr loc p -> Expr loc p -> Expr' loc p
New.ELetIn LetExtension Typed
ext ValueBinder Typed SourceRegion
binder (UniqueTyVar -> Monotype SourceRegion -> TypedExpr -> TypedExpr
substituteExpr UniqueTyVar
tv Monotype SourceRegion
t TypedExpr
e1) (UniqueTyVar -> Monotype SourceRegion -> TypedExpr -> TypedExpr
substituteExpr UniqueTyVar
tv Monotype SourceRegion
t TypedExpr
e2)
    New.ELet LetExtension Typed
ext ValueBinder Typed SourceRegion
binder TypedExpr
e1 -> LetExtension Typed
-> ValueBinder Typed SourceRegion
-> TypedExpr
-> Expr' SourceRegion Typed
forall {k} loc (p :: k).
LetExtension p -> ValueBinder p loc -> Expr loc p -> Expr' loc p
New.ELet LetExtension Typed
ext ValueBinder Typed SourceRegion
binder (UniqueTyVar -> Monotype SourceRegion -> TypedExpr -> TypedExpr
substituteExpr UniqueTyVar
tv Monotype SourceRegion
t TypedExpr
e1)
    New.EBlock NonEmpty TypedExpr
exprs -> NonEmpty TypedExpr -> Expr' SourceRegion Typed
forall {k} loc (p :: k). NonEmpty (Expr loc p) -> Expr' loc p
New.EBlock ((TypedExpr -> TypedExpr)
-> NonEmpty TypedExpr -> NonEmpty TypedExpr
forall a b. (a -> b) -> NonEmpty a -> NonEmpty b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (UniqueTyVar -> Monotype SourceRegion -> TypedExpr -> TypedExpr
substituteExpr UniqueTyVar
tv Monotype SourceRegion
t) NonEmpty TypedExpr
exprs)
    New.EAnn TypedExpr
e Type SourceRegion Typed
ty -> TypedExpr -> Type SourceRegion Typed -> Expr' SourceRegion Typed
forall {k} loc (p :: k). Expr loc p -> Type loc p -> Expr' loc p
New.EAnn (UniqueTyVar -> Monotype SourceRegion -> TypedExpr -> TypedExpr
substituteExpr UniqueTyVar
tv Monotype SourceRegion
t TypedExpr
e) (UniqueTyVar
-> Monotype SourceRegion
-> Type SourceRegion Typed
-> Type SourceRegion Typed
substituteAstType UniqueTyVar
tv Monotype SourceRegion
t Type SourceRegion Typed
ty)
    New.EExtension ExpressionExtension Typed SourceRegion
v -> Void -> Expr' SourceRegion Typed
forall a. Void -> a
absurd Void
ExpressionExtension Typed SourceRegion
v

-- | Bulk substitute in expression body (performance optimized)
substituteAllExpr' :: Substitution SourceRegion -> TypedExpr' -> TypedExpr'
substituteAllExpr' :: Substitution SourceRegion
-> Expr' SourceRegion Typed -> Expr' SourceRegion Typed
substituteAllExpr' Substitution SourceRegion
s = \case
    New.EInt Integer
i -> Integer -> Expr' SourceRegion Typed
forall {k} loc (p :: k). Integer -> Expr' loc p
New.EInt Integer
i
    New.EFloat Double
f -> Double -> Expr' SourceRegion Typed
forall {k} loc (p :: k). Double -> Expr' loc p
New.EFloat Double
f
    New.EString Text
s' -> Text -> Expr' SourceRegion Typed
forall {k} loc (p :: k). Text -> Expr' loc p
New.EString Text
s'
    New.EChar Char
c -> Char -> Expr' SourceRegion Typed
forall {k} loc (p :: k). Char -> Expr' loc p
New.EChar Char
c
    Expr' SourceRegion Typed
New.EUnit -> Expr' SourceRegion Typed
forall {k} loc (p :: k). Expr' loc p
New.EUnit
    New.EVar VariableExtension Typed
vt ValueOccurrence Typed SourceRegion
v -> VariableExtension Typed
-> ValueOccurrence Typed SourceRegion -> Expr' SourceRegion Typed
forall {k} loc (p :: k).
VariableExtension p -> ValueOccurrence p loc -> Expr' loc p
New.EVar (Substitution SourceRegion -> Type SourceRegion -> Type SourceRegion
forall (a :: * -> *) loc.
(Substitutable a loc, Eq (a loc)) =>
Substitution loc -> a loc -> a loc
substituteAll Substitution SourceRegion
s VariableExtension Typed
Type SourceRegion
vt) ValueOccurrence Typed SourceRegion
v
    New.ECon ConstructorNodeExtension Typed
ext ConstructorOccurrence Typed SourceRegion
v -> ConstructorNodeExtension Typed
-> ConstructorOccurrence Typed SourceRegion
-> Expr' SourceRegion Typed
forall {k} loc (p :: k).
ConstructorNodeExtension p
-> ConstructorOccurrence p loc -> Expr' loc p
New.ECon ConstructorNodeExtension Typed
ext ConstructorOccurrence Typed SourceRegion
v
    New.ELam LambdaExtension Typed
ext LambdaBinder Typed SourceRegion
binder TypedExpr
body -> LambdaExtension Typed
-> LambdaBinder Typed SourceRegion
-> TypedExpr
-> Expr' SourceRegion Typed
forall {k} loc (p :: k).
LambdaExtension p
-> LambdaBinder p loc -> Expr loc p -> Expr' loc p
New.ELam LambdaExtension Typed
ext (Substitution SourceRegion
-> TypedLambdaParam (Unique VarName) SourceRegion Typed
-> TypedLambdaParam (Unique VarName) SourceRegion Typed
substituteAllLambdaBinder Substitution SourceRegion
s LambdaBinder Typed SourceRegion
TypedLambdaParam (Unique VarName) SourceRegion Typed
binder) (Substitution SourceRegion -> TypedExpr -> TypedExpr
substituteAllExpr Substitution SourceRegion
s TypedExpr
body)
    New.EApp ApplicationExtension Typed
ext TypedExpr
f TypedExpr
x -> ApplicationExtension Typed
-> TypedExpr -> TypedExpr -> Expr' SourceRegion Typed
forall {k} loc (p :: k).
ApplicationExtension p -> Expr loc p -> Expr loc p -> Expr' loc p
New.EApp ApplicationExtension Typed
ext (Substitution SourceRegion -> TypedExpr -> TypedExpr
substituteAllExpr Substitution SourceRegion
s TypedExpr
f) (Substitution SourceRegion -> TypedExpr -> TypedExpr
substituteAllExpr Substitution SourceRegion
s TypedExpr
x)
    New.ETyApp TypedExpr
e Type SourceRegion Typed
ty -> TypedExpr -> Type SourceRegion Typed -> Expr' SourceRegion Typed
forall {k} loc (p :: k). Expr loc p -> Type loc p -> Expr' loc p
New.ETyApp (Substitution SourceRegion -> TypedExpr -> TypedExpr
substituteAllExpr Substitution SourceRegion
s TypedExpr
e) (Substitution SourceRegion
-> Type SourceRegion Typed -> Type SourceRegion Typed
substituteAllAstType Substitution SourceRegion
s Type SourceRegion Typed
ty)
    New.EIf TypedExpr
c TypedExpr
th TypedExpr
el -> TypedExpr -> TypedExpr -> TypedExpr -> Expr' SourceRegion Typed
forall {k} loc (p :: k).
Expr loc p -> Expr loc p -> Expr loc p -> Expr' loc p
New.EIf (Substitution SourceRegion -> TypedExpr -> TypedExpr
substituteAllExpr Substitution SourceRegion
s TypedExpr
c) (Substitution SourceRegion -> TypedExpr -> TypedExpr
substituteAllExpr Substitution SourceRegion
s TypedExpr
th) (Substitution SourceRegion -> TypedExpr -> TypedExpr
substituteAllExpr Substitution SourceRegion
s TypedExpr
el)
    New.EMatch TypedExpr
e [(Pattern SourceRegion Typed, TypedExpr)]
cases -> TypedExpr
-> [(Pattern SourceRegion Typed, TypedExpr)]
-> Expr' SourceRegion Typed
forall {k} loc (p :: k).
Expr loc p -> [(Pattern loc p, Expr loc p)] -> Expr' loc p
New.EMatch (Substitution SourceRegion -> TypedExpr -> TypedExpr
substituteAllExpr Substitution SourceRegion
s TypedExpr
e) ((Pattern SourceRegion Typed -> Pattern SourceRegion Typed)
-> (TypedExpr -> TypedExpr)
-> [(Pattern SourceRegion Typed, TypedExpr)]
-> [(Pattern SourceRegion Typed, TypedExpr)]
forall (f :: * -> *) (p :: * -> * -> *) a c b d.
(Functor f, Bifunctor p) =>
(a -> c) -> (b -> d) -> f (p a b) -> f (p c d)
bimapF (Substitution SourceRegion
-> Pattern SourceRegion Typed -> Pattern SourceRegion Typed
substituteAllPattern Substitution SourceRegion
s) (Substitution SourceRegion -> TypedExpr -> TypedExpr
substituteAllExpr Substitution SourceRegion
s) [(Pattern SourceRegion Typed, TypedExpr)]
cases)
    New.ELetIn LetExtension Typed
ext ValueBinder Typed SourceRegion
binder TypedExpr
e1 TypedExpr
e2 -> LetExtension Typed
-> ValueBinder Typed SourceRegion
-> TypedExpr
-> TypedExpr
-> Expr' SourceRegion Typed
forall {k} loc (p :: k).
LetExtension p
-> ValueBinder p loc -> Expr loc p -> Expr loc p -> Expr' loc p
New.ELetIn LetExtension Typed
ext ValueBinder Typed SourceRegion
binder (Substitution SourceRegion -> TypedExpr -> TypedExpr
substituteAllExpr Substitution SourceRegion
s TypedExpr
e1) (Substitution SourceRegion -> TypedExpr -> TypedExpr
substituteAllExpr Substitution SourceRegion
s TypedExpr
e2)
    New.ELet LetExtension Typed
ext ValueBinder Typed SourceRegion
binder TypedExpr
e1 -> LetExtension Typed
-> ValueBinder Typed SourceRegion
-> TypedExpr
-> Expr' SourceRegion Typed
forall {k} loc (p :: k).
LetExtension p -> ValueBinder p loc -> Expr loc p -> Expr' loc p
New.ELet LetExtension Typed
ext ValueBinder Typed SourceRegion
binder (Substitution SourceRegion -> TypedExpr -> TypedExpr
substituteAllExpr Substitution SourceRegion
s TypedExpr
e1)
    New.EBlock NonEmpty TypedExpr
exprs -> NonEmpty TypedExpr -> Expr' SourceRegion Typed
forall {k} loc (p :: k). NonEmpty (Expr loc p) -> Expr' loc p
New.EBlock ((TypedExpr -> TypedExpr)
-> NonEmpty TypedExpr -> NonEmpty TypedExpr
forall a b. (a -> b) -> NonEmpty a -> NonEmpty b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Substitution SourceRegion -> TypedExpr -> TypedExpr
substituteAllExpr Substitution SourceRegion
s) NonEmpty TypedExpr
exprs)
    New.EAnn TypedExpr
e Type SourceRegion Typed
ty -> TypedExpr -> Type SourceRegion Typed -> Expr' SourceRegion Typed
forall {k} loc (p :: k). Expr loc p -> Type loc p -> Expr' loc p
New.EAnn (Substitution SourceRegion -> TypedExpr -> TypedExpr
substituteAllExpr Substitution SourceRegion
s TypedExpr
e) (Substitution SourceRegion
-> Type SourceRegion Typed -> Type SourceRegion Typed
substituteAllAstType Substitution SourceRegion
s Type SourceRegion Typed
ty)
    New.EExtension ExpressionExtension Typed SourceRegion
v -> Void -> Expr' SourceRegion Typed
forall a. Void -> a
absurd Void
ExpressionExtension Typed SourceRegion
v

substituteExpr :: UniqueTyVar -> Monotype SourceRegion -> TypedExpr -> TypedExpr
substituteExpr :: UniqueTyVar -> Monotype SourceRegion -> TypedExpr -> TypedExpr
substituteExpr UniqueTyVar
tv Monotype SourceRegion
t (New.Expr SourceRegion
loc ExpressionMeta Typed SourceRegion
meta Expr' SourceRegion Typed
e') = SourceRegion
-> ExpressionMeta Typed SourceRegion
-> Expr' SourceRegion Typed
-> TypedExpr
forall {k} loc (p :: k).
loc -> ExpressionMeta p loc -> Expr' loc p -> Expr loc p
New.Expr SourceRegion
loc (UniqueTyVar
-> Monotype SourceRegion
-> Monotype SourceRegion
-> Monotype SourceRegion
forall (a :: * -> *) loc.
Substitutable a loc =>
UniqueTyVar -> Monotype loc -> a loc -> a loc
substitute UniqueTyVar
tv Monotype SourceRegion
t ExpressionMeta Typed SourceRegion
Monotype SourceRegion
meta) (UniqueTyVar
-> Monotype SourceRegion
-> Expr' SourceRegion Typed
-> Expr' SourceRegion Typed
substituteExpr' UniqueTyVar
tv Monotype SourceRegion
t Expr' SourceRegion Typed
e')

substituteAllExpr :: Substitution SourceRegion -> TypedExpr -> TypedExpr
substituteAllExpr :: Substitution SourceRegion -> TypedExpr -> TypedExpr
substituteAllExpr Substitution SourceRegion
s (New.Expr SourceRegion
loc ExpressionMeta Typed SourceRegion
meta Expr' SourceRegion Typed
e') = SourceRegion
-> ExpressionMeta Typed SourceRegion
-> Expr' SourceRegion Typed
-> TypedExpr
forall {k} loc (p :: k).
loc -> ExpressionMeta p loc -> Expr' loc p -> Expr loc p
New.Expr SourceRegion
loc (Substitution SourceRegion
-> Monotype SourceRegion -> Monotype SourceRegion
forall (a :: * -> *) loc.
(Substitutable a loc, Eq (a loc)) =>
Substitution loc -> a loc -> a loc
substituteAll Substitution SourceRegion
s ExpressionMeta Typed SourceRegion
Monotype SourceRegion
meta) (Substitution SourceRegion
-> Expr' SourceRegion Typed -> Expr' SourceRegion Typed
substituteAllExpr' Substitution SourceRegion
s Expr' SourceRegion Typed
e')

substitutePattern :: UniqueTyVar -> Monotype SourceRegion -> NewT.TypedPattern -> NewT.TypedPattern
substitutePattern :: UniqueTyVar
-> Monotype SourceRegion
-> Pattern SourceRegion Typed
-> Pattern SourceRegion Typed
substitutePattern UniqueTyVar
tv Monotype SourceRegion
t (New.Pattern SourceRegion
loc PatternMeta Typed SourceRegion
meta Pattern' SourceRegion Typed
p') = SourceRegion
-> PatternMeta Typed SourceRegion
-> Pattern' SourceRegion Typed
-> Pattern SourceRegion Typed
forall {k} loc (p :: k).
loc -> PatternMeta p loc -> Pattern' loc p -> Pattern loc p
New.Pattern SourceRegion
loc (UniqueTyVar
-> Monotype SourceRegion
-> Monotype SourceRegion
-> Monotype SourceRegion
forall (a :: * -> *) loc.
Substitutable a loc =>
UniqueTyVar -> Monotype loc -> a loc -> a loc
substitute UniqueTyVar
tv Monotype SourceRegion
t PatternMeta Typed SourceRegion
Monotype SourceRegion
meta) (UniqueTyVar
-> Monotype SourceRegion
-> Pattern' SourceRegion Typed
-> Pattern' SourceRegion Typed
substitutePattern' UniqueTyVar
tv Monotype SourceRegion
t Pattern' SourceRegion Typed
p')

substituteAllPattern :: Substitution SourceRegion -> NewT.TypedPattern -> NewT.TypedPattern
substituteAllPattern :: Substitution SourceRegion
-> Pattern SourceRegion Typed -> Pattern SourceRegion Typed
substituteAllPattern Substitution SourceRegion
s (New.Pattern SourceRegion
loc PatternMeta Typed SourceRegion
meta Pattern' SourceRegion Typed
p') = SourceRegion
-> PatternMeta Typed SourceRegion
-> Pattern' SourceRegion Typed
-> Pattern SourceRegion Typed
forall {k} loc (p :: k).
loc -> PatternMeta p loc -> Pattern' loc p -> Pattern loc p
New.Pattern SourceRegion
loc (Substitution SourceRegion
-> Monotype SourceRegion -> Monotype SourceRegion
forall (a :: * -> *) loc.
(Substitutable a loc, Eq (a loc)) =>
Substitution loc -> a loc -> a loc
substituteAll Substitution SourceRegion
s PatternMeta Typed SourceRegion
Monotype SourceRegion
meta) (Substitution SourceRegion
-> Pattern' SourceRegion Typed -> Pattern' SourceRegion Typed
substituteAllPattern' Substitution SourceRegion
s Pattern' SourceRegion Typed
p')

substitutePattern' :: UniqueTyVar -> Monotype SourceRegion -> NewT.TypedPattern' -> NewT.TypedPattern'
substitutePattern' :: UniqueTyVar
-> Monotype SourceRegion
-> Pattern' SourceRegion Typed
-> Pattern' SourceRegion Typed
substitutePattern' UniqueTyVar
tv Monotype SourceRegion
t = \case
    New.PVar ValueBinder Typed SourceRegion
v -> ValueBinder Typed SourceRegion -> Pattern' SourceRegion Typed
forall {k} loc (p :: k). ValueBinder p loc -> Pattern' loc p
New.PVar ValueBinder Typed SourceRegion
v
    New.PCon ConstructorOccurrence Typed SourceRegion
c [Pattern SourceRegion Typed]
ps -> ConstructorOccurrence Typed SourceRegion
-> [Pattern SourceRegion Typed] -> Pattern' SourceRegion Typed
forall {k} loc (p :: k).
ConstructorOccurrence p loc -> [Pattern loc p] -> Pattern' loc p
New.PCon ConstructorOccurrence Typed SourceRegion
c ((Pattern SourceRegion Typed -> Pattern SourceRegion Typed)
-> [Pattern SourceRegion Typed] -> [Pattern SourceRegion Typed]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (UniqueTyVar
-> Monotype SourceRegion
-> Pattern SourceRegion Typed
-> Pattern SourceRegion Typed
substitutePattern UniqueTyVar
tv Monotype SourceRegion
t) [Pattern SourceRegion Typed]
ps)
    Pattern' SourceRegion Typed
New.PWildcard -> Pattern' SourceRegion Typed
forall {k} loc (p :: k). Pattern' loc p
New.PWildcard
    New.PInt Integer
i -> Integer -> Pattern' SourceRegion Typed
forall {k} loc (p :: k). Integer -> Pattern' loc p
New.PInt Integer
i
    New.PFloat Double
f -> Double -> Pattern' SourceRegion Typed
forall {k} loc (p :: k). Double -> Pattern' loc p
New.PFloat Double
f
    New.PString Text
s -> Text -> Pattern' SourceRegion Typed
forall {k} loc (p :: k). Text -> Pattern' loc p
New.PString Text
s
    New.PChar Char
c -> Char -> Pattern' SourceRegion Typed
forall {k} loc (p :: k). Char -> Pattern' loc p
New.PChar Char
c
    Pattern' SourceRegion Typed
New.PUnit -> Pattern' SourceRegion Typed
forall {k} loc (p :: k). Pattern' loc p
New.PUnit
    New.PExtension PatternExtension Typed SourceRegion
v -> Void -> Pattern' SourceRegion Typed
forall a. Void -> a
absurd Void
PatternExtension Typed SourceRegion
v

substituteAllPattern' :: Substitution SourceRegion -> NewT.TypedPattern' -> NewT.TypedPattern'
substituteAllPattern' :: Substitution SourceRegion
-> Pattern' SourceRegion Typed -> Pattern' SourceRegion Typed
substituteAllPattern' Substitution SourceRegion
s = \case
    New.PVar ValueBinder Typed SourceRegion
v -> ValueBinder Typed SourceRegion -> Pattern' SourceRegion Typed
forall {k} loc (p :: k). ValueBinder p loc -> Pattern' loc p
New.PVar ValueBinder Typed SourceRegion
v
    New.PCon ConstructorOccurrence Typed SourceRegion
c [Pattern SourceRegion Typed]
ps -> ConstructorOccurrence Typed SourceRegion
-> [Pattern SourceRegion Typed] -> Pattern' SourceRegion Typed
forall {k} loc (p :: k).
ConstructorOccurrence p loc -> [Pattern loc p] -> Pattern' loc p
New.PCon ConstructorOccurrence Typed SourceRegion
c ((Pattern SourceRegion Typed -> Pattern SourceRegion Typed)
-> [Pattern SourceRegion Typed] -> [Pattern SourceRegion Typed]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Substitution SourceRegion
-> Pattern SourceRegion Typed -> Pattern SourceRegion Typed
substituteAllPattern Substitution SourceRegion
s) [Pattern SourceRegion Typed]
ps)
    Pattern' SourceRegion Typed
New.PWildcard -> Pattern' SourceRegion Typed
forall {k} loc (p :: k). Pattern' loc p
New.PWildcard
    New.PInt Integer
i -> Integer -> Pattern' SourceRegion Typed
forall {k} loc (p :: k). Integer -> Pattern' loc p
New.PInt Integer
i
    New.PFloat Double
f -> Double -> Pattern' SourceRegion Typed
forall {k} loc (p :: k). Double -> Pattern' loc p
New.PFloat Double
f
    New.PString Text
s -> Text -> Pattern' SourceRegion Typed
forall {k} loc (p :: k). Text -> Pattern' loc p
New.PString Text
s
    New.PChar Char
c -> Char -> Pattern' SourceRegion Typed
forall {k} loc (p :: k). Char -> Pattern' loc p
New.PChar Char
c
    Pattern' SourceRegion Typed
New.PUnit -> Pattern' SourceRegion Typed
forall {k} loc (p :: k). Pattern' loc p
New.PUnit
    New.PExtension PatternExtension Typed SourceRegion
v -> Void -> Pattern' SourceRegion Typed
forall a. Void -> a
absurd Void
PatternExtension Typed SourceRegion
v

substituteLambdaBinder :: UniqueTyVar -> Monotype SourceRegion -> TypedLambdaParam (Unique VarName) SourceRegion Typed -> TypedLambdaParam (Unique VarName) SourceRegion Typed
substituteLambdaBinder :: UniqueTyVar
-> Monotype SourceRegion
-> TypedLambdaParam (Unique VarName) SourceRegion Typed
-> TypedLambdaParam (Unique VarName) SourceRegion Typed
substituteLambdaBinder UniqueTyVar
tv Monotype SourceRegion
t (TypedLambdaParam Unique VarName
v PatternMeta Typed SourceRegion
meta) = Unique VarName
-> PatternMeta Typed SourceRegion
-> TypedLambdaParam (Unique VarName) SourceRegion Typed
forall {k} v loc (p :: k).
v -> PatternMeta p loc -> TypedLambdaParam v loc p
TypedLambdaParam Unique VarName
v (UniqueTyVar
-> Monotype SourceRegion
-> Monotype SourceRegion
-> Monotype SourceRegion
forall (a :: * -> *) loc.
Substitutable a loc =>
UniqueTyVar -> Monotype loc -> a loc -> a loc
substitute UniqueTyVar
tv Monotype SourceRegion
t PatternMeta Typed SourceRegion
Monotype SourceRegion
meta)

substituteAllLambdaBinder :: Substitution SourceRegion -> TypedLambdaParam (Unique VarName) SourceRegion Typed -> TypedLambdaParam (Unique VarName) SourceRegion Typed
substituteAllLambdaBinder :: Substitution SourceRegion
-> TypedLambdaParam (Unique VarName) SourceRegion Typed
-> TypedLambdaParam (Unique VarName) SourceRegion Typed
substituteAllLambdaBinder Substitution SourceRegion
s (TypedLambdaParam Unique VarName
v PatternMeta Typed SourceRegion
meta) = Unique VarName
-> PatternMeta Typed SourceRegion
-> TypedLambdaParam (Unique VarName) SourceRegion Typed
forall {k} v loc (p :: k).
v -> PatternMeta p loc -> TypedLambdaParam v loc p
TypedLambdaParam Unique VarName
v (Substitution SourceRegion
-> Monotype SourceRegion -> Monotype SourceRegion
forall (a :: * -> *) loc.
(Substitutable a loc, Eq (a loc)) =>
Substitution loc -> a loc -> a loc
substituteAll Substitution SourceRegion
s PatternMeta Typed SourceRegion
Monotype SourceRegion
meta)

-- | Substitute a type variable in an AST type (New.Type SourceRegion Typed)
substituteAstType :: UniqueTyVar -> Monotype SourceRegion -> NewT.TypedType -> NewT.TypedType
substituteAstType :: UniqueTyVar
-> Monotype SourceRegion
-> Type SourceRegion Typed
-> Type SourceRegion Typed
substituteAstType UniqueTyVar
tv Monotype SourceRegion
t (New.Type SourceRegion
loc TypeMeta Typed SourceRegion
kind Type' SourceRegion Typed
t') = case Type' SourceRegion Typed
t' of
    New.TVar (Located SourceRegion
_ UniqueTyVar
tv')
        | UniqueTyVar
tv UniqueTyVar -> UniqueTyVar -> Bool
forall a. Eq a => a -> a -> Bool
== UniqueTyVar
tv' -> SourceRegion
-> ElaraKind -> Monotype SourceRegion -> Type SourceRegion Typed
monotypeToAstType SourceRegion
loc TypeMeta Typed SourceRegion
ElaraKind
kind Monotype SourceRegion
t
    Type' SourceRegion Typed
_ -> SourceRegion
-> TypeMeta Typed SourceRegion
-> Type' SourceRegion Typed
-> Type SourceRegion Typed
forall {k} loc (p :: k).
loc -> TypeMeta p loc -> Type' loc p -> Type loc p
New.Type SourceRegion
loc TypeMeta Typed SourceRegion
kind (UniqueTyVar
-> Monotype SourceRegion
-> Type' SourceRegion Typed
-> Type' SourceRegion Typed
substituteAstType' UniqueTyVar
tv Monotype SourceRegion
t Type' SourceRegion Typed
t')

substituteAstType' :: UniqueTyVar -> Monotype SourceRegion -> NewT.TypedType' -> NewT.TypedType'
substituteAstType' :: UniqueTyVar
-> Monotype SourceRegion
-> Type' SourceRegion Typed
-> Type' SourceRegion Typed
substituteAstType' UniqueTyVar
tv Monotype SourceRegion
t = \case
    New.TVar TypeVariable Typed SourceRegion
v -> TypeVariable Typed SourceRegion -> Type' SourceRegion Typed
forall {k} loc (p :: k). TypeVariable p loc -> Type' loc p
New.TVar TypeVariable Typed SourceRegion
v -- not matching (matching case handled in substituteAstType)
    New.TFun Type SourceRegion Typed
a Type SourceRegion Typed
b -> Type SourceRegion Typed
-> Type SourceRegion Typed -> Type' SourceRegion Typed
forall {k} loc (p :: k). Type loc p -> Type loc p -> Type' loc p
New.TFun (UniqueTyVar
-> Monotype SourceRegion
-> Type SourceRegion Typed
-> Type SourceRegion Typed
substituteAstType UniqueTyVar
tv Monotype SourceRegion
t Type SourceRegion Typed
a) (UniqueTyVar
-> Monotype SourceRegion
-> Type SourceRegion Typed
-> Type SourceRegion Typed
substituteAstType UniqueTyVar
tv Monotype SourceRegion
t Type SourceRegion Typed
b)
    Type' SourceRegion Typed
New.TUnit -> Type' SourceRegion Typed
forall {k} loc (p :: k). Type' loc p
New.TUnit
    New.TApp Type SourceRegion Typed
a Type SourceRegion Typed
b -> Type SourceRegion Typed
-> Type SourceRegion Typed -> Type' SourceRegion Typed
forall {k} loc (p :: k). Type loc p -> Type loc p -> Type' loc p
New.TApp (UniqueTyVar
-> Monotype SourceRegion
-> Type SourceRegion Typed
-> Type SourceRegion Typed
substituteAstType UniqueTyVar
tv Monotype SourceRegion
t Type SourceRegion Typed
a) (UniqueTyVar
-> Monotype SourceRegion
-> Type SourceRegion Typed
-> Type SourceRegion Typed
substituteAstType UniqueTyVar
tv Monotype SourceRegion
t Type SourceRegion Typed
b)
    New.TUserDefined TypeOccurrence Typed SourceRegion
n -> TypeOccurrence Typed SourceRegion -> Type' SourceRegion Typed
forall {k} loc (p :: k). TypeOccurrence p loc -> Type' loc p
New.TUserDefined TypeOccurrence Typed SourceRegion
n
    New.TRecord NonEmpty
  (Locate SourceRegion LowerAlphaName, Type SourceRegion Typed)
fields -> NonEmpty
  (Locate SourceRegion LowerAlphaName, Type SourceRegion Typed)
-> Type' SourceRegion Typed
forall {k} loc (p :: k).
NonEmpty (Locate loc LowerAlphaName, Type loc p) -> Type' loc p
New.TRecord (UniqueTyVar
-> Monotype SourceRegion
-> Type SourceRegion Typed
-> Type SourceRegion Typed
substituteAstType UniqueTyVar
tv Monotype SourceRegion
t (Type SourceRegion Typed -> Type SourceRegion Typed)
-> NonEmpty (Located LowerAlphaName, Type SourceRegion Typed)
-> NonEmpty (Located LowerAlphaName, Type SourceRegion Typed)
forall (f :: * -> *) (g :: * -> *) a b.
(Functor f, Functor g) =>
(a -> b) -> f (g a) -> f (g b)
<<$>> NonEmpty (Located LowerAlphaName, Type SourceRegion Typed)
NonEmpty
  (Locate SourceRegion LowerAlphaName, Type SourceRegion Typed)
fields)
    New.TList Type SourceRegion Typed
a -> Type SourceRegion Typed -> Type' SourceRegion Typed
forall {k} loc (p :: k). Type loc p -> Type' loc p
New.TList (UniqueTyVar
-> Monotype SourceRegion
-> Type SourceRegion Typed
-> Type SourceRegion Typed
substituteAstType UniqueTyVar
tv Monotype SourceRegion
t Type SourceRegion Typed
a)
    New.TExtension TypeSyntaxExtension Typed SourceRegion
v -> Void -> Type' SourceRegion Typed
forall a. Void -> a
absurd Void
TypeSyntaxExtension Typed SourceRegion
v

-- | Bulk substitute in an AST type
substituteAllAstType :: Substitution SourceRegion -> NewT.TypedType -> NewT.TypedType
substituteAllAstType :: Substitution SourceRegion
-> Type SourceRegion Typed -> Type SourceRegion Typed
substituteAllAstType (Substitution Map UniqueTyVar (Monotype SourceRegion)
s) Type SourceRegion Typed
ty = (Type SourceRegion Typed
 -> (UniqueTyVar, Monotype SourceRegion) -> Type SourceRegion Typed)
-> Type SourceRegion Typed
-> [(UniqueTyVar, Monotype SourceRegion)]
-> Type SourceRegion Typed
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' (\Type SourceRegion Typed
acc (UniqueTyVar
tv, Monotype SourceRegion
t) -> UniqueTyVar
-> Monotype SourceRegion
-> Type SourceRegion Typed
-> Type SourceRegion Typed
substituteAstType UniqueTyVar
tv Monotype SourceRegion
t Type SourceRegion Typed
acc) Type SourceRegion Typed
ty (Map UniqueTyVar (Monotype SourceRegion)
-> [(UniqueTyVar, Monotype SourceRegion)]
forall k a. Map k a -> [(k, a)]
Map.toList Map UniqueTyVar (Monotype SourceRegion)
s)

-- | Convert a Monotype to an AST Type for the Typed phase
monotypeToAstType :: SourceRegion -> ElaraKind -> Monotype SourceRegion -> NewT.TypedType
monotypeToAstType :: SourceRegion
-> ElaraKind -> Monotype SourceRegion -> Type SourceRegion Typed
monotypeToAstType SourceRegion
loc ElaraKind
kind = \case
    TypeVar SourceRegion
_ TypeVariable
tv -> SourceRegion
-> TypeMeta Typed SourceRegion
-> Type' SourceRegion Typed
-> Type SourceRegion Typed
forall {k} loc (p :: k).
loc -> TypeMeta p loc -> Type' loc p -> Type loc p
New.Type SourceRegion
loc TypeMeta Typed SourceRegion
ElaraKind
kind (TypeVariable Typed SourceRegion -> Type' SourceRegion Typed
forall {k} loc (p :: k). TypeVariable p loc -> Type' loc p
New.TVar (SourceRegion -> UniqueTyVar -> Located UniqueTyVar
forall a. SourceRegion -> a -> Located a
Located SourceRegion
loc (TypeVariable -> UniqueTyVar
typeVarToUniqueTyVar TypeVariable
tv)))
    Function SourceRegion
_ Monotype SourceRegion
a Monotype SourceRegion
b -> SourceRegion
-> TypeMeta Typed SourceRegion
-> Type' SourceRegion Typed
-> Type SourceRegion Typed
forall {k} loc (p :: k).
loc -> TypeMeta p loc -> Type' loc p -> Type loc p
New.Type SourceRegion
loc TypeMeta Typed SourceRegion
ElaraKind
kind (Type SourceRegion Typed
-> Type SourceRegion Typed -> Type' SourceRegion Typed
forall {k} loc (p :: k). Type loc p -> Type loc p -> Type' loc p
New.TFun (SourceRegion
-> ElaraKind -> Monotype SourceRegion -> Type SourceRegion Typed
monotypeToAstType SourceRegion
loc ElaraKind
kind Monotype SourceRegion
a) (SourceRegion
-> ElaraKind -> Monotype SourceRegion -> Type SourceRegion Typed
monotypeToAstType SourceRegion
loc ElaraKind
kind Monotype SourceRegion
b))
    TypeConstructor SourceRegion
_ Qualified TypeName
qn [Monotype SourceRegion]
args -> case [Monotype SourceRegion]
args of
        [] -> SourceRegion
-> TypeMeta Typed SourceRegion
-> Type' SourceRegion Typed
-> Type SourceRegion Typed
forall {k} loc (p :: k).
loc -> TypeMeta p loc -> Type' loc p -> Type loc p
New.Type SourceRegion
loc TypeMeta Typed SourceRegion
ElaraKind
kind (TypeOccurrence Typed SourceRegion -> Type' SourceRegion Typed
forall {k} loc (p :: k). TypeOccurrence p loc -> Type' loc p
New.TUserDefined (SourceRegion -> Qualified TypeName -> Located (Qualified TypeName)
forall a. SourceRegion -> a -> Located a
Located SourceRegion
loc Qualified TypeName
qn))
        [Monotype SourceRegion]
_ -> (Type SourceRegion Typed
 -> Monotype SourceRegion -> Type SourceRegion Typed)
-> Type SourceRegion Typed
-> [Monotype SourceRegion]
-> Type SourceRegion Typed
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' (\Type SourceRegion Typed
acc Monotype SourceRegion
arg -> SourceRegion
-> TypeMeta Typed SourceRegion
-> Type' SourceRegion Typed
-> Type SourceRegion Typed
forall {k} loc (p :: k).
loc -> TypeMeta p loc -> Type' loc p -> Type loc p
New.Type SourceRegion
loc TypeMeta Typed SourceRegion
ElaraKind
kind (Type SourceRegion Typed
-> Type SourceRegion Typed -> Type' SourceRegion Typed
forall {k} loc (p :: k). Type loc p -> Type loc p -> Type' loc p
New.TApp Type SourceRegion Typed
acc (SourceRegion
-> ElaraKind -> Monotype SourceRegion -> Type SourceRegion Typed
monotypeToAstType SourceRegion
loc ElaraKind
kind Monotype SourceRegion
arg))) (SourceRegion
-> TypeMeta Typed SourceRegion
-> Type' SourceRegion Typed
-> Type SourceRegion Typed
forall {k} loc (p :: k).
loc -> TypeMeta p loc -> Type' loc p -> Type loc p
New.Type SourceRegion
loc TypeMeta Typed SourceRegion
ElaraKind
kind (TypeOccurrence Typed SourceRegion -> Type' SourceRegion Typed
forall {k} loc (p :: k). TypeOccurrence p loc -> Type' loc p
New.TUserDefined (SourceRegion -> Qualified TypeName -> Located (Qualified TypeName)
forall a. SourceRegion -> a -> Located a
Located SourceRegion
loc Qualified TypeName
qn))) [Monotype SourceRegion]
args

typeVarToUniqueTyVar :: TypeVariable -> UniqueTyVar
typeVarToUniqueTyVar :: TypeVariable -> UniqueTyVar
typeVarToUniqueTyVar (UnificationVar UniqueTyVar
tv) = UniqueTyVar
tv
typeVarToUniqueTyVar (SkolemVar UniqueTyVar
tv) = UniqueTyVar
tv