{- |
Module      : Language.Egison.Type.Unify
Licence     : MIT

This module provides type unification for the Egison type system.
-}

module Language.Egison.Type.Unify
  ( unify
  , unifyStrict
  , unifyStrictWithConstraints
  , unifyWithTopLevel
  , unifyWithConstraints
  , unifyMany
  , UnifyError(..)
  ) where

import qualified Data.Set                    as Set

import           Language.Egison.Type.Subst  (Subst, applySubst, composeSubst,
                                              emptySubst, singletonSubst, applySubstConstraint)
import           Language.Egison.Type.Tensor (normalizeTensorType)
import           Language.Egison.Type.Types  (TyVar (..), Type (..), freeTyVars, normalizeInductiveTypes,
                                              Constraint(..))
import           Language.Egison.Type.Env    (ClassEnv, lookupInstances, InstanceInfo(..), emptyClassEnv)

-- | Unification errors
data UnifyError
  = OccursCheck TyVar Type        -- ^ Infinite type detected
  | TypeMismatch Type Type        -- ^ Types cannot be unified
  deriving (UnifyError -> UnifyError -> Bool
(UnifyError -> UnifyError -> Bool)
-> (UnifyError -> UnifyError -> Bool) -> Eq UnifyError
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: UnifyError -> UnifyError -> Bool
== :: UnifyError -> UnifyError -> Bool
$c/= :: UnifyError -> UnifyError -> Bool
/= :: UnifyError -> UnifyError -> Bool
Eq, Int -> UnifyError -> ShowS
[UnifyError] -> ShowS
UnifyError -> String
(Int -> UnifyError -> ShowS)
-> (UnifyError -> String)
-> ([UnifyError] -> ShowS)
-> Show UnifyError
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> UnifyError -> ShowS
showsPrec :: Int -> UnifyError -> ShowS
$cshow :: UnifyError -> String
show :: UnifyError -> String
$cshowList :: [UnifyError] -> ShowS
showList :: [UnifyError] -> ShowS
Show)

-- | Unify two types, returning a substitution if successful
-- This is a wrapper around unifyWithConstraints with empty constraints
-- Discards the flag since it's not needed in basic unification
unify :: Type -> Type -> Either UnifyError Subst
unify :: Type -> Type -> Either UnifyError Subst
unify Type
t1 Type
t2 = ((Subst, Bool) -> Subst)
-> Either UnifyError (Subst, Bool) -> Either UnifyError Subst
forall a b. (a -> b) -> Either UnifyError a -> Either UnifyError b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Subst, Bool) -> Subst
forall a b. (a, b) -> a
fst (ClassEnv
-> [Constraint] -> Type -> Type -> Either UnifyError (Subst, Bool)
unifyWithConstraints ClassEnv
emptyClassEnv [] Type
t1 Type
t2)


-- | Strict unification that does NOT allow Tensor a to unify with a
-- This is a wrapper around unifyStrictWithConstraints with empty constraints
-- This is used for checking type class instances in TensorMapInsertion
-- to ensure that Tensor types are properly distinguished from scalar types
unifyStrict :: Type -> Type -> Either UnifyError Subst
unifyStrict :: Type -> Type -> Either UnifyError Subst
unifyStrict = ClassEnv -> [Constraint] -> Type -> Type -> Either UnifyError Subst
unifyStrictWithConstraints ClassEnv
emptyClassEnv []


-- | Strict unification with type class constraints
-- This is like unifyStrict but considers type class constraints when unifying type variables.
-- IMPORTANT: This does NOT allow Tensor a to unify with a (strict unification).
-- When unifying a constrained type variable with Tensor type, it checks if Tensor
-- has instances for all the constraints.
unifyStrictWithConstraints :: ClassEnv -> [Constraint] -> Type -> Type -> Either UnifyError Subst
unifyStrictWithConstraints :: ClassEnv -> [Constraint] -> Type -> Type -> Either UnifyError Subst
unifyStrictWithConstraints ClassEnv
classEnv [Constraint]
constraints Type
t1 Type
t2 =
  let t1' :: Type
t1' = Type -> Type
normalizeInductiveTypes (Type -> Type
normalizeTensorType Type
t1)
      t2' :: Type
t2' = Type -> Type
normalizeInductiveTypes (Type -> Type
normalizeTensorType Type
t2)
  in ClassEnv -> [Constraint] -> Type -> Type -> Either UnifyError Subst
unifyStrictWithConstraints' ClassEnv
classEnv [Constraint]
constraints Type
t1' Type
t2'

unifyStrictWithConstraints' :: ClassEnv -> [Constraint] -> Type -> Type -> Either UnifyError Subst
-- Same types unify trivially
unifyStrictWithConstraints' :: ClassEnv -> [Constraint] -> Type -> Type -> Either UnifyError Subst
unifyStrictWithConstraints' ClassEnv
_ [Constraint]
_ Type
TInt Type
TInt = Subst -> Either UnifyError Subst
forall a b. b -> Either a b
Right Subst
emptySubst
unifyStrictWithConstraints' ClassEnv
_ [Constraint]
_ Type
TMathExpr Type
TMathExpr = Subst -> Either UnifyError Subst
forall a b. b -> Either a b
Right Subst
emptySubst
unifyStrictWithConstraints' ClassEnv
_ [Constraint]
_ Type
TPolyExpr Type
TPolyExpr = Subst -> Either UnifyError Subst
forall a b. b -> Either a b
Right Subst
emptySubst
unifyStrictWithConstraints' ClassEnv
_ [Constraint]
_ Type
TTermExpr Type
TTermExpr = Subst -> Either UnifyError Subst
forall a b. b -> Either a b
Right Subst
emptySubst
unifyStrictWithConstraints' ClassEnv
_ [Constraint]
_ Type
TSymbolExpr Type
TSymbolExpr = Subst -> Either UnifyError Subst
forall a b. b -> Either a b
Right Subst
emptySubst
unifyStrictWithConstraints' ClassEnv
_ [Constraint]
_ Type
TIndexExpr Type
TIndexExpr = Subst -> Either UnifyError Subst
forall a b. b -> Either a b
Right Subst
emptySubst
unifyStrictWithConstraints' ClassEnv
_ [Constraint]
_ Type
TFloat Type
TFloat = Subst -> Either UnifyError Subst
forall a b. b -> Either a b
Right Subst
emptySubst
unifyStrictWithConstraints' ClassEnv
_ [Constraint]
_ Type
TBool Type
TBool = Subst -> Either UnifyError Subst
forall a b. b -> Either a b
Right Subst
emptySubst
unifyStrictWithConstraints' ClassEnv
_ [Constraint]
_ Type
TChar Type
TChar = Subst -> Either UnifyError Subst
forall a b. b -> Either a b
Right Subst
emptySubst
unifyStrictWithConstraints' ClassEnv
_ [Constraint]
_ Type
TString Type
TString = Subst -> Either UnifyError Subst
forall a b. b -> Either a b
Right Subst
emptySubst

-- Special rule: TInt and TMathExpr unify
unifyStrictWithConstraints' ClassEnv
_ [Constraint]
_ Type
TInt Type
TMathExpr = Subst -> Either UnifyError Subst
forall a b. b -> Either a b
Right Subst
emptySubst
unifyStrictWithConstraints' ClassEnv
_ [Constraint]
_ Type
TMathExpr Type
TInt = Subst -> Either UnifyError Subst
forall a b. b -> Either a b
Right Subst
emptySubst

-- Type variables - use constraint-aware strict unification
unifyStrictWithConstraints' ClassEnv
classEnv [Constraint]
constraints (TVar TyVar
v) Type
t =
  ClassEnv
-> [Constraint] -> TyVar -> Type -> Either UnifyError Subst
unifyVarStrictWithConstraints ClassEnv
classEnv [Constraint]
constraints TyVar
v Type
t
unifyStrictWithConstraints' ClassEnv
classEnv [Constraint]
constraints Type
t (TVar TyVar
v) =
  ClassEnv
-> [Constraint] -> TyVar -> Type -> Either UnifyError Subst
unifyVarStrictWithConstraints ClassEnv
classEnv [Constraint]
constraints TyVar
v Type
t

unifyStrictWithConstraints' ClassEnv
classEnv [Constraint]
constraints (TTuple [Type]
ts1) (TTuple [Type]
ts2)
  | [Type] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Type]
ts1 Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== [Type] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Type]
ts2 = ClassEnv
-> [Constraint] -> [Type] -> [Type] -> Either UnifyError Subst
unifyManyStrictWithConstraints ClassEnv
classEnv [Constraint]
constraints [Type]
ts1 [Type]
ts2
  | Bool
otherwise = UnifyError -> Either UnifyError Subst
forall a b. a -> Either a b
Left (UnifyError -> Either UnifyError Subst)
-> UnifyError -> Either UnifyError Subst
forall a b. (a -> b) -> a -> b
$ Type -> Type -> UnifyError
TypeMismatch ([Type] -> Type
TTuple [Type]
ts1) ([Type] -> Type
TTuple [Type]
ts2)

unifyStrictWithConstraints' ClassEnv
classEnv [Constraint]
constraints (TCollection Type
t1) (TCollection Type
t2) =
  ClassEnv -> [Constraint] -> Type -> Type -> Either UnifyError Subst
unifyStrictWithConstraints ClassEnv
classEnv [Constraint]
constraints Type
t1 Type
t2

