{-# LANGUAGE CPP #-}

module Covenant.Internal.Unification
  ( TypeAppError (..),
    checkApp,
    runUnifyM,
    UnifyM,
  )
where

import Control.Monad (foldM, unless, when)
import Data.Ord (comparing)
#if __GLASGOW_HASKELL__==908
import Data.Foldable (foldl')
#endif
import Control.Monad.Except (MonadError, catchError, throwError)
import Control.Monad.Reader (MonadReader, ReaderT (runReaderT), ask)
import Covenant.Data (DatatypeInfo)
import Covenant.Index (Index, intCount, intIndex)
import Covenant.Internal.Rename (RenameError, renameDatatypeInfo)
import Covenant.Internal.Type
  ( AbstractTy,
    BuiltinFlatT,
    CompT (CompT),
    CompTBody (CompTBody),
    Renamed (Rigid, Unifiable, Wildcard),
    TyName,
    ValT (Abstraction, BuiltinFlat, Datatype, ThunkT),
  )
import Data.Kind (Type)
import Data.Map (Map)
import Data.Map.Merge.Strict qualified as Merge
import Data.Map.Strict qualified as Map
import Data.Maybe (fromJust, mapMaybe)
import Data.Set (Set)
import Data.Set qualified as Set
import Data.Text (Text)
import Data.Vector (Vector)
import Data.Vector qualified as Vector
import Data.Vector.NonEmpty (NonEmptyVector)
import Data.Vector.NonEmpty qualified as NonEmpty
import Data.Word (Word64)
import Optics.Core (ix, preview, view)

-- | Possible errors resulting from applications of arguments to functions.
--
-- @since 1.0.0
data TypeAppError
  = -- | The final type after all arguments are applied is @forall a . a@.
    LeakingUnifiable (Index "tyvar")
  | -- | A wildcard (thus, a skolem) escaped its scope.
    LeakingWildcard Word64 Int (Index "tyvar")
  | -- | We were given too many arguments.
    ExcessArgs (CompT Renamed) (Vector (Maybe (ValT Renamed)))
  | -- | We weren't given enough arguments.
    --
    -- @since 1.1.0
    InsufficientArgs Int (CompT Renamed) [Maybe (ValT Renamed)]
  | -- | The expected type (first field) and actual type (second field) do not
    -- unify.
    DoesNotUnify (ValT Renamed) (ValT Renamed)
  | -- | No datatype info associated with requested TyName
    --
    -- @since 1.1.0
    NoDatatypeInfo TyName
  | -- | No BB form. The only datatypes which should lack one are those isomorphic to `Void`.
    --
    -- @since 1.1.0
    NoBBForm TyName
  | -- | Datatype renaming failed.
    --
    -- @since 1.1.0
    DatatypeInfoRenameFailed TyName RenameError
  | -- | Something happened that definitely should not have. For right now, this means: The BB form of a datatype isn't a thunk
    --   (but it might be useful to keep this around as a catchall for things that really shouldn't happen).
    --
    -- @since 1.1.0
    ImpossibleHappened Text
  deriving stock
    ( -- | @since 1.0.0
      TypeAppError -> TypeAppError -> Bool
(TypeAppError -> TypeAppError -> Bool)
-> (TypeAppError -> TypeAppError -> Bool) -> Eq TypeAppError
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: TypeAppError -> TypeAppError -> Bool
== :: TypeAppError -> TypeAppError -> Bool
$c/= :: TypeAppError -> TypeAppError -> Bool
/= :: TypeAppError -> TypeAppError -> Bool
Eq,
      -- | @since 1.0.0
      Int -> TypeAppError -> ShowS
[TypeAppError] -> ShowS
TypeAppError -> String
(Int -> TypeAppError -> ShowS)
-> (TypeAppError -> String)
-> ([TypeAppError] -> ShowS)
-> Show TypeAppError
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> TypeAppError -> ShowS
showsPrec :: Int -> TypeAppError -> ShowS
$cshow :: TypeAppError -> String
show :: TypeAppError -> String
$cshowList :: [TypeAppError] -> ShowS
showList :: [TypeAppError] -> ShowS
Show
    )

{- This will probably only get used directly in testing and we'll use capabilities w/ the class everywhere else? -}
newtype UnifyM a = UnifyM (ReaderT (Map TyName (DatatypeInfo AbstractTy)) (Either TypeAppError) a)
  deriving
    ( -- | @since 1.1.0
      (forall a b. (a -> b) -> UnifyM a -> UnifyM b)
-> (forall a b. a -> UnifyM b -> UnifyM a) -> Functor UnifyM
forall a b. a -> UnifyM b -> UnifyM a
forall a b. (a -> b) -> UnifyM a -> UnifyM b
forall (f :: Type -> Type).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
$cfmap :: forall a b. (a -> b) -> UnifyM a -> UnifyM b
fmap :: forall a b. (a -> b) -> UnifyM a -> UnifyM b
$c<$ :: forall a b. a -> UnifyM b -> UnifyM a
<$ :: forall a b. a -> UnifyM b -> UnifyM a
Functor,
      Functor UnifyM
Functor UnifyM =>
(forall a. a -> UnifyM a)
-> (forall a b. UnifyM (a -> b) -> UnifyM a -> UnifyM b)
-> (forall a b c.
    (a -> b -> c) -> UnifyM a -> UnifyM b -> UnifyM c)
-> (forall a b. UnifyM a -> UnifyM b -> UnifyM b)
-> (forall a b. UnifyM a -> UnifyM b -> UnifyM a)
-> Applicative UnifyM
forall a. a -> UnifyM a
forall a b. UnifyM a -> UnifyM b -> UnifyM a
forall a b. UnifyM a -> UnifyM b -> UnifyM b
forall a b. UnifyM (a -> b) -> UnifyM a -> UnifyM b
forall a b c. (a -> b -> c) -> UnifyM a -> UnifyM b -> UnifyM c
forall (f :: Type -> Type).
Functor f =>
(forall a. a -> f a)
-> (forall a b. f (a -> b) -> f a -> f b)
-> (forall a b c. (a -> b -> c) -> f a -> f b -> f c)
-> (forall a b. f a -> f b -> f b)
-> (forall a b. f a -> f b -> f a)
-> Applicative f
$cpure :: forall a. a -> UnifyM a
pure :: forall a. a -> UnifyM a
$c<*> :: forall a b. UnifyM (a -> b) -> UnifyM a -> UnifyM b
<*> :: forall a b. UnifyM (a -> b) -> UnifyM a -> UnifyM b
$cliftA2 :: forall a b c. (a -> b -> c) -> UnifyM a -> UnifyM b -> UnifyM c
liftA2 :: forall a b c. (a -> b -> c) -> UnifyM a -> UnifyM b -> UnifyM c
$c*> :: forall a b. UnifyM a -> UnifyM b -> UnifyM b
*> :: forall a b. UnifyM a -> UnifyM b -> UnifyM b
$c<* :: forall a b. UnifyM a -> UnifyM b -> UnifyM a
<* :: forall a b. UnifyM a -> UnifyM b -> UnifyM a
Applicative,
      Applicative UnifyM
Applicative UnifyM =>
(forall a b. UnifyM a -> (a -> UnifyM b) -> UnifyM b)
-> (forall a b. UnifyM a -> UnifyM b -> UnifyM b)
-> (forall a. a -> UnifyM a)
-> Monad UnifyM
forall a. a -> UnifyM a
forall a b. UnifyM a -> UnifyM b -> UnifyM b
forall a b. UnifyM a -> (a -> UnifyM b) -> UnifyM b
forall (m :: Type -> Type).
Applicative m =>
(forall a b. m a -> (a -> m b) -> m b)
-> (forall a b. m a -> m b -> m b)
-> (forall a. a -> m a)
-> Monad m
$c>>= :: forall a b. UnifyM a -> (a -> UnifyM b) -> UnifyM b
>>= :: forall a b. UnifyM a -> (a -> UnifyM b) -> UnifyM b
$c>> :: forall a b. UnifyM a -> UnifyM b -> UnifyM b
>> :: forall a b. UnifyM a -> UnifyM b -> UnifyM b
$creturn :: forall a. a -> UnifyM a
return :: forall a. a -> UnifyM a
Monad,
      MonadReader (Map TyName (DatatypeInfo AbstractTy)),
      MonadError TypeAppError
    )
    via (ReaderT (Map TyName (DatatypeInfo AbstractTy)) (Either TypeAppError))

runUnifyM :: Map TyName (DatatypeInfo AbstractTy) -> UnifyM a -> Either TypeAppError a
runUnifyM :: forall a.
Map TyName (DatatypeInfo AbstractTy)
-> UnifyM a -> Either TypeAppError a
runUnifyM Map TyName (DatatypeInfo AbstractTy)
tyDict (UnifyM ReaderT
  (Map TyName (DatatypeInfo AbstractTy)) (Either TypeAppError) a
act) = ReaderT
  (Map TyName (DatatypeInfo AbstractTy)) (Either TypeAppError) a
-> Map TyName (DatatypeInfo AbstractTy) -> Either TypeAppError a
forall r (m :: Type -> Type) a. ReaderT r m a -> r -> m a
runReaderT ReaderT
  (Map TyName (DatatypeInfo AbstractTy)) (Either TypeAppError) a
act Map TyName (DatatypeInfo AbstractTy)
tyDict

lookupDatatypeInfo ::
  TyName ->
  UnifyM (DatatypeInfo Renamed)
lookupDatatypeInfo :: TyName -> UnifyM (DatatypeInfo Renamed)
lookupDatatypeInfo TyName
tn =
  UnifyM (Map TyName (DatatypeInfo AbstractTy))
forall r (m :: Type -> Type). MonadReader r m => m r
ask UnifyM (Map TyName (DatatypeInfo AbstractTy))
-> (Map TyName (DatatypeInfo AbstractTy)
    -> UnifyM (DatatypeInfo Renamed))
-> UnifyM (DatatypeInfo Renamed)
forall a b. UnifyM a -> (a -> UnifyM b) -> UnifyM b
forall (m :: Type -> Type) a b. Monad m => m a -> (a -> m b) -> m b
>>= \Map TyName (DatatypeInfo AbstractTy)
tyDict -> case Optic'
  (IxKind (Map TyName (DatatypeInfo AbstractTy)))
  NoIx
  (Map TyName (DatatypeInfo AbstractTy))
  (DatatypeInfo AbstractTy)
-> Map TyName (DatatypeInfo AbstractTy)
-> Maybe (DatatypeInfo AbstractTy)
forall k (is :: IxList) s a.
Is k An_AffineFold =>
Optic' k is s a -> s -> Maybe a
preview (Index (Map TyName (DatatypeInfo AbstractTy))
-> Optic'
     (IxKind (Map TyName (DatatypeInfo AbstractTy)))
     NoIx
     (Map TyName (DatatypeInfo AbstractTy))
     (IxValue (Map TyName (DatatypeInfo AbstractTy)))
forall m. Ixed m => Index m -> Optic' (IxKind m) NoIx m (IxValue m)
ix Index (Map TyName (DatatypeInfo AbstractTy))
TyName
tn) Map TyName (DatatypeInfo AbstractTy)
tyDict of
    Maybe (DatatypeInfo AbstractTy)
Nothing -> TypeAppError -> UnifyM (DatatypeInfo Renamed)
forall a. TypeAppError -> UnifyM a
forall e (m :: Type -> Type) a. MonadError e m => e -> m a
throwError (TypeAppError -> UnifyM (DatatypeInfo Renamed))
-> TypeAppError -> UnifyM (DatatypeInfo Renamed)
forall a b. (a -> b) -> a -> b
$ TyName -> TypeAppError
NoDatatypeInfo TyName
tn
    Just DatatypeInfo AbstractTy
dti -> (RenameError -> UnifyM (DatatypeInfo Renamed))
-> (DatatypeInfo Renamed -> UnifyM (DatatypeInfo Renamed))
-> Either RenameError (DatatypeInfo Renamed)
-> UnifyM (DatatypeInfo Renamed)
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either (TypeAppError -> UnifyM (DatatypeInfo Renamed)
forall a. TypeAppError -> UnifyM a
forall e (m :: Type -> Type) a. MonadError e m => e -> m a
throwError (TypeAppError -> UnifyM (DatatypeInfo Renamed))
-> (RenameError -> TypeAppError)
-> RenameError
-> UnifyM (DatatypeInfo Renamed)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TyName -> RenameError -> TypeAppError
DatatypeInfoRenameFailed TyName
tn) DatatypeInfo Renamed -> UnifyM (DatatypeInfo Renamed)
forall a. a -> UnifyM a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (Either RenameError (DatatypeInfo Renamed)
 -> UnifyM (DatatypeInfo Renamed))
-> Either RenameError (DatatypeInfo Renamed)
-> UnifyM (DatatypeInfo Renamed)
forall a b. (a -> b) -> a -> b
$ DatatypeInfo AbstractTy
-> Either RenameError (DatatypeInfo Renamed)
renameDatatypeInfo DatatypeInfo AbstractTy
dti

lookupBBForm :: TyName -> UnifyM (ValT Renamed)
lookupBBForm :: TyName -> UnifyM (ValT Renamed)
lookupBBForm TyName
tn =
  TyName -> UnifyM (DatatypeInfo Renamed)
lookupDatatypeInfo TyName
tn UnifyM (DatatypeInfo Renamed)
-> (DatatypeInfo Renamed -> UnifyM (ValT Renamed))
-> UnifyM (ValT Renamed)
forall a b. UnifyM a -> (a -> UnifyM b) -> UnifyM b
forall (m :: Type -> Type) a b. Monad m => m a -> (a -> m b) -> m b
>>= \DatatypeInfo Renamed
dti -> case Optic' A_Lens NoIx (DatatypeInfo Renamed) (Maybe (ValT Renamed))
-> DatatypeInfo Renamed -> Maybe (ValT Renamed)
forall k (is :: IxList) s a.
Is k A_Getter =>
Optic' k is s a -> s -> a
view Optic' A_Lens NoIx (DatatypeInfo Renamed) (Maybe (ValT Renamed))
#bbForm DatatypeInfo Renamed
dti of
    Maybe (ValT Renamed)
Nothing -> TypeAppError -> UnifyM (ValT Renamed)
forall a. TypeAppError -> UnifyM a
forall e (m :: Type -> Type) a. MonadError e m => e -> m a
throwError (TypeAppError -> UnifyM (ValT Renamed))
-> TypeAppError -> UnifyM (ValT Renamed)
forall a b. (a -> b) -> a -> b
$ TyName -> TypeAppError
NoBBForm TyName
tn
    Just ValT Renamed
bbForm -> ValT Renamed -> UnifyM (ValT Renamed)
forall a. a -> UnifyM a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure ValT Renamed
bbForm

-- | Given information about in-scope datatypes, a computation type, and a list
-- of arguments (some of which may be errors), try to construct the type of the
-- result of the application of those arguments to the computation.
--
-- @since 1.0.0
checkApp ::
  Map TyName (DatatypeInfo AbstractTy) ->
  CompT Renamed ->
  [Maybe (ValT Renamed)] ->
  Either TypeAppError (ValT Renamed)
checkApp :: Map TyName (DatatypeInfo AbstractTy)
-> CompT Renamed
-> [Maybe (ValT Renamed)]
-> Either TypeAppError (ValT Renamed)
checkApp Map TyName (DatatypeInfo AbstractTy)
tyDict CompT Renamed
f [Maybe (ValT Renamed)]
args = Map TyName (DatatypeInfo AbstractTy)
-> UnifyM (ValT Renamed) -> Either TypeAppError (ValT Renamed)
forall a.
Map TyName (DatatypeInfo AbstractTy)
-> UnifyM a -> Either TypeAppError a
runUnifyM Map TyName (DatatypeInfo AbstractTy)
tyDict (UnifyM (ValT Renamed) -> Either TypeAppError (ValT Renamed))
-> UnifyM (ValT Renamed) -> Either TypeAppError (ValT Renamed)
forall a b. (a -> b) -> a -> b
$ CompT Renamed -> [Maybe (ValT Renamed)] -> UnifyM (ValT Renamed)
checkApp' CompT Renamed
f [Maybe (ValT Renamed)]
args

checkApp' ::
  CompT Renamed ->
  [Maybe (ValT Renamed)] ->
  UnifyM (ValT Renamed)
checkApp' :: CompT Renamed -> [Maybe (ValT Renamed)] -> UnifyM (ValT Renamed)
checkApp' f :: CompT Renamed
f@(CompT Count "tyvar"
_ (CompTBody NonEmptyVector (ValT Renamed)
xs)) [Maybe (ValT Renamed)]
ys = do
  let (ValT Renamed
curr, Vector (ValT Renamed)
rest) = NonEmptyVector (ValT Renamed)
-> (ValT Renamed, Vector (ValT Renamed))
forall a. NonEmptyVector a -> (a, Vector a)
NonEmpty.uncons NonEmptyVector (ValT Renamed)
xs
      numArgsExpected :: Int
numArgsExpected = NonEmptyVector (ValT Renamed) -> Int
forall a. NonEmptyVector a -> Int
NonEmpty.length NonEmptyVector (ValT Renamed)
xs Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1
      numArgsActual :: Int
numArgsActual = [Maybe (ValT Renamed)] -> Int
forall a. [a] -> Int
forall (t :: Type -> Type) a. Foldable t => t a -> Int
length [Maybe (ValT Renamed)]
ys
  Bool -> UnifyM () -> UnifyM ()
forall (f :: Type -> Type). Applicative f => Bool -> f () -> f ()
when (Int
numArgsActual Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
numArgsExpected) (UnifyM () -> UnifyM ()) -> UnifyM () -> UnifyM ()
forall a b. (a -> b) -> a -> b
$
    TypeAppError -> UnifyM ()
forall a. TypeAppError -> UnifyM a
forall e (m :: Type -> Type) a. MonadError e m => e -> m a
throwError (TypeAppError -> UnifyM ()) -> TypeAppError -> UnifyM ()
forall a b. (a -> b) -> a -> b
$
      Int -> CompT Renamed -> [Maybe (ValT Renamed)] -> TypeAppError
InsufficientArgs Int
numArgsActual CompT Renamed
f [Maybe (ValT Renamed)]
ys
  Bool -> UnifyM () -> UnifyM ()
forall (f :: Type -> Type). Applicative f => Bool -> f () -> f ()
when (Int
numArgsExpected Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
numArgsActual) (UnifyM () -> UnifyM ()) -> UnifyM () -> UnifyM ()
forall a b. (a -> b) -> a -> b
$
    TypeAppError -> UnifyM ()
forall a. TypeAppError -> UnifyM a
forall e (m :: Type -> Type) a. MonadError e m => e -> m a
throwError (TypeAppError -> UnifyM ()) -> TypeAppError -> UnifyM ()
forall a b. (a -> b) -> a -> b
$
      CompT Renamed -> Vector (Maybe (ValT Renamed)) -> TypeAppError
ExcessArgs CompT Renamed
f ([Maybe (ValT Renamed)] -> Vector (Maybe (ValT Renamed))
forall a. [a] -> Vector a
Vector.fromList [Maybe (ValT Renamed)]
ys)
  ValT Renamed
-> [ValT Renamed]
-> [Maybe (ValT Renamed)]
-> UnifyM (ValT Renamed)
go ValT Renamed
curr (Vector (ValT Renamed) -> [ValT Renamed]
forall a. Vector a -> [a]
Vector.toList Vector (ValT Renamed)
rest) [Maybe (ValT Renamed)]
ys
  where
    go ::
      ValT Renamed ->
      [ValT Renamed] ->
      [Maybe (ValT Renamed)] ->
      UnifyM (ValT Renamed)
    go :: ValT Renamed
-> [ValT Renamed]
-> [Maybe (ValT Renamed)]
-> UnifyM (ValT Renamed)
go ValT Renamed
currParam [ValT Renamed]
restParams [Maybe (ValT Renamed)]
args = case [ValT Renamed]
restParams of
      [] -> case [Maybe (ValT Renamed)]
args of
        -- If we got here, currParam is the resulting type after all
        -- substitutions have been applied.
        [] -> ValT Renamed -> UnifyM (ValT Renamed)
fixUp ValT Renamed
currParam
        [Maybe (ValT Renamed)]
_ -> TypeAppError -> UnifyM (ValT Renamed)
forall a. TypeAppError -> UnifyM a
forall e (m :: Type -> Type) a. MonadError e m => e -> m a
throwError (TypeAppError -> UnifyM (ValT Renamed))
-> ([Maybe (ValT Renamed)] -> TypeAppError)
-> [Maybe (ValT Renamed)]
-> UnifyM (ValT Renamed)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CompT Renamed -> Vector (Maybe (ValT Renamed)) -> TypeAppError
ExcessArgs CompT Renamed
f (Vector (Maybe (ValT Renamed)) -> TypeAppError)
-> ([Maybe (ValT Renamed)] -> Vector (Maybe (ValT Renamed)))
-> [Maybe (ValT Renamed)]
-> TypeAppError
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Maybe (ValT Renamed)] -> Vector (Maybe (ValT Renamed))
forall a. [a] -> Vector a
Vector.fromList ([Maybe (ValT Renamed)] -> UnifyM (ValT Renamed))
-> [Maybe (ValT Renamed)] -> UnifyM (ValT Renamed)
forall a b. (a -> b) -> a -> b
$ [Maybe (ValT Renamed)]
args
      [ValT Renamed]
_ -> case [Maybe (ValT Renamed)]
args of
        [] -> TypeAppError -> UnifyM (ValT Renamed)
forall a. TypeAppError -> UnifyM a
forall e (m :: Type -> Type) a. MonadError e m => e -> m a
throwError (TypeAppError -> UnifyM (ValT Renamed))
-> TypeAppError -> UnifyM (ValT Renamed)
forall a b. (a -> b) -> a -> b
$ Int -> CompT Renamed -> [Maybe (ValT Renamed)] -> TypeAppError
InsufficientArgs ([Maybe (ValT Renamed)] -> Int
forall a. [a] -> Int
forall (t :: Type -> Type) a. Foldable t => t a -> Int
length [Maybe (ValT Renamed)]
args) CompT Renamed
f [Maybe (ValT Renamed)]
args
        (Maybe (ValT Renamed)
currArg : [Maybe (ValT Renamed)]
restArgs) -> do
          [ValT Renamed]
newRestParams <- case Maybe (ValT Renamed)
currArg of
            -- An error argument unifies with anything, as it's effectively
            -- `forall a . a`. Furthermore, it requires no substitutional
            -- changes. Thus, we can just skip it.
            Maybe (ValT Renamed)
Nothing -> [ValT Renamed] -> UnifyM [ValT Renamed]
forall a. a -> UnifyM a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure [ValT Renamed]
restParams
            Just ValT Renamed
currArg' -> do
              Map (Index "tyvar") (ValT Renamed)
subs <- UnifyM (Map (Index "tyvar") (ValT Renamed))
-> (TypeAppError -> UnifyM (Map (Index "tyvar") (ValT Renamed)))
-> UnifyM (Map (Index "tyvar") (ValT Renamed))
forall a. UnifyM a -> (TypeAppError -> UnifyM a) -> UnifyM a
forall e (m :: Type -> Type) a.
MonadError e m =>
m a -> (e -> m a) -> m a
catchError (ValT Renamed
-> ValT Renamed -> UnifyM (Map (Index "tyvar") (ValT Renamed))
unify ValT Renamed
currParam ValT Renamed
currArg') (ValT Renamed
-> ValT Renamed
-> TypeAppError
-> UnifyM (Map (Index "tyvar") (ValT Renamed))
forall a. ValT Renamed -> ValT Renamed -> TypeAppError -> UnifyM a
promoteUnificationError ValT Renamed
currParam ValT Renamed
currArg')
              [ValT Renamed] -> UnifyM [ValT Renamed]
forall a. a -> UnifyM a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure ([ValT Renamed] -> UnifyM [ValT Renamed])
-> (Map (Index "tyvar") (ValT Renamed) -> [ValT Renamed])
-> Map (Index "tyvar") (ValT Renamed)
-> UnifyM [ValT Renamed]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ([ValT Renamed] -> Index "tyvar" -> ValT Renamed -> [ValT Renamed])
-> [ValT Renamed]
-> Map (Index "tyvar") (ValT Renamed)
-> [ValT Renamed]
forall a k b. (a -> k -> b -> a) -> a -> Map k b -> a
Map.foldlWithKey' [ValT Renamed] -> Index "tyvar" -> ValT Renamed -> [ValT Renamed]
applySub [ValT Renamed]
restParams (Map (Index "tyvar") (ValT Renamed) -> UnifyM [ValT Renamed])
-> Map (Index "tyvar") (ValT Renamed) -> UnifyM [ValT Renamed]
forall a b. (a -> b) -> a -> b
$ Map (Index "tyvar") (ValT Renamed)
subs
          case [ValT Renamed]
newRestParams of
            [] -> TypeAppError -> UnifyM (ValT Renamed)
forall a. TypeAppError -> UnifyM a
forall e (m :: Type -> Type) a. MonadError e m => e -> m a
throwError (TypeAppError -> UnifyM (ValT Renamed))
-> TypeAppError -> UnifyM (ValT Renamed)
forall a b. (a -> b) -> a -> b
$ Int -> CompT Renamed -> [Maybe (ValT Renamed)] -> TypeAppError
InsufficientArgs ([Maybe (ValT Renamed)] -> Int
forall a. [a] -> Int
forall (t :: Type -> Type) a. Foldable t => t a -> Int
length [Maybe (ValT Renamed)]
args) CompT Renamed
f [Maybe (ValT Renamed)]
args
            (ValT Renamed
currParam' : [ValT Renamed]
restParams') -> ValT Renamed
-> [ValT Renamed]
-> [Maybe (ValT Renamed)]
-> UnifyM (ValT Renamed)
go ValT Renamed
currParam' [ValT Renamed]
restParams' [Maybe (ValT Renamed)]
restArgs

-- Helpers

applySub ::
  [ValT Renamed] ->
  Index "tyvar" ->
  ValT Renamed ->
  [ValT Renamed]
applySub :: [ValT Renamed] -> Index "tyvar" -> ValT Renamed -> [ValT Renamed]
applySub [ValT Renamed]
acc Index "tyvar"
index ValT Renamed
sub = (ValT Renamed -> ValT Renamed) -> [ValT Renamed] -> [ValT Renamed]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap (Index "tyvar" -> ValT Renamed -> ValT Renamed -> ValT Renamed
substitute Index "tyvar"
index ValT Renamed
sub) [ValT Renamed]
acc

substitute ::
  Index "tyvar" ->
  ValT Renamed ->
  ValT Renamed ->
  ValT Renamed
substitute :: Index "tyvar" -> ValT Renamed -> ValT Renamed -> ValT Renamed
substitute Index "tyvar"
index ValT Renamed
toSub = \case
  Abstraction Renamed
t -> case Renamed
t of
    Unifiable Index "tyvar"
ourIndex ->
      if Index "tyvar"
ourIndex Index "tyvar" -> Index "tyvar" -> Bool
forall a. Eq a => a -> a -> Bool
== Index "tyvar"
index
        then ValT Renamed
toSub
        else Renamed -> ValT Renamed
forall a. a -> ValT a
Abstraction Renamed
t
    Renamed
_ -> Renamed -> ValT Renamed
forall a. a -> ValT a
Abstraction Renamed
t
  ThunkT (CompT Count "tyvar"
abstractions (CompTBody NonEmptyVector (ValT Renamed)
xs)) ->
    CompT Renamed -> ValT Renamed
forall a. CompT a -> ValT a
ThunkT (CompT Renamed -> ValT Renamed)
-> (NonEmptyVector (ValT Renamed) -> CompT Renamed)
-> NonEmptyVector (ValT Renamed)
-> ValT Renamed
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Count "tyvar" -> CompTBody Renamed -> CompT Renamed
forall a. Count "tyvar" -> CompTBody a -> CompT a
CompT Count "tyvar"
abstractions (CompTBody Renamed -> CompT Renamed)
-> (NonEmptyVector (ValT Renamed) -> CompTBody Renamed)
-> NonEmptyVector (ValT Renamed)
-> CompT Renamed
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NonEmptyVector (ValT Renamed) -> CompTBody Renamed
forall a. NonEmptyVector (ValT a) -> CompTBody a
CompTBody (NonEmptyVector (ValT Renamed) -> CompTBody Renamed)
-> (NonEmptyVector (ValT Renamed) -> NonEmptyVector (ValT Renamed))
-> NonEmptyVector (ValT Renamed)
-> CompTBody Renamed
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (ValT Renamed -> ValT Renamed)
-> NonEmptyVector (ValT Renamed) -> NonEmptyVector (ValT Renamed)
forall a b. (a -> b) -> NonEmptyVector a -> NonEmptyVector b
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap (Index "tyvar" -> ValT Renamed -> ValT Renamed -> ValT Renamed
substitute Index "tyvar"
index ValT Renamed
toSub) (NonEmptyVector (ValT Renamed) -> ValT Renamed)
-> NonEmptyVector (ValT Renamed) -> ValT Renamed
forall a b. (a -> b) -> a -> b
$ NonEmptyVector (ValT Renamed)
xs
  BuiltinFlat BuiltinFlatT
t -> BuiltinFlatT -> ValT Renamed
forall a. BuiltinFlatT -> ValT a
BuiltinFlat BuiltinFlatT
t
  Datatype TyName
tn Vector (ValT Renamed)
args -> TyName -> Vector (ValT Renamed) -> ValT Renamed
forall a. TyName -> Vector (ValT a) -> ValT a
Datatype TyName
tn (Vector (ValT Renamed) -> ValT Renamed)
-> Vector (ValT Renamed) -> ValT Renamed
forall a b. (a -> b) -> a -> b
$ Index "tyvar" -> ValT Renamed -> ValT Renamed -> ValT Renamed
substitute Index "tyvar"
index ValT Renamed
toSub (ValT Renamed -> ValT Renamed)
-> Vector (ValT Renamed) -> Vector (ValT Renamed)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Vector (ValT Renamed)
args

-- Because unification is inherently recursive, if we find an error deep within
-- a type, the message will signify only the _part_ that fails to unify, not the
-- entire type. While potentially useful, this can be quite confusing,
-- especially with generated types. Thus, we use `catchError` with this
-- function, which effectively allows us to rename the types reported in
-- unification errors to whatever types 'wrap' them.
promoteUnificationError ::
  ValT Renamed ->
  ValT Renamed ->
  TypeAppError ->
  UnifyM a
promoteUnificationError :: forall a. ValT Renamed -> ValT Renamed -> TypeAppError -> UnifyM a
promoteUnificationError ValT Renamed
topLevelExpected ValT Renamed
topLevelActual =
  TypeAppError -> UnifyM a
forall a. TypeAppError -> UnifyM a
forall e (m :: Type -> Type) a. MonadError e m => e -> m a
throwError (TypeAppError -> UnifyM a)
-> (TypeAppError -> TypeAppError) -> TypeAppError -> UnifyM a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. \case
    DoesNotUnify ValT Renamed
_ ValT Renamed
_ -> ValT Renamed -> ValT Renamed -> TypeAppError
DoesNotUnify ValT Renamed
topLevelExpected ValT Renamed
topLevelActual
    TypeAppError
err -> TypeAppError
err

fixUp :: ValT Renamed -> UnifyM (ValT Renamed)
fixUp :: ValT Renamed -> UnifyM (ValT Renamed)
fixUp = \case
  -- We have a result that's effectively `forall a . a` but not an error
  Abstraction (Unifiable Index "tyvar"
index) -> TypeAppError -> UnifyM (ValT Renamed)
forall a. TypeAppError -> UnifyM a
forall e (m :: Type -> Type) a. MonadError e m => e -> m a
throwError (TypeAppError -> UnifyM (ValT Renamed))
-> (Index "tyvar" -> TypeAppError)
-> Index "tyvar"
-> UnifyM (ValT Renamed)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Index "tyvar" -> TypeAppError
LeakingUnifiable (Index "tyvar" -> UnifyM (ValT Renamed))
-> Index "tyvar" -> UnifyM (ValT Renamed)
forall a b. (a -> b) -> a -> b
$ Index "tyvar"
index
  -- We're doing the equivalent of failing the `ST` trick
  Abstraction (Wildcard Word64
scopeId Int
trueLevel Index "tyvar"
index) -> TypeAppError -> UnifyM (ValT Renamed)
forall a. TypeAppError -> UnifyM a
forall e (m :: Type -> Type) a. MonadError e m => e -> m a
throwError (TypeAppError -> UnifyM (ValT Renamed))
-> (Index "tyvar" -> TypeAppError)
-> Index "tyvar"
-> UnifyM (ValT Renamed)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Word64 -> Int -> Index "tyvar" -> TypeAppError
LeakingWildcard Word64
scopeId Int
trueLevel (Index "tyvar" -> UnifyM (ValT Renamed))
-> Index "tyvar" -> UnifyM (ValT Renamed)
forall a b. (a -> b) -> a -> b
$ Index "tyvar"
index
  -- We may have a result with fewer unifiables than we started with
  -- This can be a problem, as we might be referring to unifiables that don't
  -- exist anymore
  ThunkT (CompT Count "tyvar"
_ (CompTBody NonEmptyVector (ValT Renamed)
xs)) -> do
    -- Figure out how many variables the thunk has to introduce now
    let remainingUnifiables :: Set (Index "tyvar")
remainingUnifiables = (Set (Index "tyvar") -> ValT Renamed -> Set (Index "tyvar"))
-> Set (Index "tyvar")
-> NonEmptyVector (ValT Renamed)
-> Set (Index "tyvar")
forall a b. (a -> b -> a) -> a -> NonEmptyVector b -> a
NonEmpty.foldl' (\Set (Index "tyvar")
acc ValT Renamed
t -> Set (Index "tyvar")
acc Set (Index "tyvar") -> Set (Index "tyvar") -> Set (Index "tyvar")
forall a. Semigroup a => a -> a -> a
<> ValT Renamed -> Set (Index "tyvar")
collectUnifiables ValT Renamed
t) Set (Index "tyvar")
forall a. Set a
Set.empty NonEmptyVector (ValT Renamed)
xs
    let requiredIntroductions :: Int
requiredIntroductions = Set (Index "tyvar") -> Int
forall a. Set a -> Int
Set.size Set (Index "tyvar")
remainingUnifiables
    -- We know that the size of a set can't be negative, but GHC doesn't.
    let asCount :: Count "tyvar"
asCount = Maybe (Count "tyvar") -> Count "tyvar"
forall a. HasCallStack => Maybe a -> a
fromJust (Maybe (Count "tyvar") -> Count "tyvar")
-> (Int -> Maybe (Count "tyvar")) -> Int -> Count "tyvar"
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Optic' A_Prism NoIx Int (Count "tyvar")
-> Int -> Maybe (Count "tyvar")
forall k (is :: IxList) s a.
Is k An_AffineFold =>
Optic' k is s a -> s -> Maybe a
preview Optic' A_Prism NoIx Int (Count "tyvar")
forall (ofWhat :: Symbol). Prism' Int (Count ofWhat)
intCount (Int -> Count "tyvar") -> Int -> Count "tyvar"
forall a b. (a -> b) -> a -> b
$ Int
requiredIntroductions
    -- Make enough indexes for us to use in one go
    let indexesToUse :: [Index "tyvar"]
indexesToUse = (Int -> Maybe (Index "tyvar")) -> [Int] -> [Index "tyvar"]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe (Optic' A_Prism NoIx Int (Index "tyvar")
-> Int -> Maybe (Index "tyvar")
forall k (is :: IxList) s a.
Is k An_AffineFold =>
Optic' k is s a -> s -> Maybe a
preview Optic' A_Prism NoIx Int (Index "tyvar")
forall (ofWhat :: Symbol). Prism' Int (Index ofWhat)
intIndex) [Int
0, Int
1 .. Int
requiredIntroductions Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1]
    -- Construct a mapping between old, possibly non-contiguous, unifiables and
    -- our new ones
    let renames :: [(Index "tyvar", ValT Renamed)]
renames =
          (Index "tyvar" -> Index "tyvar" -> (Index "tyvar", ValT Renamed))
-> [Index "tyvar"]
-> [Index "tyvar"]
-> [(Index "tyvar", ValT Renamed)]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith
            (\Index "tyvar"
i Index "tyvar"
replacement -> (Index "tyvar"
i, Renamed -> ValT Renamed
forall a. a -> ValT a
Abstraction (Renamed -> ValT Renamed)
-> (Index "tyvar" -> Renamed) -> Index "tyvar" -> ValT Renamed
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Index "tyvar" -> Renamed
Unifiable (Index "tyvar" -> ValT Renamed) -> Index "tyvar" -> ValT Renamed
forall a b. (a -> b) -> a -> b
$ Index "tyvar"
replacement))
            (Set (Index "tyvar") -> [Index "tyvar"]
forall a. Set a -> [a]
Set.toList Set (Index "tyvar")
remainingUnifiables)
            [Index "tyvar"]
indexesToUse
    let fixed :: NonEmptyVector (ValT Renamed)
fixed = (ValT Renamed -> ValT Renamed)
-> NonEmptyVector (ValT Renamed) -> NonEmptyVector (ValT Renamed)
forall a b. (a -> b) -> NonEmptyVector a -> NonEmptyVector b
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap (\ValT Renamed
t -> (ValT Renamed -> (Index "tyvar", ValT Renamed) -> ValT Renamed)
-> ValT Renamed -> [(Index "tyvar", ValT Renamed)] -> ValT Renamed
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: Type -> Type) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' (\ValT Renamed
acc (Index "tyvar"
i, ValT Renamed
r) -> Index "tyvar" -> ValT Renamed -> ValT Renamed -> ValT Renamed
substitute Index "tyvar"
i ValT Renamed
r ValT Renamed
acc) ValT Renamed
t [(Index "tyvar", ValT Renamed)]
renames) NonEmptyVector (ValT Renamed)
xs
    ValT Renamed -> UnifyM (ValT Renamed)
forall a. a -> UnifyM a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (ValT Renamed -> UnifyM (ValT Renamed))
-> (NonEmptyVector (ValT Renamed) -> ValT Renamed)
-> NonEmptyVector (ValT Renamed)
-> UnifyM (ValT Renamed)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CompT Renamed -> ValT Renamed
forall a. CompT a -> ValT a
ThunkT (CompT Renamed -> ValT Renamed)
-> (NonEmptyVector (ValT Renamed) -> CompT Renamed)
-> NonEmptyVector (ValT Renamed)
-> ValT Renamed
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Count "tyvar" -> CompTBody Renamed -> CompT Renamed
forall a. Count "tyvar" -> CompTBody a -> CompT a
CompT Count "tyvar"
asCount (CompTBody Renamed -> CompT Renamed)
-> (NonEmptyVector (ValT Renamed) -> CompTBody Renamed)
-> NonEmptyVector (ValT Renamed)
-> CompT Renamed
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NonEmptyVector (ValT Renamed) -> CompTBody Renamed
forall a. NonEmptyVector (ValT a) -> CompTBody a
CompTBody (NonEmptyVector (ValT Renamed) -> UnifyM (ValT Renamed))
-> NonEmptyVector (ValT Renamed) -> UnifyM (ValT Renamed)
forall a b. (a -> b) -> a -> b
$ NonEmptyVector (ValT Renamed)
fixed
  ValT Renamed
t -> ValT Renamed -> UnifyM (ValT Renamed)
forall a. a -> UnifyM a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure ValT Renamed
t

collectUnifiables :: ValT Renamed -> Set (Index "tyvar")
collectUnifiables :: ValT Renamed -> Set (Index "tyvar")
collectUnifiables = \case
  Abstraction Renamed
t -> case Renamed
t of
    Unifiable Index "tyvar"
index -> Index "tyvar" -> Set (Index "tyvar")
forall a. a -> Set a
Set.singleton Index "tyvar"
index
    Renamed
_ -> Set (Index "tyvar")
forall a. Set a
Set.empty
  BuiltinFlat BuiltinFlatT
_ -> Set (Index "tyvar")
forall a. Set a
Set.empty
  ThunkT (CompT Count "tyvar"
_ (CompTBody NonEmptyVector (ValT Renamed)
xs)) -> (Set (Index "tyvar") -> ValT Renamed -> Set (Index "tyvar"))
-> Set (Index "tyvar")
-> NonEmptyVector (ValT Renamed)
-> Set (Index "tyvar")
forall a b. (a -> b -> a) -> a -> NonEmptyVector b -> a
NonEmpty.foldl' (\Set (Index "tyvar")
acc ValT Renamed
t -> Set (Index "tyvar")
acc Set (Index "tyvar") -> Set (Index "tyvar") -> Set (Index "tyvar")
forall a. Semigroup a => a -> a -> a
<> ValT Renamed -> Set (Index "tyvar")
collectUnifiables ValT Renamed
t) Set (Index "tyvar")
forall a. Set a
Set.empty NonEmptyVector (ValT Renamed)
xs
  Datatype TyName
_ Vector (ValT Renamed)
args -> (Set (Index "tyvar") -> ValT Renamed -> Set (Index "tyvar"))
-> Set (Index "tyvar")
-> Vector (ValT Renamed)
-> Set (Index "tyvar")
forall a b. (a -> b -> a) -> a -> Vector b -> a
Vector.foldl' (\Set (Index "tyvar")
acc ValT Renamed
t -> Set (Index "tyvar")
acc Set (Index "tyvar") -> Set (Index "tyvar") -> Set (Index "tyvar")
forall a. Semigroup a => a -> a -> a
<> ValT Renamed -> Set (Index "tyvar")
collectUnifiables ValT Renamed
t) Set (Index "tyvar")
forall a. Set a
Set.empty Vector (ValT Renamed)
args

