Unify.hs

{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE OverloadedStrings #-}

-- |
-- SPDX-License-Identifier: BSD-3-Clause
-- Description: This module defines an effect signature for
-- computations that support doing unification.  The intention is for
-- code needing unification to use the operations defined in this
-- module, and then import 'Swarm.Effect.Unify.Fast' to dispatch the
-- 'Unification' effects.
module Swarm.Effect.Unify where

import Control.Algebra
import Data.Kind (Type)
import Data.Set (Set)
import Prettyprinter
import Swarm.Language.Types hiding (Type)
import Swarm.Pretty (PrettyPrec (..), ppr, reportBug)

-- | Data type representing available unification operations.
data Unification (m :: Type -> Type) k where
  Unify :: UType -> UType -> Unification m (Either UnificationError UType)
  ApplyBindings :: UType -> Unification m UType
  FreshIntVar :: Unification m IntVar
  FreeUVars :: UType -> Unification m (Set IntVar)

-- | Unify two types, returning a type equal to both, or a 'UnificationError' if
--   the types definitely do not unify.
(=:=) :: Has Unification sig m => UType -> UType -> m (Either UnificationError UType)
t1 =:= t2 = send (Unify t1 t2)

-- | Substitute for all the unification variables that are currently
--   bound.  It is guaranteed that any unification variables remaining
--   in the result are not currently bound, /i.e./ we have learned no
--   information about them.
applyBindings :: Has Unification sig m => UType -> m UType
applyBindings = send . ApplyBindings

-- | Compute the set of free unification variables of a type (after
--   substituting away any which are already bound).
freeUVars :: Has Unification sig m => UType -> m (Set IntVar)
freeUVars = send . FreeUVars

-- | Generate a fresh unification variable.
freshIntVar :: Has Unification sig m => m IntVar
freshIntVar = send FreshIntVar

-- | An error that occurred while running the unifier.
data UnificationError where
  -- | Occurs check failure, i.e. the solution to some unification
  --   equations was an infinite term.
  Infinite :: IntVar -> UType -> UnificationError
  -- | Mismatch error between the given terms.
  UnifyErr :: TypeF UType -> TypeF UType -> UnificationError
  -- | Encountered an undefined/unknown type constructor.
  UndefinedUserType :: UType -> UnificationError
  -- | Encountered an unexpanded recursive type in unifyF.  This
  --   should never happen.
  UnexpandedRecTy :: TypeF UType -> UnificationError
  deriving (Show)

instance PrettyPrec UnificationError where
  prettyPrec _ = \case
    Infinite x uty ->
      vsep
        [ "Encountered infinite type" <+> ppr x <+> "=" <+> ppr uty <> "."
        , "Swarm will not infer recursive types; if you want a recursive type, add an explicit type annotation."
        ]
    UnifyErr ty1 ty2 ->
      "Can't unify" <+> ppr ty1 <+> "and" <+> ppr ty2
    UndefinedUserType ty ->
      "Undefined user type" <+> ppr ty
    UnexpandedRecTy ty ->
      vsep
        [ "Unexpanded recursive type" <+> ppr ty <+> "encountered in unifyF."
        , reportBug
        ]