-- Inductive types
unifyStrictWithConstraints' ClassEnv
classEnv [Constraint]
constraints (TInductive String
n1 [Type]
ts1) (TInductive String
n2 [Type]
ts2)
  | String
n1 String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== String
n2 Bool -> Bool -> Bool
&& [Type] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Type]
ts1 Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== [Type] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Type]
ts2 = ClassEnv
-> [Constraint] -> [Type] -> [Type] -> Either UnifyError Subst
unifyManyStrictWithConstraints ClassEnv
classEnv [Constraint]
constraints [Type]
ts1 [Type]
ts2
  | Bool
otherwise = UnifyError -> Either UnifyError Subst
forall a b. a -> Either a b
Left (UnifyError -> Either UnifyError Subst)
-> UnifyError -> Either UnifyError Subst
forall a b. (a -> b) -> a -> b
$ Type -> Type -> UnifyError
TypeMismatch (String -> [Type] -> Type
TInductive String
n1 [Type]
ts1) (String -> [Type] -> Type
TInductive String
n2 [Type]
ts2)

unifyStrictWithConstraints' ClassEnv
classEnv [Constraint]
constraints (THash Type
k1 Type
v1) (THash Type
k2 Type
v2) = do
  Subst
s1 <- ClassEnv -> [Constraint] -> Type -> Type -> Either UnifyError Subst
unifyStrictWithConstraints ClassEnv
classEnv [Constraint]
constraints Type
k1 Type
k2
  let constraints' :: [Constraint]
constraints' = (Constraint -> Constraint) -> [Constraint] -> [Constraint]
forall a b. (a -> b) -> [a] -> [b]
map (Subst -> Constraint -> Constraint
applySubstConstraint Subst
s1) [Constraint]
constraints
  Subst
s2 <- ClassEnv -> [Constraint] -> Type -> Type -> Either UnifyError Subst
unifyStrictWithConstraints ClassEnv
classEnv [Constraint]
constraints' (Subst -> Type -> Type
applySubst Subst
s1 Type
v1) (Subst -> Type -> Type
applySubst Subst
s1 Type
v2)
  Subst -> Either UnifyError Subst
forall a b. b -> Either a b
Right (Subst -> Either UnifyError Subst)
-> Subst -> Either UnifyError Subst
forall a b. (a -> b) -> a -> b
$ Subst -> Subst -> Subst
composeSubst Subst
s2 Subst
s1

unifyStrictWithConstraints' ClassEnv
classEnv [Constraint]
constraints (TMatcher Type
t1) (TMatcher Type
t2) =
  ClassEnv -> [Constraint] -> Type -> Type -> Either UnifyError Subst
unifyStrictWithConstraints ClassEnv
classEnv [Constraint]
constraints Type
t1 Type
t2

unifyStrictWithConstraints' ClassEnv
classEnv [Constraint]
constraints (TFun Type
a1 Type
r1) (TFun Type
a2 Type
r2) = do
  Subst
s1 <- ClassEnv -> [Constraint] -> Type -> Type -> Either UnifyError Subst
unifyStrictWithConstraints ClassEnv
classEnv [Constraint]
constraints Type
a1 Type
a2
  let constraints' :: [Constraint]
constraints' = (Constraint -> Constraint) -> [Constraint] -> [Constraint]
forall a b. (a -> b) -> [a] -> [b]
map (Subst -> Constraint -> Constraint
applySubstConstraint Subst
s1) [Constraint]
constraints
  Subst
s2 <- ClassEnv -> [Constraint] -> Type -> Type -> Either UnifyError Subst
unifyStrictWithConstraints ClassEnv
classEnv [Constraint]
constraints' (Subst -> Type -> Type
applySubst Subst
s1 Type
r1) (Subst -> Type -> Type
applySubst Subst
s1 Type
r2)
  Subst -> Either UnifyError Subst
forall a b. b -> Either a b
Right (Subst -> Either UnifyError Subst)
-> Subst -> Either UnifyError Subst
forall a b. (a -> b) -> a -> b
$ Subst -> Subst -> Subst
composeSubst Subst
s2 Subst
s1

unifyStrictWithConstraints' ClassEnv
classEnv [Constraint]
constraints (TIO Type
t1) (TIO Type
t2) =
  ClassEnv -> [Constraint] -> Type -> Type -> Either UnifyError Subst
unifyStrictWithConstraints ClassEnv
classEnv [Constraint]
constraints Type
t1 Type
t2

unifyStrictWithConstraints' ClassEnv
classEnv [Constraint]
constraints (TIORef Type
t1) (TIORef Type
t2) =
  ClassEnv -> [Constraint] -> Type -> Type -> Either UnifyError Subst
unifyStrictWithConstraints ClassEnv
classEnv [Constraint]
constraints Type
t1 Type
t2

unifyStrictWithConstraints' ClassEnv
_ [Constraint]
_ Type
TPort Type
TPort = Subst -> Either UnifyError Subst
forall a b. b -> Either a b
Right Subst
emptySubst

-- Tensor types - STRICT: Tensor a does NOT unify with a
unifyStrictWithConstraints' ClassEnv
classEnv [Constraint]
constraints (TTensor Type
t1) (TTensor Type
t2) =
  ClassEnv -> [Constraint] -> Type -> Type -> Either UnifyError Subst
unifyStrictWithConstraints ClassEnv
classEnv [Constraint]
constraints Type
t1 Type
t2

-- TAny unifies with anything
unifyStrictWithConstraints' ClassEnv
_ [Constraint]
_ Type
TAny Type
_ = Subst -> Either UnifyError Subst
forall a b. b -> Either a b
Right Subst
emptySubst
unifyStrictWithConstraints' ClassEnv
_ [Constraint]
_ Type
_ Type
TAny = Subst -> Either UnifyError Subst
forall a b. b -> Either a b
Right Subst
emptySubst

-- Mismatched types
unifyStrictWithConstraints' ClassEnv
_ [Constraint]
_ Type
t1 Type
t2 = UnifyError -> Either UnifyError Subst
forall a b. a -> Either a b
Left (UnifyError -> Either UnifyError Subst)
-> UnifyError -> Either UnifyError Subst
forall a b. (a -> b) -> a -> b
$ Type -> Type -> UnifyError
TypeMismatch Type
t1 Type
t2

-- | Unify a type variable with a type using strict unification with constraints
-- IMPORTANT: This is STRICT - Tensor a does NOT unify with a
unifyVarStrictWithConstraints :: ClassEnv -> [Constraint] -> TyVar -> Type -> Either UnifyError Subst
unifyVarStrictWithConstraints :: ClassEnv
-> [Constraint] -> TyVar -> Type -> Either UnifyError Subst
unifyVarStrictWithConstraints ClassEnv
classEnv [Constraint]
constraints TyVar
v Type
t
  | TyVar -> Type
TVar TyVar
v Type -> Type -> Bool
forall a. Eq a => a -> a -> Bool
== Type
t = Subst -> Either UnifyError Subst
forall a b. b -> Either a b
Right Subst
emptySubst
  | Bool
otherwise = case Type
t of
      -- Tensor type: check if the type variable's constraints allow Tensor
      TTensor Type
elemType ->
        let varConstraints :: [Constraint]
varConstraints = (Constraint -> Bool) -> [Constraint] -> [Constraint]
forall a. (a -> Bool) -> [a] -> [a]
filter (\(Constraint String
_ Type
constraintType) -> Type
constraintType Type -> Type -> Bool
forall a. Eq a => a -> a -> Bool
== TyVar -> Type
TVar TyVar
v) [Constraint]
constraints
        in if [Constraint] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Constraint]
varConstraints
           then
             -- No constraints: can bind to Tensor (with occurs check)
             if TyVar
v TyVar -> Set TyVar -> Bool
forall a. Ord a => a -> Set a -> Bool
`Set.member` Type -> Set TyVar
freeTyVars Type
t
             then UnifyError -> Either UnifyError Subst
forall a b. a -> Either a b
Left (UnifyError -> Either UnifyError Subst)
-> UnifyError -> Either UnifyError Subst
forall a b. (a -> b) -> a -> b
$ TyVar -> Type -> UnifyError
OccursCheck TyVar
v Type
t
             else Subst -> Either UnifyError Subst
forall a b. b -> Either a b
Right (Subst -> Either UnifyError Subst)
-> Subst -> Either UnifyError Subst
forall a b. (a -> b) -> a -> b
$ TyVar -> Type -> Subst
singletonSubst TyVar
v Type
t
           else
             -- Has constraints: check if Tensor has instances for ALL of them
             if (Constraint -> Bool) -> [Constraint] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (ClassEnv -> Type -> Constraint -> Bool
hasInstanceForTensorType ClassEnv
classEnv Type
elemType) [Constraint]
varConstraints
             then
               -- All constraints satisfied: can bind to Tensor
               if TyVar
v TyVar -> Set TyVar -> Bool
forall a. Ord a => a -> Set a -> Bool
`Set.member` Type -> Set TyVar
freeTyVars Type
t
               then UnifyError -> Either UnifyError Subst
forall a b. a -> Either a b
Left (UnifyError -> Either UnifyError Subst)
-> UnifyError -> Either UnifyError Subst
forall a b. (a -> b) -> a -> b
$ TyVar -> Type -> UnifyError
OccursCheck TyVar
v Type
t
               else Subst -> Either UnifyError Subst