unify ::
  ValT Renamed ->
  ValT Renamed ->
  UnifyM (Map (Index "tyvar") (ValT Renamed))
unify :: ValT Renamed
-> ValT Renamed -> UnifyM (Map (Index "tyvar") (ValT Renamed))
unify ValT Renamed
expected ValT Renamed
actual =
  UnifyM (Map (Index "tyvar") (ValT Renamed))
-> (TypeAppError -> UnifyM (Map (Index "tyvar") (ValT Renamed)))
-> UnifyM (Map (Index "tyvar") (ValT Renamed))
forall a. UnifyM a -> (TypeAppError -> UnifyM a) -> UnifyM a
forall e (m :: Type -> Type) a.
MonadError e m =>
m a -> (e -> m a) -> m a
catchError
    ( case ValT Renamed
expected of
        Abstraction Renamed
t1 -> case Renamed
t1 of
          -- Unifiables unify with everything, and require a substitutional rewrite.
          Unifiable Index "tyvar"
index1 -> Map (Index "tyvar") (ValT Renamed)
-> UnifyM (Map (Index "tyvar") (ValT Renamed))
forall a. a -> UnifyM a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (Map (Index "tyvar") (ValT Renamed)
 -> UnifyM (Map (Index "tyvar") (ValT Renamed)))
-> (ValT Renamed -> Map (Index "tyvar") (ValT Renamed))
-> ValT Renamed
-> UnifyM (Map (Index "tyvar") (ValT Renamed))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Index "tyvar" -> ValT Renamed -> Map (Index "tyvar") (ValT Renamed)
forall k a. k -> a -> Map k a
Map.singleton Index "tyvar"
index1 (ValT Renamed -> UnifyM (Map (Index "tyvar") (ValT Renamed)))
-> ValT Renamed -> UnifyM (Map (Index "tyvar") (ValT Renamed))
forall a b. (a -> b) -> a -> b
$ ValT Renamed
actual
          Rigid Int
level1 Index "tyvar"
index1 -> Int -> Index "tyvar" -> UnifyM (Map (Index "tyvar") (ValT Renamed))
expectRigid Int
level1 Index "tyvar"
index1
          Wildcard Word64
scopeId1 Int
_ Index "tyvar"
index1 -> Word64
-> Index "tyvar" -> UnifyM (Map (Index "tyvar") (ValT Renamed))
expectWildcard Word64
scopeId1 Index "tyvar"
index1
        ThunkT CompT Renamed
t1 -> CompT Renamed -> UnifyM (Map (Index "tyvar") (ValT Renamed))
expectThunk CompT Renamed
t1
        BuiltinFlat BuiltinFlatT
t1 -> BuiltinFlatT -> UnifyM (Map (Index "tyvar") (ValT Renamed))
expectFlatBuiltin BuiltinFlatT
t1
        Datatype TyName
tn Vector (ValT Renamed)
xs -> TyName
-> Vector (ValT Renamed)
-> UnifyM (Map (Index "tyvar") (ValT Renamed))
expectDatatype TyName
tn Vector (ValT Renamed)
xs
    )
    (ValT Renamed
-> ValT Renamed
-> TypeAppError
-> UnifyM (Map (Index "tyvar") (ValT Renamed))
forall a. ValT Renamed -> ValT Renamed -> TypeAppError -> UnifyM a
promoteUnificationError ValT Renamed
expected ValT Renamed
actual)
  where
    unificationError :: forall (a :: Type). UnifyM a
    unificationError :: forall a. UnifyM a
