{-# LANGUAGE TemplateHaskell #-}

-- | This module is the primary interface to the Unison typechecker
-- module Unison.Typechecker (admissibleTypeAt, check, check', checkAdmissible', equals, locals, subtype, isSubtype, synthesize, synthesize', typeAt, wellTyped) where
module Unison.Typechecker
  ( synthesize,
    synthesizeAndResolve,
    check,
    wellTyped,
    isEqual,
    isSubtype,
    fitsScheme,
    Env (..),
    Notes (..),
    Resolution (..),
    Name,
    NamedReference (..),
    Context.PatternMatchCoverageCheckAndKindInferenceSwitch (..),
  )
where

import Control.Lens
import Control.Monad.Fail (fail)
import Control.Monad.State (State, StateT, execState, get, modify)
import Control.Monad.Writer
import Data.Foldable
import Data.Map qualified as Map
import Data.Sequence qualified as Seq
import Data.Sequence.NonEmpty qualified as NESeq (toSeq)
import Data.Set qualified as Set
import Data.Text qualified as Text
import Data.Tuple qualified as Tuple
import Unison.ABT qualified as ABT
import Unison.Blank qualified as B
import Unison.Codebase.BuiltinAnnotation (BuiltinAnnotation)
import Unison.Name qualified as Name
import Unison.Prelude
import Unison.PrettyPrintEnv (PrettyPrintEnv)
import Unison.Result (Result, ResultT, runResultT, pattern Result)
import Unison.Result qualified as Result
import Unison.Syntax.Name qualified as Name (unsafeParseText, unsafeParseVar)
import Unison.Term (Term)
import Unison.Term qualified as Term
import Unison.Type (Type)
import Unison.Typechecker.Context qualified as Context
import Unison.Typechecker.TypeLookup qualified as TL
import Unison.Typechecker.TypeVar qualified as TypeVar
import Unison.Util.List (uniqueBy)
import Unison.Var (Var)
import Unison.Var qualified as Var

type Name = Text

data Notes v loc = Notes
  { forall v loc. Notes v loc -> Seq (CompilerBug v loc)
bugs :: Seq (Context.CompilerBug v loc),
    forall v loc. Notes v loc -> Seq (ErrorNote v loc)
errors :: Seq (Context.ErrorNote v loc),
    forall v loc. Notes v loc -> Seq (InfoNote v loc)
infos :: Seq (Context.InfoNote v loc)
  }
  deriving (Int -> Notes v loc -> ShowS
[Notes v loc] -> ShowS
Notes v loc -> String
(Int -> Notes v loc -> ShowS)
-> (Notes v loc -> String)
-> ([Notes v loc] -> ShowS)
-> Show (Notes v loc)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall v loc.
(Var v, Show loc, Ord loc) =>
Int -> Notes v loc -> ShowS
forall v loc. (Var v, Show loc, Ord loc) => [Notes v loc] -> ShowS
forall v loc. (Var v, Show loc, Ord loc) => Notes v loc -> String
$cshowsPrec :: forall v loc.
(Var v, Show loc, Ord loc) =>
Int -> Notes v loc -> ShowS
showsPrec :: Int -> Notes v loc -> ShowS
$cshow :: forall v loc. (Var v, Show loc, Ord loc) => Notes v loc -> String
show :: Notes v loc -> String
$cshowList :: forall v loc. (Var v, Show loc, Ord loc) => [Notes v loc] -> ShowS
showList :: [Notes v loc] -> ShowS
Show)

instance Semigroup (Notes v loc) where
  Notes Seq (CompilerBug v loc)
bs Seq (ErrorNote v loc)
es Seq (InfoNote v loc)
is <> :: Notes v loc -> Notes v loc -> Notes v loc
<> Notes Seq (CompilerBug v loc)
bs' Seq (ErrorNote v loc)
es' Seq (InfoNote v loc)
is' = Seq (CompilerBug v loc)
-> Seq (ErrorNote v loc) -> Seq (InfoNote v loc) -> Notes v loc
forall v loc.
Seq (CompilerBug v loc)
-> Seq (ErrorNote v loc) -> Seq (InfoNote v loc) -> Notes v loc
Notes (Seq (CompilerBug v loc)
bs Seq (CompilerBug v loc)
-> Seq (CompilerBug v loc) -> Seq (CompilerBug v loc)
forall a. Semigroup a => a -> a -> a
<> Seq (CompilerBug v loc)
bs') (Seq (ErrorNote v loc)
es Seq (ErrorNote v loc)
-> Seq (ErrorNote v loc) -> Seq (ErrorNote v loc)
forall a. Semigroup a => a -> a -> a
<> Seq (ErrorNote v loc)
es') (Seq (InfoNote v loc)
is Seq (InfoNote v loc)
-> Seq (InfoNote v loc) -> Seq (InfoNote v loc)
forall a. Semigroup a => a -> a -> a
<> Seq (InfoNote v loc)
is')

instance Monoid (Notes v loc) where
  mempty :: Notes v loc
mempty = Seq (CompilerBug v loc)
-> Seq (ErrorNote v loc) -> Seq (InfoNote v loc) -> Notes v loc
forall v loc.
Seq (CompilerBug v loc)
-> Seq (ErrorNote v loc) -> Seq (InfoNote v loc) -> Notes v loc
Notes Seq (CompilerBug v loc)
forall a. Monoid a => a
mempty Seq (ErrorNote v loc)
forall a. Monoid a => a
mempty Seq (InfoNote v loc)
forall a. Monoid a => a
mempty

convertResult :: Context.Result v loc a -> Result (Notes v loc) a
convertResult :: forall v loc a. Result v loc a -> Result (Notes v loc) a
convertResult = \case
  Context.Success Seq (InfoNote v loc)
is a
a -> Notes v loc -> Maybe a -> Result (Notes v loc) a
forall w a. w -> Maybe a -> MaybeT (WriterT w Identity) a
Result (Seq (CompilerBug v loc)
-> Seq (ErrorNote v loc) -> Seq (InfoNote v loc) -> Notes v loc
forall v loc.
Seq (CompilerBug v loc)
-> Seq (ErrorNote v loc) -> Seq (InfoNote v loc) -> Notes v loc
Notes Seq (CompilerBug v loc)
forall a. Monoid a => a
mempty Seq (ErrorNote v loc)
forall a. Monoid a => a
mempty Seq (InfoNote v loc)
is) (a -> Maybe a
forall a. a -> Maybe a
Just a
a)
  Context.TypeError NESeq (ErrorNote v loc)
es Seq (InfoNote v loc)
is -> Notes v loc -> Maybe a -> Result (Notes v loc) a
forall w a. w -> Maybe a -> MaybeT (WriterT w Identity) a
Result (Seq (CompilerBug v loc)
-> Seq (ErrorNote v loc) -> Seq (InfoNote v loc) -> Notes v loc
forall v loc.
Seq (CompilerBug v loc)
-> Seq (ErrorNote v loc) -> Seq (InfoNote v loc) -> Notes v loc
Notes Seq (CompilerBug v loc)
forall a. Monoid a => a
mempty (NESeq (ErrorNote v loc) -> Seq (ErrorNote v loc)
forall a. NESeq a -> Seq a
NESeq.toSeq NESeq (ErrorNote v loc)
es) Seq (InfoNote v loc)
is) Maybe a
forall a. Maybe a
Nothing
  Context.CompilerBug CompilerBug v loc
bug Seq (ErrorNote v loc)
es Seq (InfoNote v loc)
is -> Notes v loc -> Maybe a -> Result (Notes v loc) a
forall w a. w -> Maybe a -> MaybeT (WriterT w Identity) a
Result (Seq (CompilerBug v loc)
-> Seq (ErrorNote v loc) -> Seq (InfoNote v loc) -> Notes v loc
forall v loc.
Seq (CompilerBug v loc)
-> Seq (ErrorNote v loc) -> Seq (InfoNote v loc) -> Notes v loc
Notes (CompilerBug v loc -> Seq (CompilerBug v loc)
forall a. a -> Seq a
Seq.singleton CompilerBug v loc
bug) Seq (ErrorNote v loc)
es Seq (InfoNote v loc)
is) Maybe a
forall a. Maybe a
Nothing

data NamedReference v loc = NamedReference
  { forall v loc. NamedReference v loc -> Name
fqn :: Name.Name,
    forall v loc. NamedReference v loc -> Type v loc
fqnType :: Type v loc,
    forall v loc. NamedReference v loc -> Replacement v
replacement :: Context.Replacement v
  }
  deriving stock (Int -> NamedReference v loc -> ShowS
[NamedReference v loc] -> ShowS
NamedReference v loc -> String
(Int -> NamedReference v loc -> ShowS)
-> (NamedReference v loc -> String)
-> ([NamedReference v loc] -> ShowS)
-> Show (NamedReference v loc)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall v loc. Show v => Int -> NamedReference v loc -> ShowS
forall v loc. Show v => [NamedReference v loc] -> ShowS
forall v loc. Show v => NamedReference v loc -> String
$cshowsPrec :: forall v loc. Show v => Int -> NamedReference v loc -> ShowS
showsPrec :: Int -> NamedReference v loc -> ShowS
$cshow :: forall v loc. Show v => NamedReference v loc -> String
show :: NamedReference v loc -> String
$cshowList :: forall v loc. Show v => [NamedReference v loc] -> ShowS
showList :: [NamedReference v loc] -> ShowS
Show)

data Env v loc = Env
  { forall v loc. Env v loc -> [Type v loc]
ambientAbilities :: [Type v loc],
    forall v loc. Env v loc -> TypeLookup v loc
typeLookup :: TL.TypeLookup v loc,
    -- TDNR environment - maps short names like `+` to fully-qualified
    -- lists of named references whose full name matches the short name
    -- Example: `+` maps to [Nat.+, Float.+, Int.+]
    --
    -- This mapping is populated before typechecking with as few entries
    -- as are needed to help resolve variables needing TDNR in the file.
    --
    -- - Left means a term in the file (for which we don't have a type before typechecking)
    -- - Right means a term/constructor in the namespace, or a constructor in the file (for which we do have a type
    --   before typechecking)
    forall v loc.
Env v loc -> Map Name [Either Name (NamedReference v loc)]
termsByShortname :: Map Name.Name [Either Name.Name (NamedReference v loc)],
    forall v loc. Env v loc -> Map Name (NamedReference v loc)
topLevelComponents :: Map Name.Name (NamedReference v loc)
  }
  deriving stock ((forall x. Env v loc -> Rep (Env v loc) x)
-> (forall x. Rep (Env v loc) x -> Env v loc)
-> Generic (Env v loc)
forall x. Rep (Env v loc) x -> Env v loc
forall x. Env v loc -> Rep (Env v loc) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall v loc x. Rep (Env v loc) x -> Env v loc
forall v loc x. Env v loc -> Rep (Env v loc) x
$cfrom :: forall v loc x. Env v loc -> Rep (Env v loc) x
from :: forall x. Env v loc -> Rep (Env v loc) x
$cto :: forall v loc x. Rep (Env v loc) x -> Env v loc
to :: forall x. Rep (Env v loc) x -> Env v loc
Generic)

-- | Infer the type of a 'Unison.Term', using
-- a function to resolve the type of @Ref@ constructors
-- contained in that term.
synthesize ::
  (Monad f, Var v, BuiltinAnnotation loc, Ord loc, Show loc) =>
  PrettyPrintEnv ->
  Context.PatternMatchCoverageCheckAndKindInferenceSwitch ->
  Env v loc ->
  Term v loc ->
  ResultT (Notes v loc) f (Type v loc)
synthesize :: forall (f :: * -> *) v loc.
(Monad f, Var v, BuiltinAnnotation loc, Ord loc, Show loc) =>
PrettyPrintEnv
-> PatternMatchCoverageCheckAndKindInferenceSwitch
-> Env v loc
-> Term v loc
-> ResultT (Notes v loc) f (Type v loc)
synthesize PrettyPrintEnv
ppe PatternMatchCoverageCheckAndKindInferenceSwitch
pmccSwitch Env v loc
env Term v loc
t =
  let result :: Result (Notes v loc) (Type v loc)
result =
        Result v loc (Type v loc) -> Result (Notes v loc) (Type v loc)
forall v loc a. Result v loc a -> Result (Notes v loc) a
convertResult (Result v loc (Type v loc) -> Result (Notes v loc) (Type v loc))
-> Result v loc (Type v loc) -> Result (Notes v loc) (Type v loc)
forall a b. (a -> b) -> a -> b
$
          PrettyPrintEnv
-> PatternMatchCoverageCheckAndKindInferenceSwitch
-> [Type v loc]
-> TypeLookup v loc
-> Term v loc
-> Result v loc (Type v loc)
forall loc v.
(BuiltinAnnotation loc, Var v, Ord loc, Show loc) =>
PrettyPrintEnv
-> PatternMatchCoverageCheckAndKindInferenceSwitch
-> [Type v loc]
-> TypeLookup v loc
-> Term v loc
-> Result v loc (Type v loc)
Context.synthesizeClosed
            PrettyPrintEnv
ppe
            PatternMatchCoverageCheckAndKindInferenceSwitch
pmccSwitch
            (Type v loc -> Type v loc
forall v a b. Ord v => Type v a -> Type (TypeVar b v) a
TypeVar.liftType (Type v loc -> Type v loc) -> [Type v loc] -> [Type v loc]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Env v loc
env.ambientAbilities)
            Env v loc
env.typeLookup
            (Term v loc -> Term v loc
forall v a b. Ord v => Term v a -> Term' (TypeVar b v) v a
TypeVar.liftTerm Term v loc
t)
   in (forall a. Identity a -> f a)
-> ResultT (Notes v loc) Identity (Type v loc)
-> ResultT (Notes v loc) f (Type v loc)
forall (f :: * -> *) notes (g :: * -> *) b.
(Monad f, Monoid notes) =>
(forall a. f a -> g a) -> ResultT notes f b -> ResultT notes g b
Result.hoist (a -> f a
forall a. a -> f a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (a -> f a) -> (Identity a -> a) -> Identity a -> f a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Identity a -> a
forall a. Identity a -> a
runIdentity) (ResultT (Notes v loc) Identity (Type v loc)
 -> ResultT (Notes v loc) f (Type v loc))
-> ResultT (Notes v loc) Identity (Type v loc)
-> ResultT (Notes v loc) f (Type v loc)
forall a b. (a -> b) -> a -> b
$ (Type v loc -> Type v loc)
-> Result (Notes v loc) (Type v loc)
-> ResultT (Notes v loc) Identity (Type v loc)
forall a b.
(a -> b)
-> MaybeT (WriterT (Notes v loc) Identity) a
-> MaybeT (WriterT (Notes v loc) Identity) b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Type v loc -> Type v loc
forall v b a. Ord v => Type (TypeVar b v) a -> Type v a
TypeVar.lowerType Result (Notes v loc) (Type v loc)
result

isSubtype :: (Var v) => Type v loc -> Type v loc -> Bool
isSubtype :: forall v loc. Var v => Type v loc -> Type v loc -> Bool
isSubtype Type v loc
t1 Type v loc
t2 =
  Either (CompilerBug v ()) Bool -> Bool
forall v a. Var v => Either (CompilerBug v ()) a -> a
handleCompilerBug (Type v () -> Type v () -> Either (CompilerBug v ()) Bool
forall v loc.
(Var v, Ord loc) =>
Type v loc -> Type v loc -> Either (CompilerBug v loc) Bool
Context.isSubtype (Type v () -> Type v ()
forall {a} {b}. Type v a -> Type (TypeVar b v) a
tvar (Type v () -> Type v ()) -> Type v () -> Type v ()
forall a b. (a -> b) -> a -> b
$ Type v loc -> Type v ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void Type v loc
t1) (Type v () -> Type v ()
forall {a} {b}. Type v a -> Type (TypeVar b v) a
tvar (Type v () -> Type v ()) -> Type v () -> Type v ()
forall a b. (a -> b) -> a -> b
$ Type v loc -> Type v ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void Type v loc
t2))
  where
    tvar :: Type v a -> Type (TypeVar b v) a
tvar = Type v a -> Type (TypeVar b v) a
forall v a b. Ord v => Type v a -> Type (TypeVar b v) a
TypeVar.liftType

handleCompilerBug :: (Var v) => Either (Context.CompilerBug v ()) a -> a
handleCompilerBug :: forall v a. Var v => Either (CompilerBug v ()) a -> a
handleCompilerBug = \case
  Left CompilerBug v ()
bug -> String -> a
forall a. HasCallStack => String -> a
error (String -> a) -> String -> a
forall a b. (a -> b) -> a -> b
$ String
"compiler bug encountered: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ CompilerBug v () -> String
forall a. Show a => a -> String
show CompilerBug v ()
bug
  Right a
b -> a
b

-- | Similar to 'isSubtype' but treats @t2@ as a scheme where the
-- outermost variables are existential rather than universal.
--
-- For example:
-- @
-- let
--   lhs = Unison.Type.ref () (Unison.Builtin.Decls.unitRef)
--   rhs = Unison.Type.forall () (Unison.Var.named "x") (Unison.Type.var () (Unison.Var.named "x"))
-- in fitsScheme @Symbol lhs rhs
-- @
-- is @True@ although the lhs is not a subtype of the rhs.
--
-- 'fitsScheme' is used to check that runnable types are a subtype of
-- @
-- exists x. '{IO, Exception} x
-- @
fitsScheme :: (Var v) => Type v loc -> Type v loc -> Bool
fitsScheme :: forall v loc. Var v => Type v loc -> Type v loc -> Bool
fitsScheme Type v loc
t1 Type v loc
t2 = Either (CompilerBug v ()) Bool -> Bool
forall v a. Var v => Either (CompilerBug v ()) a -> a
handleCompilerBug (Type v () -> Type v () -> Either (CompilerBug v ()) Bool
forall v loc.
(Var v, Ord loc) =>
Type v loc -> Type v loc -> Either (CompilerBug v loc) Bool
Context.fitsScheme (Type v () -> Type v ()
forall {a} {b}. Type v a -> Type (TypeVar b v) a
tvar (Type v () -> Type v ()) -> Type v () -> Type v ()
forall a b. (a -> b) -> a -> b
$ Type v loc -> Type v ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void Type v loc
t1) (Type v () -> Type v ()
forall {a} {b}. Type v a -> Type (TypeVar b v) a
tvar (Type v () -> Type v ()) -> Type v () -> Type v ()
forall a b. (a -> b) -> a -> b
$ Type v loc -> Type v ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void Type v loc
t2))
  where
    tvar :: Type v a -> Type (TypeVar b v) a
tvar = Type v a -> Type (TypeVar b v) a
forall v a b. Ord v => Type v a -> Type (TypeVar b v) a
TypeVar.liftType

isEqual :: (Var v) => Type v loc -> Type v loc -> Bool
isEqual :: forall v loc. Var v => Type v loc -> Type v loc -> Bool
isEqual Type v loc
t1 Type v loc
t2 = Type v loc -> Type v loc -> Bool
forall v loc. Var v => Type v loc -> Type v loc -> Bool
isSubtype Type v loc
t1 Type v loc
t2 Bool -> Bool -> Bool
&& Type v loc -> Type v loc -> Bool
forall v loc. Var v => Type v loc -> Type v loc -> Bool
isSubtype Type v loc
t2 Type v loc
t1

type TDNR f v loc a =
  StateT (Term v loc) (ResultT (Notes v loc) f) a

data Resolution v loc = Resolution
  { forall v loc. Resolution v loc -> Text
resolvedName :: Text,
    forall v loc. Resolution v loc -> Type v loc
inferredType :: Context.Type v loc,
    forall v loc. Resolution v loc -> loc
resolvedLoc :: loc,
    forall v loc. Resolution v loc -> v
v :: v,
    forall v loc. Resolution v loc -> [Suggestion v loc]
suggestions :: [Context.Suggestion v loc]
  }

-- | Infer the type of a 'Unison.Term', using type-directed name resolution
-- to attempt to resolve unknown symbols.
synthesizeAndResolve ::
  (Monad f, Var v, Monoid loc, BuiltinAnnotation loc, Ord loc, Show loc) => PrettyPrintEnv -> Env v loc -> TDNR f v loc (Type v loc)
synthesizeAndResolve :: forall (f :: * -> *) v loc.
(Monad f, Var v, Monoid loc, BuiltinAnnotation loc, Ord loc,
 Show loc) =>
PrettyPrintEnv -> Env v loc -> TDNR f v loc (Type v loc)
synthesizeAndResolve PrettyPrintEnv
ppe Env v loc
env = do
  Term v loc
tm <- StateT (Term v loc) (ResultT (Notes v loc) f) (Term v loc)
forall s (m :: * -> *). MonadState s m => m s
get
  (Type v loc
tp, Notes v loc
notes) <-
    TDNR f v loc (Type v loc)
-> StateT
     (Term v loc) (ResultT (Notes v loc) f) (Type v loc, Notes v loc)
forall a.
StateT (Term v loc) (ResultT (Notes v loc) f) a
-> StateT (Term v loc) (ResultT (Notes v loc) f) (a, Notes v loc)
forall w (m :: * -> *) a. MonadWriter w m => m a -> m (a, w)
listen (TDNR f v loc (Type v loc)
 -> StateT
      (Term v loc) (ResultT (Notes v loc) f) (Type v loc, Notes v loc))
-> (ResultT (Notes v loc) f (Type v loc)
    -> TDNR f v loc (Type v loc))
-> ResultT (Notes v loc) f (Type v loc)
-> StateT
     (Term v loc) (ResultT (Notes v loc) f) (Type v loc, Notes v loc)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ResultT (Notes v loc) f (Type v loc) -> TDNR f v loc (Type v loc)
forall (m :: * -> *) a. Monad m => m a -> StateT (Term v loc) m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (ResultT (Notes v loc) f (Type v loc)
 -> StateT
      (Term v loc) (ResultT (Notes v loc) f) (Type v loc, Notes v loc))
-> ResultT (Notes v loc) f (Type v loc)
-> StateT
     (Term v loc) (ResultT (Notes v loc) f) (Type v loc, Notes v loc)
forall a b. (a -> b) -> a -> b
$
      PrettyPrintEnv
-> PatternMatchCoverageCheckAndKindInferenceSwitch
-> Env v loc
-> Term v loc
-> ResultT (Notes v loc) f (Type v loc)
forall (f :: * -> *) v loc.
(Monad f, Var v, BuiltinAnnotation loc, Ord loc, Show loc) =>
PrettyPrintEnv
-> PatternMatchCoverageCheckAndKindInferenceSwitch
-> Env v loc
-> Term v loc
-> ResultT (Notes v loc) f (Type v loc)
synthesize
        PrettyPrintEnv
ppe
        PatternMatchCoverageCheckAndKindInferenceSwitch
Context.PatternMatchCoverageCheckAndKindInferenceSwitch'Enabled
        Env v loc
env
        Term v loc
tm
  PrettyPrintEnv
-> Notes v loc
-> Type v loc
-> Env v loc
-> TDNR f v loc (Type v loc)
forall v loc (f :: * -> *).
(Monad f, Var v, BuiltinAnnotation loc, Ord loc, Monoid loc,
 Show loc) =>
PrettyPrintEnv
-> Notes v loc
-> Type v loc
-> Env v loc
-> TDNR f v loc (Type v loc)
typeDirectedNameResolution PrettyPrintEnv
ppe Notes v loc
notes Type v loc
tp Env v loc
env

compilerBug :: Context.CompilerBug v loc -> Result (Notes v loc) ()
compilerBug :: forall v loc. CompilerBug v loc -> Result (Notes v loc) ()
compilerBug CompilerBug v loc
bug = do
  Notes v loc -> Result (Notes v loc) ()
forall w (m :: * -> *). MonadWriter w m => w -> m ()
tell (Notes v loc -> Result (Notes v loc) ())
-> Notes v loc -> Result (Notes v loc) ()
forall a b. (a -> b) -> a -> b
$ Seq (CompilerBug v loc)
-> Seq (ErrorNote v loc) -> Seq (InfoNote v loc) -> Notes v loc
forall v loc.
Seq (CompilerBug v loc)
-> Seq (ErrorNote v loc) -> Seq (InfoNote v loc) -> Notes v loc
Notes (CompilerBug v loc -> Seq (CompilerBug v loc)
forall a. a -> Seq a
Seq.singleton CompilerBug v loc
bug) Seq (ErrorNote v loc)
forall a. Monoid a => a
mempty Seq (InfoNote v loc)
forall a. Monoid a => a
mempty
  String -> Result (Notes v loc) ()
forall a. String -> MaybeT (WriterT (Notes v loc) Identity) a
forall (m :: * -> *) a. MonadFail m => String -> m a
Control.Monad.Fail.fail String
""

typeError :: Context.ErrorNote v loc -> Result (Notes v loc) ()
typeError :: forall v loc. ErrorNote v loc -> Result (Notes v loc) ()
typeError ErrorNote v loc
note = do
  Notes v loc -> Result (Notes v loc) ()
forall w (m :: * -> *). MonadWriter w m => w -> m ()
tell (Notes v loc -> Result (Notes v loc) ())
-> Notes v loc -> Result (Notes v loc) ()
forall a b. (a -> b) -> a -> b
$ Seq (CompilerBug v loc)
-> Seq (ErrorNote v loc) -> Seq (InfoNote v loc) -> Notes v loc
forall v loc.
Seq (CompilerBug v loc)
-> Seq (ErrorNote v loc) -> Seq (InfoNote v loc) -> Notes v loc
Notes Seq (CompilerBug v loc)
forall a. Monoid a => a
mempty (ErrorNote v loc -> Seq (ErrorNote v loc)
forall a. a -> Seq a
Seq.singleton ErrorNote v loc
note) Seq (InfoNote v loc)
forall a. Monoid a => a
mempty
  String -> Result (Notes v loc) ()
forall a. String -> MaybeT (WriterT (Notes v loc) Identity) a
forall (m :: * -> *) a. MonadFail m => String -> m a
Control.Monad.Fail.fail String
""

btw :: (Monad f) => Context.InfoNote v loc -> ResultT (Notes v loc) f ()
btw :: forall (f :: * -> *) v loc.
Monad f =>
InfoNote v loc -> ResultT (Notes v loc) f ()
btw InfoNote v loc
note = Notes v loc -> MaybeT (WriterT (Notes v loc) f) ()
forall w (m :: * -> *). MonadWriter w m => w -> m ()
tell (Notes v loc -> MaybeT (WriterT (Notes v loc) f) ())
-> Notes v loc -> MaybeT (WriterT (Notes v loc) f) ()
forall a b. (a -> b) -> a -> b
$ Seq (CompilerBug v loc)
-> Seq (ErrorNote v loc) -> Seq (InfoNote v loc) -> Notes v loc
forall v loc.
Seq (CompilerBug v loc)
-> Seq (ErrorNote v loc) -> Seq (InfoNote v loc) -> Notes v loc
Notes Seq (CompilerBug v loc)
forall a. Monoid a => a
mempty Seq (ErrorNote v loc)
forall a. Monoid a => a
mempty (InfoNote v loc -> Seq (InfoNote v loc)
forall a. a -> Seq a
Seq.singleton InfoNote v loc
note)

liftResult :: (Monad f) => Result (Notes v loc) a -> TDNR f v loc a
liftResult :: forall (f :: * -> *) v loc a.
Monad f =>
Result (Notes v loc) a -> TDNR f v loc a
liftResult = ResultT (Notes v loc) f a
-> StateT (Term v loc) (ResultT (Notes v loc) f) a
forall (m :: * -> *) a. Monad m => m a -> StateT (Term v loc) m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (ResultT (Notes v loc) f a
 -> StateT (Term v loc) (ResultT (Notes v loc) f) a)
-> (Result (Notes v loc) a -> ResultT (Notes v loc) f a)
-> Result (Notes v loc) a
-> StateT (Term v loc) (ResultT (Notes v loc) f) a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. WriterT (Notes v loc) f (Maybe a) -> ResultT (Notes v loc) f a
forall (m :: * -> *) a. m (Maybe a) -> MaybeT m a
MaybeT (WriterT (Notes v loc) f (Maybe a) -> ResultT (Notes v loc) f a)
-> (Result (Notes v loc) a -> WriterT (Notes v loc) f (Maybe a))
-> Result (Notes v loc) a
-> ResultT (Notes v loc) f a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. f (Maybe a, Notes v loc) -> WriterT (Notes v loc) f (Maybe a)
forall w (m :: * -> *) a. m (a, w) -> WriterT w m a
WriterT (f (Maybe a, Notes v loc) -> WriterT (Notes v loc) f (Maybe a))
-> (Result (Notes v loc) a -> f (Maybe a, Notes v loc))
-> Result (Notes v loc) a
-> WriterT (Notes v loc) f (Maybe a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Maybe a, Notes v loc) -> f (Maybe a, Notes v loc)
forall a. a -> f a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ((Maybe a, Notes v loc) -> f (Maybe a, Notes v loc))
-> (Result (Notes v loc) a -> (Maybe a, Notes v loc))
-> Result (Notes v loc) a
-> f (Maybe a, Notes v loc)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Identity (Maybe a, Notes v loc) -> (Maybe a, Notes v loc)
forall a. Identity a -> a
runIdentity (Identity (Maybe a, Notes v loc) -> (Maybe a, Notes v loc))
-> (Result (Notes v loc) a -> Identity (Maybe a, Notes v loc))
-> Result (Notes v loc) a
-> (Maybe a, Notes v loc)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Result (Notes v loc) a -> Identity (Maybe a, Notes v loc)
forall notes (f :: * -> *) a.
ResultT notes f a -> f (Maybe a, notes)
runResultT

-- Resolve "solved blanks". If a solved blank's type and name matches the type
-- and unqualified name of a symbol that isn't imported, provide a note
-- suggesting the import. If the blank is ambiguous and only one typechecks, use
-- that one.  Otherwise, provide an unknown symbol error to the user.
-- The cases we consider are:
-- 1. There exist names that match and their types match too. Tell the user
--    the fully qualified names of these terms, and their types.
-- 2. There's more than one name that matches,
--    but only one that typechecks. Substitute that one into the code.
-- 3. No match at all. Throw an unresolved symbol at the user.
typeDirectedNameResolution ::
  forall v loc f.
  (Monad f, Var v, BuiltinAnnotation loc, Ord loc, Monoid loc, Show loc) =>
  PrettyPrintEnv ->
  Notes v loc ->
  Type v loc ->
  Env v loc ->
  TDNR f v loc (Type v loc)
typeDirectedNameResolution :: forall v loc (f :: * -> *).
(Monad f, Var v, BuiltinAnnotation loc, Ord loc, Monoid loc,
 Show loc) =>
PrettyPrintEnv
-> Notes v loc
-> Type v loc
-> Env v loc
-> TDNR f v loc (Type v loc)
typeDirectedNameResolution PrettyPrintEnv
ppe Notes v loc
oldNotes Type v loc
oldType Env v loc
env = do
  -- Add typed components (local definitions) to the TDNR environment.
  let tdnrEnv :: Env v loc
tdnrEnv = State (Env v loc) () -> Env v loc -> Env v loc
forall s a. State s a -> s -> s
execState ((InfoNote v loc -> State (Env v loc) ())
-> Seq (InfoNote v loc) -> State (Env v loc) ()
forall (t :: * -> *) (f :: * -> *) a b.
(Foldable t, Applicative f) =>
(a -> f b) -> t a -> f ()
traverse_ InfoNote v loc -> State (Env v loc) ()
addTypedComponent (Seq (InfoNote v loc) -> State (Env v loc) ())
-> Seq (InfoNote v loc) -> State (Env v loc) ()
forall a b. (a -> b) -> a -> b
$ Notes v loc -> Seq (InfoNote v loc)
forall v loc. Notes v loc -> Seq (InfoNote v loc)
infos Notes v loc
oldNotes) Env v loc
env
  -- Resolve blanks in the notes and generate some resolutions
  [Maybe (Resolution v loc)]
resolutions <-
    Result (Notes v loc) [Maybe (Resolution v loc)]
-> TDNR f v loc [Maybe (Resolution v loc)]
forall (f :: * -> *) v loc a.
Monad f =>
Result (Notes v loc) a -> TDNR f v loc a
liftResult (Result (Notes v loc) [Maybe (Resolution v loc)]
 -> TDNR f v loc [Maybe (Resolution v loc)])
-> (Seq (InfoNote v loc)
    -> Result (Notes v loc) [Maybe (Resolution v loc)])
-> Seq (InfoNote v loc)
-> TDNR f v loc [Maybe (Resolution v loc)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (InfoNote v loc
 -> MaybeT
      (WriterT (Notes v loc) Identity) (Maybe (Resolution v loc)))
-> [InfoNote v loc]
-> Result (Notes v loc) [Maybe (Resolution v loc)]
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 (Env v loc
-> InfoNote v loc
-> MaybeT
     (WriterT (Notes v loc) Identity) (Maybe (Resolution v loc))
resolveNote Env v loc
tdnrEnv) ([InfoNote v loc]
 -> Result (Notes v loc) [Maybe (Resolution v loc)])
-> (Seq (InfoNote v loc) -> [InfoNote v loc])
-> Seq (InfoNote v loc)
-> Result (Notes v loc) [Maybe (Resolution v loc)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Seq (InfoNote v loc) -> [InfoNote v loc]
forall a. Seq a -> [a]
forall (t :: * -> *) a. Foldable t => t a -> [a]
toList (Seq (InfoNote v loc) -> TDNR f v loc [Maybe (Resolution v loc)])
-> Seq (InfoNote v loc) -> TDNR f v loc [Maybe (Resolution v loc)]
forall a b. (a -> b) -> a -> b
$
      Notes v loc -> Seq (InfoNote v loc)
forall v loc. Notes v loc -> Seq (InfoNote v loc)
infos Notes v loc
oldNotes
  case [Maybe (Resolution v loc)] -> [Resolution v loc]
forall a. [Maybe a] -> [a]
catMaybes [Maybe (Resolution v loc)]
resolutions of
    [] -> Type v loc -> TDNR f v loc (Type v loc)
forall a. a -> StateT (Term v loc) (ResultT (Notes v loc) f) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Type v loc
oldType
    [Resolution v loc]
resolutions -> do
      [Bool]
substituted <- (Resolution v loc
 -> StateT (Term v loc) (ResultT (Notes v loc) f) Bool)
-> [Resolution v loc]
-> StateT (Term v loc) (ResultT (Notes v loc) f) [Bool]
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 Resolution v loc
-> StateT (Term v loc) (ResultT (Notes v loc) f) Bool
substSuggestion [Resolution v loc]
resolutions
      case [Bool] -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
or [Bool]
substituted of
        Bool
True -> PrettyPrintEnv -> Env v loc -> TDNR f v loc (Type v loc)
forall (f :: * -> *) v loc.
(Monad f, Var v, Monoid loc, BuiltinAnnotation loc, Ord loc,
 Show loc) =>
PrettyPrintEnv -> Env v loc -> TDNR f v loc (Type v loc)
synthesizeAndResolve PrettyPrintEnv
ppe Env v loc
tdnrEnv
        Bool
False -> do
          -- The type hasn't changed
          Result (Notes v loc) () -> TDNR f v loc ()
forall (f :: * -> *) v loc a.
Monad f =>
Result (Notes v loc) a -> TDNR f v loc a
liftResult (Result (Notes v loc) () -> TDNR f v loc ())
-> Result (Notes v loc) () -> TDNR f v loc ()
forall a b. (a -> b) -> a -> b
$ [Resolution v loc] -> Result (Notes v loc) ()
suggest [Resolution v loc]
resolutions
          pure Type v loc
oldType
  where
    addTypedComponent :: Context.InfoNote v loc -> State (Env v loc) ()
    addTypedComponent :: InfoNote v loc -> State (Env v loc) ()
addTypedComponent (Context.TopLevelComponent [(v, Type v loc, Bool)]
vtts) =
      [(v, Type v loc, Bool)]
-> ((v, Type v loc, Bool) -> State (Env v loc) ())
-> State (Env v loc) ()
forall (t :: * -> *) (f :: * -> *) a b.
(Foldable t, Applicative f) =>
t a -> (a -> f b) -> f ()
for_ [(v, Type v loc, Bool)]
vtts \(v
v, Type v loc
typ, Bool
_) ->
        let name :: Name
name = v -> Name
forall v. Var v => v -> Name
Name.unsafeParseVar (v -> v
forall v. Var v => v -> v
Var.reset v
v)
         in ASetter
  (Env v loc)
  (Env v loc)
  (Map Name (NamedReference v loc))
  (Map Name (NamedReference v loc))
#topLevelComponents ASetter
  (Env v loc)
  (Env v loc)
  (Map Name (NamedReference v loc))
  (Map Name (NamedReference v loc))
-> (Map Name (NamedReference v loc)
    -> Map Name (NamedReference v loc))
-> State (Env v loc) ()
forall s (m :: * -> *) a b.
MonadState s m =>
ASetter s s a b -> (a -> b) -> m ()
%= Name
-> NamedReference v loc
-> Map Name (NamedReference v loc)
-> Map Name (NamedReference v loc)
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert Name
name (Name -> Type v loc -> Replacement v -> NamedReference v loc
forall v loc.
Name -> Type v loc -> Replacement v -> NamedReference v loc
NamedReference Name
name Type v loc
typ (v -> Replacement v
forall v. v -> Replacement v
Context.ReplacementVar v
v))
    addTypedComponent InfoNote v loc
_ = () -> State (Env v loc) ()
forall a. a -> StateT (Env v loc) Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()

    suggest :: [Resolution v loc] -> Result (Notes v loc) ()
    suggest :: [Resolution v loc] -> Result (Notes v loc) ()
suggest =
      (Resolution v loc -> Result (Notes v loc) ())
-> [Resolution v loc] -> Result (Notes v loc) ()
forall (t :: * -> *) (f :: * -> *) a b.
(Foldable t, Applicative f) =>
(a -> f b) -> t a -> f ()
traverse_ \(Resolution Text
name Type v loc
inferredType loc
loc v
v [Suggestion v loc]
suggestions) ->
        ErrorNote v loc -> Result (Notes v loc) ()
forall v loc. ErrorNote v loc -> Result (Notes v loc) ()
typeError (ErrorNote v loc -> Result (Notes v loc) ())
-> ErrorNote v loc -> Result (Notes v loc) ()
forall a b. (a -> b) -> a -> b
$
          Context.ErrorNote
            { $sel:cause:ErrorNote :: Cause v loc
cause = loc -> v -> [Suggestion v loc] -> Type v loc -> Cause v loc
forall v loc.
loc -> v -> [Suggestion v loc] -> Type v loc -> Cause v loc
Context.UnknownTerm loc
loc (v -> Text -> v
Var v => v -> Text -> v
suggestedVar v
v Text
name) ([Suggestion v loc] -> [Suggestion v loc]
dedupe [Suggestion v loc]
suggestions) Type v loc
inferredType,
              $sel:path:ErrorNote :: Seq (PathElement v loc)
path = Seq (PathElement v loc)
forall a. Seq a
Seq.empty
            }

    guard :: Bool -> a -> Maybe a
guard Bool
x a
a = if Bool
x then a -> Maybe a
forall a. a -> Maybe a
Just a
a else Maybe a
forall a. Maybe a
Nothing

    suggestedVar :: (Var v) => v -> Text -> v
    suggestedVar :: Var v => v -> Text -> v
suggestedVar v
v Text
name =
      case v -> Type
forall v. Var v => v -> Type
Var.typeOf v
v of
        Type
Var.MissingResult -> v
v
        Type
_ -> Text -> v
forall v. Var v => Text -> v
Var.named Text
name

    extractSubstitution :: [Context.Suggestion v loc] -> Maybe (Context.Replacement v)
    extractSubstitution :: [Suggestion v loc] -> Maybe (Replacement v)
extractSubstitution [Suggestion v loc]
suggestions =
      let [([Name], Replacement v)]
groupedByName :: [([Name.Name], Context.Replacement v)] =
            ((Replacement v, [Name]) -> ([Name], Replacement v))
-> [(Replacement v, [Name])] -> [([Name], Replacement v)]
forall a b. (a -> b) -> [a] -> [b]
map (Replacement v, [Name]) -> ([Name], Replacement v)
forall a b. (a, b) -> (b, a)
Tuple.swap
              ([(Replacement v, [Name])] -> [([Name], Replacement v)])
-> ([Suggestion v loc] -> [(Replacement v, [Name])])
-> [Suggestion v loc]
-> [([Name], Replacement v)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Map (Replacement v) [Name] -> [(Replacement v, [Name])]
forall k a. Map k a -> [(k, a)]
Map.toList
              (Map (Replacement v) [Name] -> [(Replacement v, [Name])])
-> ([Suggestion v loc] -> Map (Replacement v) [Name])
-> [Suggestion v loc]
-> [(Replacement v, [Name])]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Set Name -> [Name])
-> Map (Replacement v) (Set Name) -> Map (Replacement v) [Name]
forall a b.
(a -> b) -> Map (Replacement v) a -> Map (Replacement v) b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Set Name -> [Name]
forall a. Set a -> [a]
Set.toList
              (Map (Replacement v) (Set Name) -> Map (Replacement v) [Name])
-> ([Suggestion v loc] -> Map (Replacement v) (Set Name))
-> [Suggestion v loc]
-> Map (Replacement v) [Name]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Map (Replacement v) (Set Name)
 -> Suggestion v loc -> Map (Replacement v) (Set Name))
-> Map (Replacement v) (Set Name)
-> [Suggestion v loc]
-> Map (Replacement v) (Set Name)
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl'
                ( \Map (Replacement v) (Set Name)
b Context.Suggestion {Name
suggestionName :: Name
$sel:suggestionName:Suggestion :: forall v loc. Suggestion v loc -> Name
suggestionName, Replacement v
suggestionReplacement :: Replacement v
$sel:suggestionReplacement:Suggestion :: forall v loc. Suggestion v loc -> Replacement v
suggestionReplacement} ->
                    (Set Name -> Set Name -> Set Name)
-> Replacement v
-> Set Name
-> Map (Replacement v) (Set Name)
-> Map (Replacement v) (Set Name)
forall k a. Ord k => (a -> a -> a) -> k -> a -> Map k a -> Map k a
Map.insertWith
                      Set Name -> Set Name -> Set Name
forall a. Ord a => Set a -> Set a -> Set a
Set.union
                      Replacement v
suggestionReplacement
                      (Name -> Set Name
forall a. a -> Set a
Set.singleton Name
suggestionName)
                      Map (Replacement v) (Set Name)
b
                )
                Map (Replacement v) (Set Name)
forall k a. Map k a
Map.empty
              ([Suggestion v loc] -> [([Name], Replacement v)])
-> [Suggestion v loc] -> [([Name], Replacement v)]
forall a b. (a -> b) -> a -> b
$ (Suggestion v loc -> Bool)
-> [Suggestion v loc] -> [Suggestion v loc]
forall a. (a -> Bool) -> [a] -> [a]
filter Suggestion v loc -> Bool
forall v loc. Suggestion v loc -> Bool
Context.isExact [Suggestion v loc]
suggestions
          Set (Replacement v)
matches :: Set (Context.Replacement v) = [([Name], Replacement v)] -> Set (Replacement v)
forall r. Ord r => [([Name], r)] -> Set r
Name.preferShallowLibDepth [([Name], Replacement v)]
groupedByName
       in case Set (Replacement v) -> [Replacement v]
forall a. Set a -> [a]
forall (t :: * -> *) a. Foldable t => t a -> [a]
toList Set (Replacement v)
matches of
            [Replacement v
x] -> Replacement v -> Maybe (Replacement v)
forall a. a -> Maybe a
Just Replacement v
x
            [Replacement v]
_ -> Maybe (Replacement v)
forall a. Maybe a
Nothing

    substSuggestion :: Resolution v loc -> TDNR f v loc Bool
    substSuggestion :: Resolution v loc
-> StateT (Term v loc) (ResultT (Notes v loc) f) Bool
substSuggestion (Resolution Text
name Type v loc
_ loc
loc v
v ([Suggestion v loc] -> Maybe (Replacement v)
extractSubstitution -> Just Replacement v
replacement)) = do
      (Term v loc -> Term v loc) -> TDNR f v loc ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify (Text -> loc -> Term v loc -> Term v loc -> Term v loc
substBlank Text
name loc
loc Term v loc
solved)
      ResultT (Notes v loc) f () -> TDNR f v loc ()
forall (m :: * -> *) a. Monad m => m a -> StateT (Term v loc) m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (ResultT (Notes v loc) f () -> TDNR f v loc ())
-> (InfoNote v loc -> ResultT (Notes v loc) f ())
-> InfoNote v loc
-> TDNR f v loc ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. InfoNote v loc -> ResultT (Notes v loc) f ()
forall (f :: * -> *) v loc.
Monad f =>
InfoNote v loc -> ResultT (Notes v loc) f ()
btw (InfoNote v loc -> TDNR f v loc ())
-> InfoNote v loc -> TDNR f v loc ()
forall a b. (a -> b) -> a -> b
$ v -> loc -> Term v loc -> InfoNote v loc
forall v loc. v -> loc -> Term v loc -> InfoNote v loc
Context.Decision (v -> Text -> v
Var v => v -> Text -> v
suggestedVar v
v Text
name) loc
loc Term v loc
solved
      pure Bool
True
      where
        solved :: Term v loc
solved =
          case Replacement v
replacement of
            Context.ReplacementRef Referent
ref -> loc -> Referent -> Term v loc
forall v a vt at ap. Ord v => a -> Referent -> Term2 vt at ap v a
Term.fromReferent loc
loc Referent
ref
            Context.ReplacementVar v
var -> loc -> v -> Term v loc
forall a v vt at ap. a -> v -> Term2 vt at ap v a
Term.var loc
loc v
var
    substSuggestion Resolution v loc
_ = Bool -> StateT (Term v loc) (ResultT (Notes v loc) f) Bool
forall a. a -> StateT (Term v loc) (ResultT (Notes v loc) f) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Bool
False

    -- Resolve a `Blank` to a term
    substBlank :: Text -> loc -> Term v loc -> Term v loc -> Term v loc
    substBlank :: Text -> loc -> Term v loc -> Term v loc -> Term v loc
substBlank Text
s loc
a Term v loc
r = (Term v loc -> Maybe (Term v loc)) -> Term v loc -> Term v loc
forall (f :: * -> *) v a.
(Traversable f, Ord v) =>
(Term f v a -> Maybe (Term f v a)) -> Term f v a -> Term f v a
ABT.visitPure Term v loc -> Maybe (Term v loc)
go
      where
        go :: Term v loc -> Maybe (Term v loc)
go Term v loc
t = Bool -> Term v loc -> Maybe (Term v loc)
forall {a}. Bool -> a -> Maybe a
guard (Term v loc -> loc
forall (f :: * -> *) v a. Term f v a -> a
ABT.annotation Term v loc
t loc -> loc -> Bool
forall a. Eq a => a -> a -> Bool
== loc
a) (Term v loc -> Maybe (Term v loc))
-> Term v loc -> Maybe (Term v loc)
forall a b. (a -> b) -> a -> b
$ (Term v loc -> Maybe (Term v loc)) -> Term v loc -> Term v loc
forall (f :: * -> *) v a.
(Traversable f, Ord v) =>
(Term f v a -> Maybe (Term f v a)) -> Term f v a -> Term f v a
ABT.visitPure Term v loc -> Maybe (Term v loc)
resolve Term v loc
t
        resolve :: Term v loc -> Maybe (Term v loc)
resolve (Term.Blank' (B.Recorded (B.Resolve loc
loc String
name)))
          | String
name String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== Text -> String
Text.unpack Text
s = Term v loc -> Maybe (Term v loc)
forall a. a -> Maybe a
Just (loc
loc loc -> Term v loc -> Term v loc
forall a b. a -> Term (F v loc loc) v b -> Term (F v loc loc) v a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ Term v loc
r)
        resolve Term v loc
_ = Maybe (Term v loc)
forall a. Maybe a
Nothing

    -- Returns Nothing for irrelevant notes
    resolveNote ::
      Env v loc ->
      Context.InfoNote v loc ->
      Result (Notes v loc) (Maybe (Resolution v loc))
    resolveNote :: Env v loc
-> InfoNote v loc
-> MaybeT
     (WriterT (Notes v loc) Identity) (Maybe (Resolution v loc))
resolveNote Env v loc
env = \case
      Context.SolvedBlank (B.Resolve loc
loc String
str) v
v Type v loc
it -> do
        let shortname :: Name
shortname = HasCallStack => Text -> Name
Text -> Name
Name.unsafeParseText (String -> Text
Text.pack String
str)
            matches :: [NamedReference v loc]
matches =
              Env v loc
env.termsByShortname
                Map Name [Either Name (NamedReference v loc)]
-> (Map Name [Either Name (NamedReference v loc)]
    -> [Either Name (NamedReference v loc)])
-> [Either Name (NamedReference v loc)]
forall a b. a -> (a -> b) -> b
& [Either Name (NamedReference v loc)]
-> Name
-> Map Name [Either Name (NamedReference v loc)]
-> [Either Name (NamedReference v loc)]
forall k a. Ord k => a -> k -> Map k a -> a
Map.findWithDefault [] Name
shortname
                [Either Name (NamedReference v loc)]
-> ([Either Name (NamedReference v loc)] -> [NamedReference v loc])
-> [NamedReference v loc]
forall a b. a -> (a -> b) -> b
& (Either Name (NamedReference v loc)
 -> Maybe (NamedReference v loc))
-> [Either Name (NamedReference v loc)] -> [NamedReference v loc]
forall a b. (a -> Maybe b) -> [a] -> [b]
forall (f :: * -> *) a b.
Filterable f =>
(a -> Maybe b) -> f a -> f b
mapMaybe \case
                  Left Name
longname -> Name
-> Map Name (NamedReference v loc) -> Maybe (NamedReference v loc)
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Name
longname Env v loc
env.topLevelComponents
                  Right NamedReference v loc
namedRef -> NamedReference v loc -> Maybe (NamedReference v loc)
forall a. a -> Maybe a
Just NamedReference v loc
namedRef
        [Suggestion v loc]
suggestions <- (NamedReference v loc
 -> MaybeT
      (WriterT (Notes v loc) Identity) (Maybe (Suggestion v loc)))
-> [NamedReference v loc]
-> MaybeT (WriterT (Notes v loc) Identity) [Suggestion v loc]
forall (t :: * -> *) (f :: * -> *) a b.
(Witherable t, Applicative f) =>
(a -> f (Maybe b)) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f (Maybe b)) -> [a] -> f [b]
wither (Type v loc
-> NamedReference v loc
-> MaybeT
     (WriterT (Notes v loc) Identity) (Maybe (Suggestion v loc))
resolve Type v loc
it) [NamedReference v loc]
matches
        pure $
          Resolution v loc -> Maybe (Resolution v loc)
forall a. a -> Maybe a
Just
            Resolution
              { $sel:resolvedName:Resolution :: Text
resolvedName = String -> Text
Text.pack String
str,
                $sel:inferredType:Resolution :: Type v loc
inferredType = Type v loc
it,
                $sel:resolvedLoc:Resolution :: loc
resolvedLoc = loc
loc,
                v
$sel:v:Resolution :: v
v :: v
v,
                [Suggestion v loc]
$sel:suggestions:Resolution :: [Suggestion v loc]
suggestions :: [Suggestion v loc]
suggestions
              }
      -- Solve the case where we have a placeholder for a missing result
      -- at the end of a block. This is always an error.
      Context.SolvedBlank (B.MissingResultPlaceholder loc
loc) v
v Type v loc
it ->
        Maybe (Resolution v loc)
-> MaybeT
     (WriterT (Notes v loc) Identity) (Maybe (Resolution v loc))
forall a. a -> MaybeT (WriterT (Notes v loc) Identity) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Maybe (Resolution v loc)
 -> MaybeT
      (WriterT (Notes v loc) Identity) (Maybe (Resolution v loc)))
-> (Resolution v loc -> Maybe (Resolution v loc))
-> Resolution v loc
-> MaybeT
     (WriterT (Notes v loc) Identity) (Maybe (Resolution v loc))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Resolution v loc -> Maybe (Resolution v loc)
forall a. a -> Maybe a
Just (Resolution v loc
 -> MaybeT
      (WriterT (Notes v loc) Identity) (Maybe (Resolution v loc)))
-> Resolution v loc
-> MaybeT
     (WriterT (Notes v loc) Identity) (Maybe (Resolution v loc))
forall a b. (a -> b) -> a -> b
$ Text
-> Type v loc -> loc -> v -> [Suggestion v loc] -> Resolution v loc
forall v loc.
Text
-> Type v loc -> loc -> v -> [Suggestion v loc] -> Resolution v loc
Resolution Text
"_" Type v loc
it loc
loc v
v []
      InfoNote v loc
note -> do
        InfoNote v loc -> Result (Notes v loc) ()
forall (f :: * -> *) v loc.
Monad f =>
InfoNote v loc -> ResultT (Notes v loc) f ()
btw InfoNote v loc
note
        pure Maybe (Resolution v loc)
forall a. Maybe a
Nothing

    dedupe :: [Context.Suggestion v loc] -> [Context.Suggestion v loc]
    dedupe :: [Suggestion v loc] -> [Suggestion v loc]
dedupe =
      (Suggestion v loc -> Replacement v)
-> [Suggestion v loc] -> [Suggestion v loc]
forall (f :: * -> *) b a.
(Foldable f, Ord b) =>
(a -> b) -> f a -> [a]
uniqueBy Suggestion v loc -> Replacement v
forall v loc. Suggestion v loc -> Replacement v
Context.suggestionReplacement

    resolve ::
      Context.Type v loc ->
      NamedReference v loc ->
      Result (Notes v loc) (Maybe (Context.Suggestion v loc))
    resolve :: Type v loc
-> NamedReference v loc
-> MaybeT
     (WriterT (Notes v loc) Identity) (Maybe (Suggestion v loc))
resolve Type v loc
inferredType (NamedReference Name
fqn Type v loc
foundType Replacement v
replace) =
      -- We found a name that matches. See if the type matches too.
      case Type v loc -> Type v loc -> Either (CompilerBug v loc) Bool
forall v loc.
(Var v, Ord loc) =>
Type v loc -> Type v loc -> Either (CompilerBug v loc) Bool
Context.isSubtype (Type v loc -> Type v loc
forall v a b. Ord v => Type v a -> Type (TypeVar b v) a
TypeVar.liftType Type v loc
foundType) (Type v loc -> Type v loc
forall v loc. (Var v, Ord loc) => Type v loc -> Type v loc
Context.relax Type v loc
inferredType) of
        Left CompilerBug v loc
bug -> Maybe (Suggestion v loc)
forall a. Maybe a
Nothing Maybe (Suggestion v loc)
-> Result (Notes v loc) ()
-> MaybeT
     (WriterT (Notes v loc) Identity) (Maybe (Suggestion v loc))
forall a b.
a
-> MaybeT (WriterT (Notes v loc) Identity) b
-> MaybeT (WriterT (Notes v loc) Identity) a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ CompilerBug v loc -> Result (Notes v loc) ()
forall v loc. CompilerBug v loc -> Result (Notes v loc) ()
compilerBug CompilerBug v loc
bug
        -- Suggest the import if the type matches.
        Right Bool
b ->
          Maybe (Suggestion v loc)
-> MaybeT
     (WriterT (Notes v loc) Identity) (Maybe (Suggestion v loc))
forall a. a -> MaybeT (WriterT (Notes v loc) Identity) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Maybe (Suggestion v loc)
 -> MaybeT
      (WriterT (Notes v loc) Identity) (Maybe (Suggestion v loc)))