forall a b. b -> Either a b
Right (Subst -> Either UnifyError Subst)
-> Subst -> Either UnifyError Subst
forall a b. (a -> b) -> a -> b
$ TyVar -> Type -> Subst
singletonSubst TyVar
v Type
t
             else
               -- Some constraint not satisfied by Tensor: cannot unify (strict)
               UnifyError -> Either UnifyError Subst
forall a b. a -> Either a b
Left (UnifyError -> Either UnifyError Subst)
-> UnifyError -> Either UnifyError Subst
forall a b. (a -> b) -> a -> b
$ Type -> Type -> UnifyError
TypeMismatch (TyVar -> Type
TVar TyVar
v) Type
t
      Type
_ ->
        -- Non-Tensor type: regular occurs check and bind
        if TyVar
v TyVar -> Set TyVar -> Bool
forall a. Ord a => a -> Set a -> Bool
`Set.member` Type -> Set TyVar
freeTyVars Type
t
        then UnifyError -> Either UnifyError Subst
forall a b. a -> Either a b
Left (UnifyError -> Either UnifyError Subst)
-> UnifyError -> Either UnifyError Subst
forall a b. (a -> b) -> a -> b
$ TyVar -> Type -> UnifyError
OccursCheck TyVar
v Type
t
        else Subst -> Either UnifyError Subst
forall a b. b -> Either a b
Right (Subst -> Either UnifyError Subst)
-> Subst -> Either UnifyError Subst
forall a b. (a -> b) -> a -> b
$ TyVar -> Type -> Subst
singletonSubst TyVar
v Type
t

-- | Unify multiple type pairs with strict unification and constraints
unifyManyStrictWithConstraints :: ClassEnv -> [Constraint] -> [Type] -> [Type] -> Either UnifyError Subst
unifyManyStrictWithConstraints :: ClassEnv
-> [Constraint] -> [Type] -> [Type] -> Either UnifyError Subst
unifyManyStrictWithConstraints ClassEnv
_ [Constraint]
_ [] [] = Subst -> Either UnifyError Subst
forall a b. b -> Either a b
Right Subst
emptySubst
unifyManyStrictWithConstraints ClassEnv
classEnv [Constraint]
constraints (Type
t1:[Type]
ts1) (Type
t2:[Type]
ts2) = do
  Subst
s1 <- ClassEnv -> [Constraint] -> Type -> Type -> Either UnifyError Subst
unifyStrictWithConstraints ClassEnv
classEnv [Constraint]
constraints Type
t1 Type
t2
  let constraints' :: [Constraint]
constraints' = (Constraint -> Constraint) -> [Constraint] -> [Constraint]
forall a b. (a -> b) -> [a] -> [b]
map (Subst -> Constraint -> Constraint
applySubstConstraint Subst
s1) [Constraint]
constraints
  Subst
s2 <- ClassEnv
-> [Constraint] -> [Type] -> [Type] -> Either UnifyError Subst
unifyManyStrictWithConstraints ClassEnv
classEnv [Constraint]
constraints' ((Type -> Type) -> [Type] -> [Type]
forall a b. (a -> b) -> [a] -> [b]
map (Subst -> Type -> Type
applySubst Subst
s1) [Type]
ts1) ((Type -> Type) -> [Type] -> [Type]
forall a b. (a -> b) -> [a] -> [b]
map (Subst -> Type -> Type
applySubst Subst
s1) [Type]
ts2)
  Subst -> Either UnifyError Subst
forall a b. b -> Either a b
Right (Subst -> Either UnifyError Subst)
-> Subst -> Either UnifyError Subst
forall a b. (a -> b) -> a -> b
$ Subst -> Subst -> Subst
composeSubst Subst
s2 Subst
s1
unifyManyStrictWithConstraints ClassEnv
_ [Constraint]
_ [Type]
_ [Type]
_ = UnifyError -> Either UnifyError Subst
forall a b. a -> Either a b
Left (UnifyError -> Either UnifyError Subst)
-> UnifyError -> Either UnifyError Subst
forall a b. (a -> b) -> a -> b
$ Type -> Type -> UnifyError
TypeMismatch ([Type] -> Type
TTuple []) ([Type] -> Type
TTuple [])

-- | Unify a type variable with a type
unifyVar :: TyVar -> Type -> Either UnifyError Subst
unifyVar :: TyVar -> Type -> Either UnifyError Subst
unifyVar TyVar
v Type
t
  | TyVar -> Type
TVar TyVar
v Type -> Type -> Bool
forall a. Eq a => a -> a -> Bool
== Type
t = Subst -> Either UnifyError Subst
forall a b. b -> Either a b
Right Subst
emptySubst
  | TyVar -> Type -> Bool
occursIn TyVar
v Type
t = UnifyError -> Either UnifyError Subst
forall a b. a -> Either a b
Left (UnifyError -> Either UnifyError Subst)
-> UnifyError -> Either UnifyError Subst
forall a b. (a -> b) -> a -> b
$ TyVar -> Type -> UnifyError
OccursCheck TyVar
v Type
t
  | Bool
otherwise = Subst -> Either UnifyError Subst
forall a b. b -> Either a b
Right (Subst -> Either UnifyError Subst)
-> Subst -> Either UnifyError Subst
forall a b. (a -> b) -> a -> b
$ TyVar -> Type -> Subst
singletonSubst TyVar
v Type
t

-- | Occurs check: ensure a type variable doesn't occur in a type
-- This prevents infinite types like a = [a]
occursIn :: TyVar -> Type -> Bool
occursIn :: TyVar -> Type -> Bool
occursIn TyVar
v Type
t = TyVar
v TyVar -> Set TyVar -> Bool
forall a. Ord a => a -> Set a -> Bool
`Set.member` Type -> Set TyVar
freeTyVars Type
t

-- | Unify Matcher b with (t1, t2, ...) by treating each ti as Matcher ci
-- Result: b = (c1, c2, ...) where ti unifies with Matcher ci
unifyMatcherWithTuple :: Type -> [Type] -> Either UnifyError Subst
unifyMatcherWithTuple :: Type -> [Type] -> Either UnifyError Subst
unifyMatcherWithTuple Type
b [Type]
ts = do
  -- Process each element: extract inner type or create constraint
  ([Type]
innerTypes, Subst
s1) <- [Type] -> Subst -> Either UnifyError ([Type], Subst)
unifyEachAsMatcher [Type]
ts Subst
emptySubst
  -- Now unify b with (c1, c2, ...)
  let tupleType :: Type
tupleType = [Type] -> Type
TTuple [Type]
innerTypes
  Subst
s2 <- Type -> Type -> Either UnifyError Subst
unify (Subst -> Type -> Type
applySubst Subst
s1 Type
b) Type
tupleType
  Subst -> Either UnifyError Subst
forall a b. b -> Either a b
Right (Subst -> Either UnifyError Subst)
-> Subst -> Either UnifyError Subst
forall a b. (a -> b) -> a -> b
$ Subst -> Subst -> Subst
composeSubst Subst
s2 Subst
s1
  where
    -- Unify each type in the tuple with Matcher ci, extracting ci
    unifyEachAsMatcher :: [Type] -> Subst -> Either UnifyError ([Type], Subst)
    unifyEachAsMatcher :: [Type] -> Subst -> Either UnifyError ([Type], Subst)
unifyEachAsMatcher [] Subst
s = ([Type], Subst) -> Either UnifyError ([Type], Subst)
forall a b. b -> Either a b
Right ([], Subst
s)
    unifyEachAsMatcher (Type
t:[Type]
rest) Subst
s = do
      let t' :: Type
t' = Subst -> Type -> Type
applySubst Subst
s Type
t
      (Type
innerType, Subst
s1) <- case Type
t' of
        -- If already Matcher c, extract c
        TMatcher Type
inner -> (Type, Subst) -> Either UnifyError (Type, Subst)
forall a b. b -> Either a b
Right (Type
inner, Subst
emptySubst)
        -- If type variable, unify it with Matcher (fresh variable)
        TVar TyVar
v -> do
          -- Generate a new variable name for the inner type
          let innerVar :: TyVar
innerVar = String -> TyVar
TyVar (TyVar -> String
getTyVarName TyVar
v String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"'")
              innerType :: Type
innerType = TyVar -> Type
TVar TyVar
innerVar
          Subst
s' <- Type -> Type -> Either UnifyError Subst
unify Type
t' (Type -> Type
TMatcher Type
innerType)
          (Type, Subst) -> Either UnifyError (Type, Subst)