unificationError = TypeAppError -> UnifyM a
forall a. TypeAppError -> UnifyM a
forall e (m :: Type -> Type) a. MonadError e m => e -> m a
throwError (TypeAppError -> UnifyM a)
-> (ValT Renamed -> TypeAppError) -> ValT Renamed -> UnifyM a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ValT Renamed -> ValT Renamed -> TypeAppError
DoesNotUnify ValT Renamed
expected (ValT Renamed -> UnifyM a) -> ValT Renamed -> UnifyM a
forall a b. (a -> b) -> a -> b
$ ValT Renamed
actual
    noSubUnify :: forall (k :: Type) (a :: Type). UnifyM (Map k a)
    noSubUnify :: forall k a. UnifyM (Map k a)
noSubUnify = Map k a -> UnifyM (Map k a)
forall a. a -> UnifyM a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure Map k a
forall k a. Map k a
Map.empty
    expectRigid ::
      Int -> Index "tyvar" -> UnifyM (Map (Index "tyvar") (ValT Renamed))
    -- Rigids behave identically to concrete types: they can unify with
    -- themselves, or any other abstraction, but nothing else. No substitutional
    -- rewrites are needed.
    expectRigid :: Int -> Index "tyvar" -> UnifyM (Map (Index "tyvar") (ValT Renamed))