-> (Suggestion v loc -> Maybe (Suggestion v loc))
-> Suggestion v loc
-> MaybeT
     (WriterT (Notes v loc) Identity) (Maybe (Suggestion v loc))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Suggestion v loc -> Maybe (Suggestion v loc)
forall a. a -> Maybe a
Just (Suggestion v loc
 -> MaybeT
      (WriterT (Notes v loc) Identity) (Maybe (Suggestion v loc)))
-> Suggestion v loc
-> MaybeT
     (WriterT (Notes v loc) Identity) (Maybe (Suggestion v loc))
forall a b. (a -> b) -> a -> b
$
            Name
-> Type v loc
-> Replacement v
-> SuggestionMatch
-> Suggestion v loc
forall v loc.
Name
-> Type v loc
-> Replacement v
-> SuggestionMatch
-> Suggestion v loc
Context.Suggestion
              Name
fqn
              (Type v loc -> Type v loc
forall v a b. Ord v => Type v a -> Type (TypeVar b v) a
TypeVar.liftType Type v loc
foundType)
              Replacement v
replace
              (if Bool
b then SuggestionMatch
Context.Exact else SuggestionMatch
Context.WrongType)

-- | Check whether a term matches a type, using a
-- function to resolve the type of @Ref@ constructors
-- contained in the term. Returns @typ@ if successful,
-- and a note about typechecking failure otherwise.
check ::
  (Monad f, Var v, BuiltinAnnotation loc, Ord loc, Show loc) =>
  PrettyPrintEnv ->
  Env v loc ->
  Term v loc ->
  Type v loc ->
  ResultT (Notes v loc) f (Type v loc)