forall a b. b -> Either a b
Right (Subst -> Type -> Type
applySubst Subst
s' Type
innerType, Subst
s')
        -- Other types cannot be unified with Matcher
        Type
_ -> UnifyError -> Either UnifyError (Type, Subst)
forall a b. a -> Either a b
Left (UnifyError -> Either UnifyError (Type, Subst))
-> UnifyError -> Either UnifyError (Type, Subst)
forall a b. (a -> b) -> a -> b
$ Type -> Type -> UnifyError
TypeMismatch (Type -> Type
TMatcher (TyVar -> Type
TVar (String -> TyVar
TyVar String
"?"))) Type
t'
      
      let s2 :: Subst
s2 = Subst -> Subst -> Subst
composeSubst Subst
s1 Subst
s
      ([Type]
restInnerTypes, Subst
s3) <- [Type] -> Subst -> Either UnifyError ([Type], Subst)
unifyEachAsMatcher [Type]
rest Subst
s2
      ([Type], Subst) -> Either UnifyError ([Type], Subst)
forall a b. b -> Either a b
Right (Subst -> Type -> Type
applySubst Subst
s3 Type
innerType Type -> [Type] -> [Type]
forall a. a -> [a] -> [a]
: [Type]
restInnerTypes, Subst
s3)
    
    getTyVarName :: TyVar -> String
    getTyVarName :: TyVar -> String
getTyVarName (TyVar String
name) = String
name

-- | Unify two types, allowing Tensor a to unify with a at top-level definitions
-- This is used only for top-level definitions with type annotations
-- According to type-tensor-simple.md: "トップレベル定義のテンソルについてのみ、Tensor a型が a型とunifyするとa型になる。"
unifyWithTopLevel :: Type -> Type -> Either UnifyError Subst
unifyWithTopLevel :: Type -> Type -> Either UnifyError Subst
unifyWithTopLevel Type
t1 Type
t2 =
  let t1' :: Type
t1' = Type -> Type
normalizeInductiveTypes (Type -> Type
normalizeTensorType Type
t1)
      t2' :: Type
t2' = Type -> Type
normalizeInductiveTypes (Type -> Type
normalizeTensorType Type
t2)
  in Type -> Type -> Either UnifyError Subst
unifyWithTopLevel' Type
t1' Type
t2'

unifyWithTopLevel' :: Type -> Type -> Either UnifyError Subst
-- Same types unify trivially
unifyWithTopLevel' :: Type -> Type -> Either UnifyError Subst
unifyWithTopLevel' Type
TInt Type
TInt = Subst -> Either UnifyError Subst
forall a b. b -> Either a b
Right Subst
emptySubst
unifyWithTopLevel' Type
TMathExpr Type
TMathExpr = Subst -> Either UnifyError Subst
forall a b. b -> Either a b
Right Subst
emptySubst
unifyWithTopLevel' Type
TPolyExpr Type
TPolyExpr = Subst -> Either UnifyError Subst
forall a b. b -> Either a b
Right Subst
emptySubst
unifyWithTopLevel' Type
TTermExpr Type
TTermExpr = Subst -> Either UnifyError Subst
forall a b. b -> Either a b
Right Subst
emptySubst
unifyWithTopLevel' Type
TSymbolExpr Type
TSymbolExpr = Subst -> Either UnifyError Subst
forall a b. b -> Either a b
Right Subst
emptySubst
unifyWithTopLevel' Type
TIndexExpr Type
TIndexExpr = Subst -> Either UnifyError Subst
forall a b. b -> Either a b
Right Subst
emptySubst
unifyWithTopLevel' Type
TFloat Type
TFloat = Subst -> Either UnifyError Subst
forall a b. b -> Either a b
Right Subst
emptySubst
unifyWithTopLevel' Type
TBool Type
TBool = Subst -> Either UnifyError Subst
forall a b. b -> Either a b
Right Subst
emptySubst
unifyWithTopLevel' Type
TChar Type
TChar = Subst -> Either UnifyError Subst
forall a b. b -> Either a b
Right Subst
emptySubst
unifyWithTopLevel' Type
TString Type
TString = Subst -> Either UnifyError Subst
forall a b. b -> Either a b
Right Subst
emptySubst

-- Special rule: TInt and TMathExpr unify to TMathExpr
unifyWithTopLevel' Type
TInt Type
TMathExpr = Subst -> Either UnifyError Subst
forall a b. b -> Either a b
Right Subst
emptySubst
unifyWithTopLevel' Type
TMathExpr Type
TInt = Subst -> Either UnifyError Subst
forall a b. b -> Either a b
Right Subst
emptySubst

-- Type variables
unifyWithTopLevel' (TVar TyVar
v) Type
t = TyVar -> Type -> Either UnifyError Subst
unifyVar TyVar
v Type
t
unifyWithTopLevel' Type
t (TVar TyVar
v) = TyVar -> Type -> Either UnifyError Subst
unifyVar TyVar
v Type
t

unifyWithTopLevel' (TTuple [Type]
ts1) (TTuple [Type]
ts2)
  | [Type] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Type]
ts1 Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== [Type] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Type]
ts2 = [Type] -> [Type] -> Either UnifyError Subst
unifyManyWithTopLevel [Type]
ts1 [Type]
ts2
  | Bool
otherwise = UnifyError -> Either UnifyError Subst
forall a b. a -> Either a b
Left (UnifyError -> Either UnifyError Subst)
-> UnifyError -> Either UnifyError Subst
forall a b. (a -> b) -> a -> b
$ Type -> Type -> UnifyError
TypeMismatch ([Type] -> Type
TTuple [Type]
ts1) ([Type] -> Type
TTuple [Type]
ts2)

unifyWithTopLevel' (TCollection Type
t1) (TCollection Type
t2) = Type -> Type -> Either UnifyError Subst
unifyWithTopLevel Type
t1 Type
t2

-- Inductive types
unifyWithTopLevel' (TInductive String
n1 [Type]
ts1) (TInductive String
n2 [Type]
ts2)
  | String
n1 String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== String
n2 Bool -> Bool -> Bool
&& [Type] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Type]
ts1 Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== [Type] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Type]
ts2 = [Type] -> [Type] -> Either UnifyError Subst
unifyManyWithTopLevel [Type]
ts1 [Type]
ts2
  | Bool
otherwise = UnifyError -> Either UnifyError Subst
forall a b. a -> Either a b
Left (UnifyError -> Either UnifyError Subst)
-> UnifyError -> Either UnifyError Subst
forall a b. (a -> b) -> a -> b
$ Type -> Type -> UnifyError
TypeMismatch (String -> [Type] -> Type
TInductive String
n1 [Type]
ts1) (String -> [Type] -> Type
TInductive String
n2 [Type]
ts2)

unifyWithTopLevel' (THash Type
k1 Type
v1) (THash Type
k2 Type
v2) = do
  Subst
s1 <- Type -> Type -> Either UnifyError Subst
unifyWithTopLevel Type
k1 Type
k2
  Subst
s2 <- Type -> Type -> Either UnifyError Subst
unifyWithTopLevel (Subst -> Type -> Type
applySubst Subst
s1 Type
v1) (Subst -> Type -> Type
applySubst Subst
s1 Type
v2)
  Subst -> Either UnifyError Subst
forall a b. b -> Either a b
Right (Subst -> Either UnifyError Subst)
-> Subst -> Either UnifyError Subst
forall a b. (a -> b) -> a -> b
$ Subst -> Subst -> Subst
composeSubst Subst
s2 Subst
s1

unifyWithTopLevel' (TMatcher Type
t1) (TMatcher Type
t2) = Type -> Type -> Either UnifyError Subst
unifyWithTopLevel Type
t1 Type
t2

unifyWithTopLevel' (TFun Type
a1 Type
r1) (TFun Type
a2 Type
r2) = do
  Subst
s1 <- Type -> Type -> Either UnifyError Subst
unifyWithTopLevel Type
a1 Type
a2
  Subst
s2 <- Type -> Type -> Either UnifyError Subst
unifyWithTopLevel (Subst -> Type -> Type
applySubst Subst
s1 Type
r1) (Subst -> Type -> Type
applySubst Subst
s1 Type
r2)
  Subst -> Either UnifyError Subst
forall a b. b -> Either a b
Right (Subst -> Either UnifyError Subst)
-> Subst -> Either UnifyError Subst
forall a b. (a -> b) -> a -> b
$ Subst -> Subst -> Subst
composeSubst Subst
s2 Subst
s1

unifyWithTopLevel' (TIO Type
t1) (TIO Type
t2) = Type -> Type -> Either UnifyError Subst
unifyWithTopLevel Type
t1 Type
t2

unifyWithTopLevel' (TIORef Type
t1) (TIORef Type
t2) = Type -> Type -> Either UnifyError Subst
unifyWithTopLevel Type
t1 Type
t2

unifyWithTopLevel' Type
TPort Type
TPort = Subst -> Either UnifyError Subst
forall a b. b -> Either a b
Right Subst
emptySubst

-- TAny unifies with anything
unifyWithTopLevel' Type
TAny Type
_ = Subst -> Either UnifyError Subst
forall a b. b -> Either a b
Right Subst
emptySubst
unifyWithTopLevel' Type
_ Type
TAny = Subst -> Either UnifyError Subst
forall a b. b -> Either a b
Right Subst
emptySubst

-- Tensor types
-- Tensor a and Tensor b unify if a and b unify
unifyWithTopLevel' (TTensor Type
t1) (TTensor Type
t2) = Type -> Type -> Either UnifyError Subst
unifyWithTopLevel Type
t1 Type
t2
-- Tensor a and a can unify as a (only at top-level definitions)
-- Tensor MathExpr can unifies with MathExpr as MathExpr
unifyWithTopLevel' (TTensor Type
t1) Type
t2 = do
  Subst
s <- Type -> Type -> Either UnifyError Subst
unifyWithTopLevel Type
t1 Type
t2
  -- Return substitution that unifies t1 with t2, result type is t2 (scalar)
  Subst -> Either UnifyError Subst
forall a b. b -> Either a b
Right Subst
s

unifyWithTopLevel' Type
t1 (TTensor Type
t2) = do
  Subst
s <- Type -> Type -> Either UnifyError Subst
unifyWithTopLevel Type
t1 Type
t2
  -- Return substitution that unifies t1 with t2, result type is t1 (scalar)
  Subst -> Either UnifyError Subst