expectRigid Int
level1 Index "tyvar"
index1 = case ValT Renamed
actual of
      Abstraction (Rigid Int
level2 Index "tyvar"
index2) ->
        if Int
level1 Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
level2 Bool -> Bool -> Bool
&& Index "tyvar"
index1 Index "tyvar" -> Index "tyvar" -> Bool
forall a. Eq a => a -> a -> Bool
== Index "tyvar"
index2
          then UnifyM (Map (Index "tyvar") (ValT Renamed))
forall k a. UnifyM (Map k a)
noSubUnify
          else UnifyM (Map (Index "tyvar") (ValT Renamed))
forall a. UnifyM a
unificationError
      Abstraction Renamed
_ -> UnifyM (Map (Index "tyvar") (ValT Renamed))
forall k a. UnifyM (Map k a)
noSubUnify
      ValT Renamed
_ -> UnifyM (Map (Index "tyvar") (ValT Renamed))
forall a. UnifyM a
unificationError
    expectWildcard ::
      Word64 -> Index "tyvar" -> UnifyM (Map (Index "tyvar") (ValT Renamed))
    -- Wildcards can unify with unifiables, as well as themselves, but nothing
    -- else. No substitutional rewrites are needed.
    expectWildcard :: Word64
-> Index "tyvar" -> UnifyM (Map (Index "tyvar") (ValT Renamed))
expectWildcard Word64
scopeId1 Index "tyvar"
index1 = case ValT Renamed
actual of
      Abstraction (Unifiable Index "tyvar"
_) -> UnifyM (Map (Index "tyvar") (ValT Renamed))
forall k a. UnifyM (Map k a)
noSubUnify
      Abstraction (Wildcard Word64
scopeId2 Int
_ Index "tyvar"
index2) ->
        if Word64