check :: forall (f :: * -> *) v loc.
(Monad f, Var v, BuiltinAnnotation loc, Ord loc, Show loc) =>
PrettyPrintEnv
-> Env v loc
-> Term v loc
-> Type v loc
-> ResultT (Notes v loc) f (Type v loc)
check PrettyPrintEnv
ppe Env v loc
env Term v loc
term Type v loc
typ =
  PrettyPrintEnv
-> PatternMatchCoverageCheckAndKindInferenceSwitch
-> Env v loc
-> Term v loc
-> ResultT (Notes v loc) f (Type v loc)
forall (f :: * -> *) v loc.
(Monad f, Var v, BuiltinAnnotation loc, Ord loc, Show loc) =>
PrettyPrintEnv
-> PatternMatchCoverageCheckAndKindInferenceSwitch
-> Env v loc
-> Term v loc
-> ResultT (Notes v loc) f (Type v loc)
synthesize
    PrettyPrintEnv
ppe
    PatternMatchCoverageCheckAndKindInferenceSwitch
Context.PatternMatchCoverageCheckAndKindInferenceSwitch'Enabled
    Env v loc
env
    (loc -> Term v loc -> Type v loc -> Term v loc
forall v a vt at ap.
Ord v =>
a -> Term2 vt at ap v a -> Type vt at -> Term2 vt at ap v a
Term.ann (Term v loc -> loc
forall (f :: * -> *) v a. Term f v a -> a
ABT.annotation Term v loc
term) Term v loc
term Type v loc
typ)