forall a b. b -> Either a b
Right Subst
s

-- Mismatched types
unifyWithTopLevel' Type
t1 Type
t2 = UnifyError -> Either UnifyError Subst
forall a b. a -> Either a b
Left (UnifyError -> Either UnifyError Subst)
-> UnifyError -> Either UnifyError Subst
forall a b. (a -> b) -> a -> b
$ Type -> Type -> UnifyError
TypeMismatch Type
t1 Type
t2

-- | Unify a list of type pairs with top-level tensor unification
unifyManyWithTopLevel :: [Type] -> [Type] -> Either UnifyError Subst
unifyManyWithTopLevel :: [Type] -> [Type] -> Either UnifyError Subst
unifyManyWithTopLevel [] [] = Subst -> Either UnifyError Subst
forall a b. b -> Either a b
Right Subst
emptySubst
unifyManyWithTopLevel (Type
t1:[Type]
ts1) (Type
t2:[Type]
ts2) = do
  Subst
s1 <- Type -> Type -> Either UnifyError Subst
unifyWithTopLevel Type
t1 Type
t2
  Subst
s2 <- [Type] -> [Type] -> Either UnifyError Subst
unifyManyWithTopLevel ((Type -> Type) -> [Type] -> [Type]
forall a b. (a -> b) -> [a] -> [b]
map (Subst -> Type -> Type
applySubst Subst
s1) [Type]
ts1) ((Type -> Type) -> [Type] -> [Type]
forall a b. (a -> b) -> [a] -> [b]
map (Subst -> Type -> Type
applySubst Subst
s1) [Type]
ts2)
  Subst -> Either UnifyError Subst
forall a b. b -> Either a b
Right (Subst -> Either UnifyError Subst)
-> Subst -> Either UnifyError Subst
forall a b. (a -> b) -> a -> b
$ Subst -> Subst -> Subst
composeSubst Subst
s2 Subst
s1
unifyManyWithTopLevel [Type]
_ [Type]
_ = UnifyError -> Either UnifyError Subst
forall a b. a -> Either a b
Left (UnifyError -> Either UnifyError Subst)
-> UnifyError -> Either UnifyError Subst
forall a b. (a -> b) -> a -> b
$ Type -> Type -> UnifyError
TypeMismatch ([Type] -> Type
TTuple []) ([Type] -> Type
TTuple [])  -- Length mismatch

-- | Unify a list of type pairs
unifyMany :: [Type] -> [Type] -> Either UnifyError Subst
unifyMany :: [Type] -> [Type] -> Either UnifyError Subst
unifyMany [] [] = Subst -> Either UnifyError Subst
forall a b. b -> Either a b
Right Subst
emptySubst
unifyMany (Type
t1:[Type]
ts1) (Type
t2:[Type]
ts2) = do
  Subst
s1 <- Type -> Type -> Either UnifyError Subst
unify Type
t1 Type
t2
  Subst
s2 <- [Type] -> [Type] -> Either UnifyError Subst
unifyMany ((Type -> Type) -> [Type] -> [Type]
forall a b. (a -> b) -> [a] -> [b]
map (Subst -> Type -> Type
applySubst Subst
s1) [Type]
ts1) ((Type -> Type) -> [Type] -> [Type]
forall a b. (a -> b) -> [a] -> [b]
map (Subst -> Type -> Type
applySubst Subst
s1) [Type]
ts2)
  Subst -> Either UnifyError Subst
forall a b. b -> Either a b
Right (Subst -> Either UnifyError Subst)
-> Subst -> Either UnifyError Subst
forall a b. (a -> b) -> a -> b
$ Subst -> Subst -> Subst
composeSubst Subst
s2 Subst
s1
unifyMany [Type]
_ [Type]
_ = UnifyError -> Either UnifyError Subst
forall a b. a -> Either a b
Left (UnifyError -> Either UnifyError Subst)
-> UnifyError -> Either UnifyError Subst
forall a b. (a -> b) -> a -> b
$ Type -> Type -> UnifyError
TypeMismatch ([Type] -> Type
TTuple []) ([Type] -> Type
TTuple [])  -- Length mismatch

--------------------------------------------------------------------------------
-- Constraint-Aware Unification
--------------------------------------------------------------------------------

-- | Unify two types while considering type class constraints
-- This function chooses unifiers that satisfy type class constraints
-- Specifically, when unifying Tensor a with a constrained type variable t:
--   - If C t constraint exists and C (Tensor a) is not satisfiable,
--     prefer t = a over t = Tensor a
-- Returns (Subst, Bool) where Bool indicates if Tensor was unwrapped during unification
unifyWithConstraints :: ClassEnv -> [Constraint] -> Type -> Type -> Either UnifyError (Subst, Bool)
unifyWithConstraints :: ClassEnv
-> [Constraint] -> Type -> Type -> Either UnifyError (Subst, Bool)
unifyWithConstraints ClassEnv
classEnv [Constraint]
constraints Type
t1 Type
t2 =
  let t1' :: Type
t1' = Type -> Type
normalizeInductiveTypes (Type -> Type
normalizeTensorType Type
t1)
      t2' :: Type
t2' = Type -> Type
normalizeInductiveTypes (Type -> Type
normalizeTensorType Type
t2)
  in ClassEnv
-> [Constraint] -> Type -> Type -> Either UnifyError (Subst, Bool)
unifyWithConstraints' ClassEnv
classEnv [Constraint]
constraints Type
t1' Type
t2'

unifyWithConstraints' :: ClassEnv -> [Constraint] -> Type -> Type -> Either UnifyError (Subst, Bool)
-- Same types unify trivially
unifyWithConstraints' :: ClassEnv
-> [Constraint] -> Type -> Type -> Either UnifyError (Subst, Bool)
unifyWithConstraints' ClassEnv
_ [Constraint]
_ Type
TInt Type
TInt = (Subst, Bool) -> Either UnifyError (Subst, Bool)
forall a b. b -> Either a b
Right (Subst
emptySubst, Bool
False)
unifyWithConstraints' ClassEnv
_ [Constraint]
_ Type
TMathExpr Type
TMathExpr = (Subst, Bool) -> Either UnifyError (Subst, Bool)
forall a b. b -> Either a b
Right (Subst
emptySubst, Bool
False)
unifyWithConstraints' ClassEnv
_ [Constraint]
_ Type
TPolyExpr Type
TPolyExpr = (Subst, Bool) -> Either UnifyError (Subst, Bool)
forall a b. b -> Either a b
Right (Subst
emptySubst, Bool
False)
unifyWithConstraints' ClassEnv
_ [Constraint]
_ Type
TTermExpr Type
TTermExpr = (Subst, Bool) -> Either UnifyError (Subst, Bool)
forall a b. b -> Either a b
Right (Subst
emptySubst, Bool
False)
unifyWithConstraints' ClassEnv
_ [Constraint]
_ Type
TSymbolExpr Type
TSymbolExpr = (Subst, Bool) -> Either UnifyError (Subst, Bool)
forall a b. b -> Either a b
Right (Subst
emptySubst, Bool
False)
unifyWithConstraints' ClassEnv
_ [Constraint]
_ Type
TIndexExpr Type
TIndexExpr = (Subst, Bool) -> Either UnifyError (Subst, Bool)
forall a b. b -> Either a b
Right (Subst
emptySubst, Bool
False)
unifyWithConstraints' ClassEnv
_ [Constraint]
_ Type
TFloat Type
TFloat = (Subst, Bool) -> Either UnifyError (Subst, Bool)
forall a b. b -> Either a b
Right (Subst
emptySubst, Bool
False)
unifyWithConstraints' ClassEnv
_ [Constraint]
_ Type
TBool Type
TBool = (Subst, Bool) -> Either UnifyError (Subst, Bool)
forall a b. b -> Either a b
Right (Subst
emptySubst, Bool
False)
unifyWithConstraints' ClassEnv
_ [Constraint]
_ Type
TChar Type
TChar = (Subst, Bool) -> Either UnifyError (Subst, Bool)
forall a b. b -> Either a b
Right (Subst
emptySubst, Bool
False)
unifyWithConstraints' ClassEnv
_ [Constraint]
_ Type
TString Type
TString = (Subst, Bool) -> Either UnifyError (Subst, Bool)
forall a b. b -> Either a b
Right (Subst
emptySubst, Bool
False)

-- Special rule: TInt and TMathExpr unify to TMathExpr
unifyWithConstraints' ClassEnv
_ [Constraint]
_ Type
TInt Type
TMathExpr = (Subst, Bool) -> Either UnifyError (Subst, Bool)
forall a b. b -> Either a b
Right (Subst
emptySubst, Bool
False)
unifyWithConstraints' ClassEnv
_ [Constraint]
_ Type
TMathExpr Type
TInt = (Subst, Bool) -> Either UnifyError (Subst, Bool)
forall a b. b -> Either a b
Right (Subst
emptySubst, Bool
False)

-- Type variables - with constraint-aware Tensor handling
unifyWithConstraints' ClassEnv
classEnv [Constraint]
constraints (TVar TyVar
v) Type
t =
  ClassEnv
-> [Constraint] -> TyVar -> Type -> Either UnifyError (Subst, Bool)
unifyVarWithConstraints ClassEnv
classEnv [Constraint]
constraints TyVar
v Type
t
unifyWithConstraints' ClassEnv
classEnv [Constraint]
constraints Type
t (TVar TyVar
v) =
  ClassEnv