scopeId1 Word64 -> Word64 -> Bool
forall a. Eq a => a -> a -> Bool
/= Word64
scopeId2 Bool -> Bool -> Bool
|| Index "tyvar"
index1 Index "tyvar" -> Index "tyvar" -> Bool
forall a. Eq a => a -> a -> Bool
== Index "tyvar"
index2
          then UnifyM (Map (Index "tyvar") (ValT Renamed))
forall k a. UnifyM (Map k a)
noSubUnify
          else UnifyM (Map (Index "tyvar") (ValT Renamed))
forall a. UnifyM a
unificationError
      ValT Renamed
_ -> UnifyM (Map (Index "tyvar") (ValT Renamed))
forall a. UnifyM a
unificationError
    expectThunk :: CompT Renamed -> UnifyM (Map (Index "tyvar") (ValT Renamed))
    -- Thunks unify unconditionally with wildcards or unifiables. They unify
    -- conditionally with other thunks, provided that we can unify each argument
    -- with its counterpart in the same position, as well as their result types,
    -- without conflicts.
    expectThunk :: CompT Renamed -> UnifyM (Map (Index "tyvar") (ValT Renamed))
expectThunk (CompT Count "tyvar"
_ (CompTBody NonEmptyVector (ValT Renamed)
t1)) = case ValT Renamed
actual of
      Abstraction (Rigid Int
_ Index "tyvar"
_) -> UnifyM (Map (Index "tyvar") (ValT Renamed))
forall a. UnifyM a
unificationError
      Abstraction Renamed