-- | `checkAdmissible' e t` tests that `(f : t -> r) e` is well-typed.
-- If `t` has quantifiers, these are moved outside, so if `t : forall a . a`,
-- this will check that `(f : forall a . a -> a) e` is well typed.
-- checkAdmissible' :: Var v => Term v -> Type v -> Either Note (Type v)
-- checkAdmissible' term typ =
--   synthesize' (Term.blank() `Term.ann_` tweak typ `Term.app_` term)
--   where
--     tweak (Type.ForallNamed' v body) = Type.forall() v (tweak body)
--     tweak t = Type.arrow() t t
-- | Returns `True` if the expression is well-typed, `False` otherwise
wellTyped :: (Monad f, Var v, BuiltinAnnotation loc, Ord loc, Show loc) => PrettyPrintEnv -> Env v loc -> Term v loc -> f Bool
wellTyped :: forall (f :: * -> *) v loc.
(Monad f, Var v, BuiltinAnnotation loc, Ord loc, Show loc) =>
PrettyPrintEnv -> Env v loc -> Term v loc -> f Bool
wellTyped PrettyPrintEnv
ppe Env v loc
env Term v loc
term = (Maybe (Type v loc), Notes v loc) -> Bool
forall {a} {b}. (Maybe a, b) -> Bool
go ((Maybe (Type v loc), Notes v loc) -> Bool)
-> f (Maybe (Type v loc), Notes v loc) -> f Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ResultT (Notes v loc) f (Type v loc)
-> f (Maybe (Type v loc), Notes v loc)
forall notes (f :: * -> *) a.
ResultT notes f a -> f (Maybe a, notes)
runResultT (PrettyPrintEnv
-> PatternMatchCoverageCheckAndKindInferenceSwitch
-> Env v loc
-> Term v loc
-> ResultT (Notes v loc) f (Type v loc)
forall (f :: * -> *) v loc.
(Monad f, Var v, BuiltinAnnotation loc, Ord loc, Show loc) =>
PrettyPrintEnv
-> PatternMatchCoverageCheckAndKindInferenceSwitch
-> Env v loc
-> Term v loc
-> ResultT (Notes v loc) f (Type v loc)
synthesize PrettyPrintEnv
ppe PatternMatchCoverageCheckAndKindInferenceSwitch
Context.PatternMatchCoverageCheckAndKindInferenceSwitch'Enabled Env v loc
env Term v loc
term)
  where
    go :: (Maybe a, b) -> Bool
go (Maybe a
may, b
_) = Maybe a -> Bool
forall a. Maybe a -> Bool
isJust Maybe a
may

-- | @subtype a b@ is @Right b@ iff @f x@ is well-typed given
-- @x : a@ and @f : b -> t@. That is, if a value of type `a`
-- can be passed to a function expecting a `b`, then `subtype a b`
-- returns `Right b`. This function returns @Left note@ with information
-- about the reason for subtyping failure otherwise.
--
-- Example: @subtype (forall a. a -> a) (Int -> Int)@ returns @Right (Int -> Int)@.
-- subtype :: Var v => Type v -> Type v -> Either Note (Type v)
-- subtype t1 t2 = error "todo"
-- let (t1', t2') = (ABT.vmap TypeVar.Universal t1, ABT.vmap TypeVar.Universal t2)
-- in case Context.runM (Context.subtype t1' t2')
--                      (Context.MEnv Context.env0 [] Map.empty True) of
--   Left e -> Left e
--   Right _ -> Right t2

-- | Returns true if @subtype t1 t2@ returns @Right@, false otherwise
-- isSubtype :: Var v => Type v -> Type v -> Bool
-- isSubtype t1 t2 = case subtype t1 t2 of
--   Left _ -> False
--   Right _ -> True

-- | Returns true if the two type are equal, up to alpha equivalence and
-- order of quantifier introduction. Note that alpha equivalence considers:
-- `forall b a . a -> b -> a` and
-- `forall a b . a -> b -> a` to be different types
-- equals :: Var v => Type v -> Type v -> Bool
-- equals t1 t2 = isSubtype t1 t2 && isSubtype t2 t1