-> [Constraint] -> TyVar -> Type -> Either UnifyError (Subst, Bool)
unifyVarWithConstraints ClassEnv
classEnv [Constraint]
constraints TyVar
v Type
t

unifyWithConstraints' ClassEnv
classEnv [Constraint]
constraints (TTuple [Type]
ts1) (TTuple [Type]
ts2)
  | [Type] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Type]
ts1 Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== [Type] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Type]
ts2 = ClassEnv
-> [Constraint]
-> [Type]
-> [Type]
-> Either UnifyError (Subst, Bool)
unifyManyWithConstraints ClassEnv
classEnv [Constraint]
constraints [Type]
ts1 [Type]
ts2
  | Bool
otherwise = UnifyError -> Either UnifyError (Subst, Bool)
forall a b. a -> Either a b
Left (UnifyError -> Either UnifyError (Subst, Bool))
-> UnifyError -> Either UnifyError (Subst, Bool)
forall a b. (a -> b) -> a -> b
$ Type -> Type -> UnifyError
TypeMismatch ([Type] -> Type
TTuple [Type]
ts1) ([Type] -> Type
TTuple [Type]
ts2)

unifyWithConstraints' ClassEnv
classEnv [Constraint]
constraints (TCollection Type
t1) (TCollection Type
t2) = do
  (Subst
s, Bool
flag) <- ClassEnv
-> [Constraint] -> Type -> Type -> Either UnifyError (Subst, Bool)
unifyWithConstraints ClassEnv
classEnv [Constraint]
constraints Type
t1 Type
t2
  (Subst, Bool) -> Either UnifyError (Subst, Bool)
forall a b. b -> Either a b
Right (Subst
s, Bool
flag)

-- Inductive types
unifyWithConstraints' ClassEnv
classEnv [Constraint]
constraints (TInductive String
n1 [Type]
ts1) (TInductive String
n2 [Type]
ts2)
  | String
n1 String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== String
n2 Bool -> Bool -> Bool
&& [Type] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Type]
ts1 Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== [Type] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Type]
ts2 = ClassEnv
-> [Constraint]
-> [Type]
-> [Type]
-> Either UnifyError (Subst, Bool)
unifyManyWithConstraints ClassEnv
classEnv [Constraint]
constraints [Type]
ts1 [Type]
ts2
  | Bool
otherwise = UnifyError -> Either UnifyError (Subst, Bool)
forall a b. a -> Either a b
Left (UnifyError -> Either UnifyError (Subst, Bool))
-> UnifyError -> Either UnifyError (Subst, Bool)
forall a b. (a -> b) -> a -> b
$ Type -> Type -> UnifyError
TypeMismatch (String -> [Type] -> Type
TInductive String
n1 [Type]
ts1) (String -> [Type] -> Type
TInductive String
n2 [Type]
ts2)

unifyWithConstraints' ClassEnv
classEnv [Constraint]
constraints (THash Type
k1 Type
v1) (THash Type
k2 Type
v2) = do
  (Subst
s1, Bool
flag1) <- ClassEnv
-> [Constraint] -> Type -> Type -> Either UnifyError (Subst, Bool)
unifyWithConstraints ClassEnv
classEnv [Constraint]
constraints Type
k1 Type
k2
  (Subst
s2, Bool
flag2) <- ClassEnv
-> [Constraint] -> Type -> Type -> Either UnifyError (Subst, Bool)
unifyWithConstraints ClassEnv
classEnv ((Constraint -> Constraint) -> [Constraint] -> [Constraint]
forall a b. (a -> b) -> [a] -> [b]
map (Subst -> Constraint -> Constraint
applySubstConstraint Subst
s1) [Constraint]
constraints) (Subst -> Type -> Type
applySubst Subst
s1 Type
v1) (Subst -> Type -> Type
applySubst Subst
s1 Type
v2)
  (Subst, Bool) -> Either UnifyError (Subst, Bool)
forall a b. b -> Either a b
Right (Subst -> Subst -> Subst
composeSubst Subst
s2 Subst
s1, Bool
flag1 Bool -> Bool -> Bool
|| Bool
flag2)

-- Special rule: Matcher b unifies with (t1, t2, ...)
-- by treating each ti as Matcher ci, resulting in b = (c1, c2, ...)
unifyWithConstraints' ClassEnv
classEnv [Constraint]
constraints (TMatcher Type
b) (TTuple [Type]
ts) =
  ClassEnv
-> [Constraint]
-> Type
-> [Type]
-> Either UnifyError (Subst, Bool)
unifyMatcherWithTupleWithConstraints ClassEnv
classEnv [Constraint]
constraints Type
b [Type]
ts
unifyWithConstraints' ClassEnv
classEnv [Constraint]
constraints (TTuple [Type]
ts) (TMatcher Type
b) =
  ClassEnv
-> [Constraint]
-> Type
-> [Type]
-> Either UnifyError (Subst, Bool)
unifyMatcherWithTupleWithConstraints ClassEnv
classEnv [Constraint]
constraints Type
b [Type]
ts

unifyWithConstraints' ClassEnv
classEnv [Constraint]
constraints (TMatcher Type
t1) (TMatcher Type
t2) = do
  (Subst
s, Bool
flag) <- ClassEnv
-> [Constraint] -> Type -> Type -> Either UnifyError (Subst, Bool)
unifyWithConstraints ClassEnv
classEnv [Constraint]
constraints Type
t1 Type
t2
  (Subst, Bool) -> Either UnifyError (Subst, Bool)
forall a b. b -> Either a b
Right (Subst
s, Bool
flag)

unifyWithConstraints' ClassEnv
classEnv [Constraint]
constraints (TFun Type
a1 Type
r1) (TFun Type
a2 Type
r2) = do
  (Subst
s1, Bool
flag1) <- ClassEnv
-> [Constraint] -> Type -> Type -> Either UnifyError (Subst, Bool)
unifyWithConstraints ClassEnv
classEnv [Constraint]
constraints Type
a1 Type
a2
  (Subst
s2, Bool
flag2) <- ClassEnv
-> [Constraint] -> Type -> Type -> Either UnifyError (Subst, Bool)
unifyWithConstraints ClassEnv
classEnv ((Constraint -> Constraint) -> [Constraint] -> [Constraint]
forall a b. (a -> b) -> [a] -> [b]
map (Subst -> Constraint -> Constraint
applySubstConstraint Subst
s1) [Constraint]
constraints) (Subst -> Type -> Type
applySubst Subst
s1 Type
r1) (Subst -> Type -> Type
applySubst Subst
s1 Type
r2)
  (Subst, Bool) -> Either UnifyError (Subst, Bool)
forall a b. b -> Either a b
Right (Subst -> Subst -> Subst
composeSubst Subst
s2 Subst
s1, Bool
flag1 Bool -> Bool -> Bool
|| Bool
flag2)

unifyWithConstraints' ClassEnv
classEnv [Constraint]
constraints (TIO Type
t1) (TIO Type
t2) = do
  (Subst
s, Bool
flag) <- ClassEnv
-> [Constraint] -> Type -> Type -> Either UnifyError (Subst, Bool)
unifyWithConstraints ClassEnv
classEnv [Constraint]
constraints Type
t1 Type
t2
  (Subst, Bool) -> Either UnifyError (Subst, Bool)
forall a b. b -> Either a b
Right (Subst
s, Bool
flag)

unifyWithConstraints' ClassEnv
classEnv [Constraint]
constraints (TIORef Type
t1) (TIORef Type
t2) = do
  (Subst
s, Bool
flag) <- ClassEnv
-> [Constraint] -> Type -> Type -> Either UnifyError (Subst, Bool)
unifyWithConstraints ClassEnv
classEnv [Constraint]
constraints Type
t1 Type
t2
  (Subst, Bool) -> Either UnifyError (Subst, Bool)
forall a b. b -> Either a b
Right (Subst
s, Bool
flag)

unifyWithConstraints' ClassEnv
_ [Constraint]
_ Type
TPort Type
TPort = (Subst, Bool) -> Either UnifyError (Subst, Bool)
forall a b. b -> Either a b
Right (Subst
emptySubst, Bool
False)

-- Tensor types - both Tensor
unifyWithConstraints' ClassEnv
classEnv [Constraint]
constraints (TTensor Type
t1) (TTensor Type
t2) = do
  (Subst
s, Bool
flag) <- ClassEnv
-> [Constraint] -> Type -> Type -> Either UnifyError (Subst, Bool)
unifyWithConstraints ClassEnv
classEnv [Constraint]
constraints Type
t1 Type
t2
  (Subst, Bool) -> Either UnifyError (Subst, Bool)
forall a b. b -> Either a b
Right (Subst
s, Bool
flag)

-- IMPORTANT: Constraint-aware handling for Tensor <-> non-Tensor
-- When unifying Tensor a with non-Tensor, prefer non-Tensor if it satisfies constraints
unifyWithConstraints' ClassEnv
classEnv [Constraint]
constraints (TTensor Type
t1) Type
t2 =
  ClassEnv
-> [Constraint] -> Type -> Type -> Either UnifyError (Subst, Bool)
unifyTensorWithConstraints ClassEnv
classEnv [Constraint]
constraints Type
t1 Type
t2
unifyWithConstraints' ClassEnv
classEnv [Constraint]
constraints Type
t1 (TTensor Type
t2) =
  ClassEnv