_ -> UnifyM (Map (Index "tyvar") (ValT Renamed))
forall k a. UnifyM (Map k a)
noSubUnify
      ThunkT (CompT Count "tyvar"
_ (CompTBody NonEmptyVector (ValT Renamed)
t2)) -> do
        Bool -> UnifyM () -> UnifyM ()
forall (f :: Type -> Type). Applicative f => Bool -> f () -> f ()
unless ((NonEmptyVector (ValT Renamed) -> Int)
-> NonEmptyVector (ValT Renamed)
-> NonEmptyVector (ValT Renamed)
-> Ordering
forall a b. Ord a => (b -> a) -> b -> b -> Ordering
comparing NonEmptyVector (ValT Renamed) -> Int
forall a. NonEmptyVector a -> Int
NonEmpty.length NonEmptyVector (ValT Renamed)
t1 NonEmptyVector (ValT Renamed)
t2 Ordering -> Ordering -> Bool
forall a. Eq a => a -> a -> Bool
== Ordering
EQ) UnifyM ()
forall a. UnifyM a
unificationError
        UnifyM (Map (Index "tyvar") (ValT Renamed))
-> (TypeAppError -> UnifyM (Map (Index "tyvar") (ValT Renamed)))
-> UnifyM (Map (Index "tyvar") (ValT Renamed))
forall a. UnifyM a -> (TypeAppError -> UnifyM a) -> UnifyM a
forall e (m :: Type -> Type) a.
MonadError e m =>
m a -> (e -> m a) -> m a
catchError
          ((Map (Index "tyvar") (ValT Renamed)
 -> (ValT Renamed, ValT Renamed)
 -> UnifyM (Map (Index "tyvar") (ValT Renamed)))
-> Map (Index "tyvar") (ValT Renamed)
-> NonEmptyVector (ValT Renamed, ValT Renamed)
-> UnifyM (Map (Index "tyvar") (ValT Renamed))
forall (t :: Type -> Type) (m :: Type -> Type) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM (\Map (Index "tyvar") (ValT Renamed)
acc (ValT Renamed
l, ValT Renamed
r) -> ValT Renamed
-> ValT Renamed -> UnifyM (Map (Index "tyvar") (ValT Renamed))
unify ValT Renamed
l ValT Renamed
r UnifyM (Map (Index "tyvar") (ValT Renamed))
-> (Map (Index "tyvar") (ValT Renamed)
    -> UnifyM (Map (Index "tyvar") (ValT Renamed)))
-> UnifyM (Map (Index "tyvar") (ValT Renamed))
forall a b. UnifyM a -> (a -> UnifyM b) -> UnifyM b
forall (m :: Type -> Type) a b. Monad m => m a -> (a -> m b) -> m b
>>= Map (Index "tyvar") (ValT Renamed)
-> Map (Index "tyvar") (ValT Renamed)
-> UnifyM (Map (Index "tyvar") (ValT Renamed))
reconcile Map (Index "tyvar") (ValT Renamed)
acc) Map (Index "tyvar") (ValT Renamed)
forall k a. Map k a
Map.empty (NonEmptyVector (ValT Renamed, ValT Renamed)
 -> UnifyM (Map (Index "tyvar") (ValT Renamed)))
-> (NonEmptyVector (ValT Renamed)
    -> NonEmptyVector (ValT Renamed, ValT Renamed))
-> NonEmptyVector (ValT Renamed)
-> UnifyM (Map (Index "tyvar") (ValT Renamed))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NonEmptyVector (ValT Renamed)
-> NonEmptyVector (ValT Renamed)
-> NonEmptyVector (ValT Renamed, ValT Renamed)
forall a b.
NonEmptyVector a -> NonEmptyVector b -> NonEmptyVector (a, b)
NonEmpty.zip NonEmptyVector (ValT Renamed)
t1 (NonEmptyVector (ValT Renamed)
 -> UnifyM (Map (Index "tyvar") (ValT Renamed)))
-> NonEmptyVector (ValT Renamed)
-> UnifyM (Map (Index "tyvar") (ValT Renamed))
forall a b. (a -> b) -> a -> b
$ NonEmptyVector (ValT Renamed)
t2)
          (ValT Renamed
-> ValT Renamed
-> TypeAppError
-> UnifyM (Map (Index "tyvar") (ValT Renamed))
forall a. ValT Renamed -> ValT Renamed -> TypeAppError -> UnifyM a
promoteUnificationError ValT Renamed
expected ValT Renamed
actual)
      ValT Renamed