-> [Constraint] -> Type -> Type -> Either UnifyError (Subst, Bool)
unifyTensorWithConstraints ClassEnv
classEnv [Constraint]
constraints Type
t2 Type
t1

-- TAny unifies with anything
unifyWithConstraints' ClassEnv
_ [Constraint]
_ Type
TAny Type
_ = (Subst, Bool) -> Either UnifyError (Subst, Bool)
forall a b. b -> Either a b
Right (Subst
emptySubst, Bool
False)
unifyWithConstraints' ClassEnv
_ [Constraint]
_ Type
_ Type
TAny = (Subst, Bool) -> Either UnifyError (Subst, Bool)
forall a b. b -> Either a b
Right (Subst
emptySubst, Bool
False)

-- Mismatched types
unifyWithConstraints' ClassEnv
_ [Constraint]
_ Type
t1 Type
t2 = UnifyError -> Either UnifyError (Subst, Bool)
forall a b. a -> Either a b
Left (UnifyError -> Either UnifyError (Subst, Bool))
-> UnifyError -> Either UnifyError (Subst, Bool)
forall a b. (a -> b) -> a -> b
$ Type -> Type -> UnifyError
TypeMismatch Type
t1 Type
t2

-- | Unify type variable with another type, considering constraints
-- Note: occurs check is deferred to handle cases like unifying t0 with Tensor t0
-- when t0 has constraints (e.g., {Num t0}) and there's no Num (Tensor t0) instance.
-- In such cases, we bind t0 to the element type (t0 itself), which is identity.
-- Returns (Subst, Bool) where Bool indicates if Tensor was unwrapped during unification
unifyVarWithConstraints :: ClassEnv -> [Constraint] -> TyVar -> Type -> Either UnifyError (Subst, Bool)
unifyVarWithConstraints :: ClassEnv
-> [Constraint] -> TyVar -> Type -> Either UnifyError (Subst, Bool)
unifyVarWithConstraints ClassEnv
classEnv [Constraint]
constraints TyVar
v Type
t
  | TyVar -> Type
TVar TyVar
v Type -> Type -> Bool
forall a. Eq a => a -> a -> Bool
== Type
t = (Subst, Bool) -> Either UnifyError (Subst, Bool)
forall a b. b -> Either a b
Right (Subst
emptySubst, Bool
False)
  | Bool
otherwise = case Type
t of
      -- Special handling for Tensor types with constraints
      TTensor Type
elemType ->
        -- Check if the type variable has constraints
        let varConstraints :: [Constraint]
varConstraints = (Constraint -> Bool) -> [Constraint] -> [Constraint]
forall a. (a -> Bool) -> [a] -> [a]
filter (\(Constraint String
_ Type
constraintType) -> Type
constraintType Type -> Type -> Bool
forall a. Eq a => a -> a -> Bool
== TyVar -> Type
TVar TyVar
v) [Constraint]
constraints
        in if [Constraint] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Constraint]
varConstraints
           then
             -- No constraints on this variable, bind to Tensor (need occurs check)
             if TyVar
v TyVar -> Set TyVar -> Bool
forall a. Ord a => a -> Set a -> Bool
`Set.member` Type -> Set TyVar
freeTyVars Type
t
             then UnifyError -> Either UnifyError (Subst, Bool)
forall a b. a -> Either a b
Left (UnifyError -> Either UnifyError (Subst, Bool))
-> UnifyError -> Either UnifyError (Subst, Bool)
forall a b. (a -> b) -> a -> b
$ TyVar -> Type -> UnifyError
OccursCheck TyVar
v Type
t
             else (Subst, Bool) -> Either UnifyError (Subst, Bool)
forall a b. b -> Either a b
Right (TyVar -> Type -> Subst
singletonSubst TyVar
v Type
t, Bool
False)
           else
             -- Has constraints: check if Tensor has instances for all of them
             if (Constraint -> Bool) -> [Constraint] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (ClassEnv -> Type -> Constraint -> Bool
hasInstanceForTensorType ClassEnv
classEnv Type
elemType) [Constraint]
varConstraints
             then
               -- All constraints have Tensor instances, bind to Tensor (need occurs check)
               if TyVar
v TyVar -> Set TyVar -> Bool
forall a. Ord a => a -> Set a -> Bool
`Set.member` Type -> Set TyVar
freeTyVars Type
t
               then UnifyError -> Either UnifyError (Subst, Bool)
forall a b. a -> Either a b
Left (UnifyError -> Either UnifyError (Subst, Bool))
-> UnifyError -> Either UnifyError (Subst, Bool)
forall a b. (a -> b) -> a -> b
$ TyVar -> Type -> UnifyError
OccursCheck TyVar
v Type
t
               else (Subst, Bool) -> Either UnifyError (Subst, Bool)
forall a b. b -> Either a b
Right (TyVar -> Type -> Subst
singletonSubst TyVar
v Type
t, Bool
False)
             else
               -- Some constraint lacks Tensor instance, bind to element type instead
               -- This allows tensorMap to handle the Tensor -> scalar conversion
               -- Special case: if v == elemType (e.g., t0 with Tensor t0), return identity
               -- FLAG: Set to True because Tensor was unwrapped
               if TyVar -> Type
TVar TyVar
v Type -> Type -> Bool
forall a. Eq a => a -> a -> Bool
== Type
elemType
               then (Subst, Bool) -> Either UnifyError (Subst, Bool)
forall a b. b -> Either a b
Right (Subst
emptySubst, Bool
True)
               else if TyVar
v TyVar -> Set TyVar -> Bool
forall a. Ord a => a -> Set a -> Bool
`Set.member` Type -> Set TyVar
freeTyVars Type
elemType
                    then UnifyError -> Either UnifyError (Subst, Bool)
forall a b. a -> Either a b
Left (UnifyError -> Either UnifyError (Subst, Bool))
-> UnifyError -> Either UnifyError (Subst, Bool)
forall a b. (a -> b) -> a -> b
$ TyVar -> Type -> UnifyError
OccursCheck TyVar
v Type
elemType
                    else (Subst, Bool) -> Either UnifyError (Subst, Bool)
forall a b. b -> Either a b
Right (TyVar -> Type -> Subst
singletonSubst TyVar
v Type
elemType, Bool
True)
      Type
_ ->
        -- Non-Tensor type, regular occurs check
        if TyVar
v TyVar -> Set TyVar -> Bool
forall a. Ord a => a -> Set a -> Bool
`Set.member` Type -> Set TyVar
freeTyVars Type
t
        then UnifyError -> Either UnifyError (Subst, Bool)
forall a b. a -> Either a b
Left (UnifyError -> Either UnifyError (Subst, Bool))
-> UnifyError -> Either UnifyError (Subst, Bool)
forall a b. (a -> b) -> a -> b
$ TyVar -> Type -> UnifyError
OccursCheck TyVar
v Type
t
        else (Subst, Bool) -> Either UnifyError (Subst, Bool)
forall a b. b -> Either a b
Right (TyVar -> Type -> Subst
singletonSubst TyVar
v Type
t, Bool
False)

-- | Check if there's an instance for Constraint (Tensor elemType)
-- e.g., check if Num (Tensor Integer) exists given elemType = Integer and constraint = Num
hasInstanceForTensorType :: ClassEnv -> Type -> Constraint -> Bool
hasInstanceForTensorType :: ClassEnv -> Type -> Constraint -> Bool
hasInstanceForTensorType ClassEnv
classEnv Type
elemType (Constraint String
className Type
_) =
  let tensorType :: Type
tensorType = Type -> Type
TTensor Type
elemType
      instances :: [InstanceInfo]
instances = String -> ClassEnv -> [InstanceInfo]
lookupInstances String
className ClassEnv
classEnv
  in (InstanceInfo -> Bool) -> [InstanceInfo] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (\InstanceInfo
inst -> case Type -> Type -> Either UnifyError Subst
unifyStrict (InstanceInfo -> Type
instType InstanceInfo
inst) Type
tensorType of
                     Right Subst
_ -> Bool
True
                     Left UnifyError
_  -> Bool
False
         ) [InstanceInfo]
instances

-- | Unify Tensor elemType with a non-Tensor type, considering constraints
-- Returns (Subst, Bool) where Bool indicates if Tensor was unwrapped during unification
unifyTensorWithConstraints :: ClassEnv -> [Constraint] -> Type -> Type -> Either UnifyError (Subst, Bool)
unifyTensorWithConstraints :: ClassEnv
-> [Constraint] -> Type -> Type -> Either UnifyError (Subst, Bool)
unifyTensorWithConstraints ClassEnv
classEnv [Constraint]
constraints Type
elemType Type
otherType =
  case Type
otherType of
    TVar TyVar
v ->
      -- Symmetric case: handled by unifyVarWithConstraints
      ClassEnv
-> [Constraint] -> TyVar -> Type -> Either UnifyError (Subst, Bool)
unifyVarWithConstraints ClassEnv
classEnv [Constraint]
constraints TyVar
v (Type -> Type
TTensor Type
elemType)
    Type
_ ->
      -- Normal unification: Tensor elemType with otherType means elemType = otherType
      -- FLAG: Set to True because we're unwrapping Tensor
      do
        (Subst
s, Bool
_) <- ClassEnv
-> [Constraint] -> Type -> Type -> Either UnifyError (Subst, Bool)
unifyWithConstraints ClassEnv
classEnv [Constraint]
constraints Type
elemType Type
otherType
        (Subst, Bool) -> Either UnifyError (Subst, Bool)