_ -> UnifyM (Map (Index "tyvar") (ValT Renamed))
forall a. UnifyM a
unificationError
    expectFlatBuiltin :: BuiltinFlatT -> UnifyM (Map (Index "tyvar") (ValT Renamed))
    -- 'Flat' builtins are always concrete. They can unify with themselves,
    -- unifiables or wildcards, but nothing else. No substitutional rewrites are
    -- needed.
    expectFlatBuiltin :: BuiltinFlatT -> UnifyM (Map (Index "tyvar") (ValT Renamed))
expectFlatBuiltin BuiltinFlatT
t1 = case ValT Renamed
actual of
      Abstraction (Rigid Int
_ Index "tyvar"
_) -> UnifyM (Map (Index "tyvar") (ValT Renamed))
forall a. UnifyM a
unificationError
      Abstraction Renamed
_ -> UnifyM (Map (Index "tyvar") (ValT Renamed))
forall k a. UnifyM (Map k a)
noSubUnify
      BuiltinFlat BuiltinFlatT
t2 ->
        if BuiltinFlatT
t1 BuiltinFlatT -> BuiltinFlatT -> Bool
forall a. Eq a => a -> a -> Bool
== BuiltinFlatT
t2
          then UnifyM (Map (Index "tyvar") (ValT Renamed))
forall k a. UnifyM (Map k a)
noSubUnify
          else UnifyM (Map (Index "tyvar") (ValT Renamed))
forall a. UnifyM a
unificationError
      ValT Renamed
_ -> UnifyM (Map (Index "tyvar") (ValT Renamed))
forall a. UnifyM a
unificationError
    expectDatatype :: TyName -> Vector (ValT Renamed) -> UnifyM (Map (Index "tyvar") (ValT Renamed))
    -- Datatypes unify with wildcards or unifiables, or other "suitable" instances of the same datatype.
    -- Suitability with other datatypes is determined by converting to BB form, then concretifying
    -- the BB form using the arguments to the actual datatype.
    -- For example, the BB form of `Maybe` is: forall a r. r -> (a -> r) -> r
    -- which, if we concretify while attempting to unify with `Maybe Int`, becomes: `forall r. r -> (Int -> r) -> r`
    expectDatatype :: TyName
-> Vector (ValT Renamed)
-> UnifyM (Map (Index "tyvar") (ValT Renamed))
expectDatatype TyName
tn Vector (ValT Renamed)
args = do
      ValT Renamed
bbForm <- TyName -> UnifyM (ValT Renamed)
lookupBBForm TyName
tn
      ValT Renamed
bbFormConcreteE <- ValT Renamed -> Vector (ValT Renamed) -> UnifyM (ValT Renamed)
concretify ValT Renamed
bbForm Vector (ValT Renamed)
args
      case ValT Renamed
actual of
        Abstraction (Rigid Int
_ Index "tyvar"
_) -> UnifyM (Map (Index "tyvar") (ValT Renamed))
forall a. UnifyM a
unificationError
        Abstraction Renamed
_ -> UnifyM (Map (Index "tyvar") (ValT Renamed))
forall k a. UnifyM (Map k a)
noSubUnify
        Datatype TyName
tn' Vector (ValT Renamed)
args'
          | TyName
tn' TyName -> TyName -> Bool
forall a. Eq a => a -> a -> Bool
/= TyName
tn -> UnifyM (Map (Index "tyvar") (ValT Renamed))
forall a. UnifyM a
unificationError
          | Bool
otherwise -> do
              ValT Renamed
bbFormConcreteA <- ValT Renamed -> Vector (ValT Renamed) -> UnifyM (ValT Renamed)
concretify ValT Renamed
bbForm Vector (ValT Renamed)
args'
              ValT Renamed
-> ValT Renamed -> UnifyM (Map (Index "tyvar") (ValT Renamed))
unify ValT Renamed
bbFormConcreteE ValT Renamed
bbFormConcreteA
        ValT Renamed
_ -> UnifyM (Map (Index "tyvar") (ValT Renamed))
forall a. UnifyM a
unificationError
    concretify :: ValT Renamed -> Vector (ValT Renamed) -> UnifyM (ValT Renamed)
    concretify :: ValT Renamed -> Vector (ValT Renamed) -> UnifyM (ValT Renamed)
concretify (ThunkT (CompT Count "tyvar"
count (CompTBody NonEmptyVector (ValT Renamed)
fn))) Vector (ValT Renamed)
args = ValT Renamed -> UnifyM (ValT Renamed)
fixUp (ValT Renamed -> UnifyM (ValT Renamed))
-> ValT Renamed -> UnifyM (ValT Renamed)
forall a b. (a -> b) -> a -> b
$ CompT Renamed -> ValT Renamed
forall a. CompT a -> ValT a
ThunkT (Count "tyvar" -> CompTBody Renamed -> CompT Renamed
forall a. Count "tyvar" -> CompTBody a -> CompT a
CompT Count "tyvar"
count (NonEmptyVector (ValT Renamed) -> CompTBody Renamed
forall a. NonEmptyVector (ValT a) -> CompTBody a
CompTBody NonEmptyVector (ValT Renamed)
newFn))
      where
        indexedArgs :: [(Index "tyvar", ValT Renamed)]
        indexedArgs :: [(Index "tyvar", ValT Renamed)]
indexedArgs = Vector (Index "tyvar", ValT Renamed)
-> [(Index "tyvar", ValT Renamed)]
forall a. Vector a -> [a]
Vector.toList (Vector (Index "tyvar", ValT Renamed)
 -> [(Index "tyvar", ValT Renamed)])
-> Vector (Index "tyvar", ValT Renamed)
-> [(Index "tyvar", ValT Renamed)]
forall a b. (a -> b) -> a -> b
$ (Int -> ValT Renamed -> (Index "tyvar", ValT Renamed))
-> Vector (ValT Renamed) -> Vector (Index "tyvar", ValT Renamed)
forall a b. (Int -> a -> b) -> Vector a -> Vector b
Vector.imap (\Int
i ValT Renamed
x -> (Maybe (Index "tyvar") -> Index "tyvar"
forall a. HasCallStack => Maybe a -> a
fromJust (Maybe (Index "tyvar") -> Index "tyvar")
-> (Int -> Maybe (Index "tyvar")) -> Int -> Index "tyvar"
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Optic' A_Prism NoIx Int (Index "tyvar")
-> Int -> Maybe (Index "tyvar")
forall k (is :: IxList) s a.
Is k An_AffineFold =>
Optic' k is s a -> s -> Maybe a
preview Optic' A_Prism NoIx Int (Index "tyvar")
forall (ofWhat :: Symbol). Prism' Int (Index ofWhat)
intIndex (Int -> Index "tyvar") -> Int -> Index "tyvar"
forall a b. (a -> b) -> a -> b
$ Int
i, ValT Renamed
x)) Vector (ValT Renamed)
args
        newFn :: NonEmptyVector (ValT Renamed)
        newFn :: NonEmptyVector (ValT Renamed)
newFn = [(Index "tyvar", ValT Renamed)] -> ValT Renamed -> ValT Renamed
go [(Index "tyvar", ValT Renamed)]
indexedArgs (ValT Renamed -> ValT Renamed)
-> NonEmptyVector (ValT Renamed) -> NonEmptyVector (ValT Renamed)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> NonEmptyVector (ValT Renamed)
fn
        go :: [(Index "tyvar", ValT Renamed)] -> ValT Renamed -> ValT Renamed
        go :: [(Index "tyvar", ValT Renamed)] -> ValT Renamed -> ValT Renamed
go [(Index "tyvar", ValT Renamed)]
subs ValT Renamed
arg = (ValT Renamed -> (Index "tyvar", ValT Renamed) -> ValT Renamed)
-> ValT Renamed -> [(Index "tyvar", ValT Renamed)] -> ValT Renamed
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: Type -> Type) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' (\ValT Renamed
val (Index "tyvar"
i, ValT Renamed
concrete) -> Index "tyvar" -> ValT Renamed -> ValT Renamed -> ValT Renamed
substitute Index "tyvar"
i ValT Renamed
concrete ValT Renamed
val) ValT Renamed
arg [(Index "tyvar", ValT Renamed)]
subs
    concretify ValT Renamed
_ Vector (ValT Renamed)
_ = TypeAppError -> UnifyM (ValT Renamed)
forall a. TypeAppError -> UnifyM a
forall e (m :: Type -> Type) a. MonadError e m => e -> m a
throwError (TypeAppError -> UnifyM (ValT Renamed))
-> TypeAppError -> UnifyM (ValT Renamed)
forall a b. (a -> b) -> a -> b
$ Text -> TypeAppError
ImpossibleHappened Text
"bbForm is not a thunk"
    reconcile ::
      Map (Index "tyvar") (ValT Renamed) ->
      Map (Index "tyvar") (ValT Renamed) ->
      UnifyM (Map (Index "tyvar") (ValT Renamed))
    -- Note (Koz, 14/04/2025): This utter soup means the following:
    --
    -- - If the old map and the new map don't have any overlapping assignments,
    --   just union them.
    -- - Otherwise, for any assignment to a unifiable that is present in both
    --   maps, ensure they assign to the same thing; if they do, it's fine,
    --   otherwise we have a problem.
    reconcile :: Map (Index "tyvar") (ValT Renamed)
-> Map (Index "tyvar") (ValT Renamed)
-> UnifyM (Map (Index "tyvar") (ValT Renamed))
reconcile =
      WhenMissing UnifyM (Index "tyvar") (ValT Renamed) (ValT Renamed)
-> WhenMissing UnifyM (Index "tyvar") (ValT Renamed) (ValT Renamed)
-> WhenMatched
     UnifyM (Index "tyvar") (ValT Renamed) (ValT Renamed) (ValT Renamed)
-> Map (Index "tyvar") (ValT Renamed)
-> Map (Index "tyvar") (ValT Renamed)
-> UnifyM (Map (Index "tyvar") (ValT Renamed))
forall (f :: Type -> Type) k a c b.
(Applicative f, Ord k) =>
WhenMissing f k a c
-> WhenMissing f k b c
-> WhenMatched f k a b c
-> Map k a
-> Map k b
-> f (Map k c)
Merge.mergeA
        WhenMissing UnifyM (Index "tyvar") (ValT Renamed) (ValT Renamed)
forall (f :: Type -> Type) k x.
Applicative f =>
WhenMissing f k x x
Merge.preserveMissing
        WhenMissing UnifyM (Index "tyvar") (ValT Renamed) (ValT Renamed)
forall (f :: Type -> Type) k x.
Applicative f =>
WhenMissing f k x x
Merge.preserveMissing
        ((Index "tyvar"
 -> ValT Renamed -> ValT Renamed -> UnifyM (ValT Renamed))
-> WhenMatched
     UnifyM (Index "tyvar") (ValT Renamed) (ValT Renamed) (ValT Renamed)
forall (f :: Type -> Type) k x y z.
Applicative f =>
(k -> x -> y -> f z) -> WhenMatched f k x y z
Merge.zipWithAMatched Index "tyvar"
-> ValT Renamed -> ValT Renamed -> UnifyM (ValT Renamed)
combineBindings)
    combineBindings :: Index "tyvar" -> ValT Renamed -> ValT Renamed -> UnifyM (ValT Renamed)
    combineBindings :: Index "tyvar"
-> ValT Renamed -> ValT Renamed -> UnifyM (ValT Renamed)
combineBindings Index "tyvar"
_ ValT Renamed
old ValT Renamed
new =
      if ValT Renamed
old ValT Renamed -> ValT Renamed -> Bool
forall a. Eq a => a -> a -> Bool
== ValT Renamed
new
        then ValT Renamed -> UnifyM (ValT Renamed)
forall a. a -> UnifyM a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure ValT Renamed
old
        else case ValT Renamed
old of
          Abstraction (Unifiable Index "tyvar"
_) -> ValT Renamed -> UnifyM (ValT Renamed)
forall a. a -> UnifyM a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure ValT Renamed
new
          ValT Renamed
_ -> case ValT Renamed
new of
            Abstraction (Unifiable Index "tyvar"
_) -> ValT Renamed -> UnifyM (ValT Renamed)
forall a. a -> UnifyM a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure ValT Renamed
old
            ValT Renamed
_ -> UnifyM (ValT Renamed)
forall a. UnifyM a
unificationError