forall a b. b -> Either a b
Right (Subst
s, Bool
True)

-- | Unify multiple type pairs with constraints
-- Returns (Subst, Bool) where Bool indicates if any Tensor was unwrapped during unification
unifyManyWithConstraints :: ClassEnv -> [Constraint] -> [Type] -> [Type] -> Either UnifyError (Subst, Bool)
unifyManyWithConstraints :: ClassEnv
-> [Constraint]
-> [Type]
-> [Type]
-> Either UnifyError (Subst, Bool)
unifyManyWithConstraints ClassEnv
_ [Constraint]
_ [] [] = (Subst, Bool) -> Either UnifyError (Subst, Bool)
forall a b. b -> Either a b
Right (Subst
emptySubst, Bool
False)
unifyManyWithConstraints ClassEnv
classEnv [Constraint]
constraints (Type
t1:[Type]
ts1) (Type
t2:[Type]
ts2) = do
  (Subst
s1, Bool
flag1) <- ClassEnv
-> [Constraint] -> Type -> Type -> Either UnifyError (Subst, Bool)
unifyWithConstraints ClassEnv
classEnv [Constraint]
constraints Type
t1 Type
t2
  let constraints' :: [Constraint]
constraints' = (Constraint -> Constraint) -> [Constraint] -> [Constraint]
forall a b. (a -> b) -> [a] -> [b]
map (Subst -> Constraint -> Constraint
applySubstConstraint Subst
s1) [Constraint]
constraints
  (Subst
s2, Bool
flag2) <- ClassEnv
-> [Constraint]
-> [Type]
-> [Type]
-> Either UnifyError (Subst, Bool)
unifyManyWithConstraints ClassEnv
classEnv [Constraint]
constraints' ((Type -> Type) -> [Type] -> [Type]
forall a b. (a -> b) -> [a] -> [b]
map (Subst -> Type -> Type
applySubst Subst
s1) [Type]
ts1) ((Type -> Type) -> [Type] -> [Type]
forall a b. (a -> b) -> [a] -> [b]
map (Subst -> Type -> Type
applySubst Subst
s1) [Type]
ts2)
  (Subst, Bool) -> Either UnifyError (Subst, Bool)
forall a b. b -> Either a b
Right (Subst -> Subst -> Subst
composeSubst Subst
s2 Subst
s1, Bool
flag1 Bool -> Bool -> Bool
|| Bool
flag2)
unifyManyWithConstraints ClassEnv
_ [Constraint]
_ [Type]
_ [Type]
_ = UnifyError -> Either UnifyError (Subst, Bool)
forall a b. a -> Either a b
Left (UnifyError -> Either UnifyError (Subst, Bool))
-> UnifyError -> Either UnifyError (Subst, Bool)
forall a b. (a -> b) -> a -> b
$ Type -> Type -> UnifyError
TypeMismatch ([Type] -> Type
TTuple []) ([Type] -> Type
TTuple [])

-- | Unify Matcher b with (t1, t2, ...) using constraint-aware unification
-- Result: b = (c1, c2, ...) where ti unifies with Matcher ci
-- Returns (Subst, Bool) where Bool indicates if any Tensor was unwrapped during unification
unifyMatcherWithTupleWithConstraints :: ClassEnv -> [Constraint] -> Type -> [Type] -> Either UnifyError (Subst, Bool)
unifyMatcherWithTupleWithConstraints :: ClassEnv
-> [Constraint]
-> Type
-> [Type]
-> Either UnifyError (Subst, Bool)
unifyMatcherWithTupleWithConstraints ClassEnv
classEnv [Constraint]
constraints Type
b [Type]
ts = do
  -- Process each element: extract inner type or create constraint
  ([Type]
innerTypes, Subst
s1, Bool
flag1) <- ClassEnv
-> [Constraint]
-> [Type]
-> Subst
-> Either UnifyError ([Type], Subst, Bool)
unifyEachAsMatcherWithConstraints ClassEnv
classEnv [Constraint]
constraints [Type]
ts Subst
emptySubst
  -- Now unify b with (c1, c2, ...)
  let tupleType :: Type
tupleType = [Type] -> Type
TTuple [Type]
innerTypes
      constraints' :: [Constraint]
constraints' = (Constraint -> Constraint) -> [Constraint] -> [Constraint]
forall a b. (a -> b) -> [a] -> [b]
map (Subst -> Constraint -> Constraint
applySubstConstraint Subst
s1) [Constraint]
constraints
  (Subst
s2, Bool
flag2) <- ClassEnv
-> [Constraint] -> Type -> Type -> Either UnifyError (Subst, Bool)
unifyWithConstraints ClassEnv
classEnv [Constraint]
constraints' (Subst -> Type -> Type
applySubst Subst
s1 Type
b) Type
tupleType
  (Subst, Bool) -> Either UnifyError (Subst, Bool)
forall a b. b -> Either a b
Right (Subst -> Subst -> Subst
composeSubst Subst
s2 Subst
s1, Bool
flag1 Bool -> Bool -> Bool
|| Bool
flag2)
  where
    -- Unify each type in the tuple with Matcher ci, extracting ci
    unifyEachAsMatcherWithConstraints :: ClassEnv -> [Constraint] -> [Type] -> Subst -> Either UnifyError ([Type], Subst, Bool)
    unifyEachAsMatcherWithConstraints :: ClassEnv
-> [Constraint]
-> [Type]
-> Subst
-> Either UnifyError ([Type], Subst, Bool)
unifyEachAsMatcherWithConstraints ClassEnv
_ [Constraint]
_ [] Subst
s = ([Type], Subst, Bool) -> Either UnifyError ([Type], Subst, Bool)
forall a b. b -> Either a b
Right ([], Subst
s, Bool
False)
    unifyEachAsMatcherWithConstraints ClassEnv
env [Constraint]
cons (Type
t:[Type]
rest) Subst
s = do
      let t' :: Type
t' = Subst -> Type -> Type
applySubst Subst
s Type
t
          cons' :: [Constraint]
cons' = (Constraint -> Constraint) -> [Constraint] -> [Constraint]
forall a b. (a -> b) -> [a] -> [b]
map (Subst -> Constraint -> Constraint
applySubstConstraint Subst
s) [Constraint]
cons
      (Type
innerType, Subst
s1, Bool
flag1) <- case Type
t' of
        -- If already Matcher c, extract c
        TMatcher Type
inner -> (Type, Subst, Bool) -> Either UnifyError (Type, Subst, Bool)
forall a b. b -> Either a b
Right (Type
inner, Subst
emptySubst, Bool
False)
        -- If type variable, unify it with Matcher (fresh variable)
        TVar TyVar
v -> do
          -- Generate a new variable name for the inner type
          let innerVar :: TyVar
innerVar = String -> TyVar
TyVar (TyVar -> String
getTyVarName TyVar
v String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"'")
              innerType :: Type
innerType = TyVar -> Type
TVar TyVar
innerVar
          (Subst
s', Bool
flag) <- ClassEnv
-> [Constraint] -> Type -> Type -> Either UnifyError (Subst, Bool)
unifyWithConstraints ClassEnv
env [Constraint]
cons' Type
t' (Type -> Type
TMatcher Type
innerType)
          (Type, Subst, Bool) -> Either UnifyError (Type, Subst, Bool)
forall a b. b -> Either a b
Right (Subst -> Type -> Type
applySubst Subst
s' Type
innerType, Subst
s', Bool
flag)
        -- Other types cannot be unified with Matcher
        Type
_ -> UnifyError -> Either UnifyError (Type, Subst, Bool)
forall a b. a -> Either a b
Left (UnifyError -> Either UnifyError (Type, Subst, Bool))
-> UnifyError -> Either UnifyError (Type, Subst, Bool)
forall a b. (a -> b) -> a -> b
$ Type -> Type -> UnifyError
TypeMismatch (Type -> Type
TMatcher (TyVar -> Type
TVar (String -> TyVar
TyVar String
"?"))) Type
t'

      let s2 :: Subst
s2 = Subst -> Subst -> Subst
composeSubst Subst
s1 Subst
s
          cons'' :: [Constraint]
cons'' = (Constraint -> Constraint) -> [Constraint] -> [Constraint]
forall a b. (a -> b) -> [a] -> [b]
map (Subst -> Constraint -> Constraint
applySubstConstraint Subst
s2) [Constraint]
cons
      ([Type]
restInnerTypes, Subst
s3, Bool
flag2) <- ClassEnv
-> [Constraint]
-> [Type]
-> Subst
-> Either UnifyError ([Type], Subst, Bool)
unifyEachAsMatcherWithConstraints ClassEnv
env [Constraint]
cons'' [Type]
rest Subst
s2
      ([Type], Subst, Bool) -> Either UnifyError ([Type], Subst, Bool)
forall a b. b -> Either a b
Right (Subst -> Type -> Type
applySubst Subst
s3 Type
innerType Type -> [Type] -> [Type]
forall a. a -> [a] -> [a]
: [Type]
restInnerTypes, Subst
s3, Bool
flag1 Bool -> Bool -> Bool
|| Bool
flag2)

    getTyVarName :: TyVar -> String
    getTyVarName :: TyVar -> String
getTyVarName (TyVar String
name) = String
name