{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeFamilies #-}
{-# OPTIONS_GHC -fno-warn-tabs #-}

-- | The point at which point inconsistency is detected.
-- depends on the ordering of the 'Constraint's
-- and on the 'Solver's used.
--
-- Because choosing an ordering for the 'Constraint's
-- closely relates to the order in which types are unified (with 'mgu_with_synonyms'),
-- a /greedy 'Constraint' solver/, beeing highly sensitive
-- to the order in which it solves 'Constraint_Monotype_Unification's,
-- will report different 'Constraint's for different orders.
module Language.LOL.Typing.Solver.Greedy where

import Control.Monad (Monad)
import qualified Control.Monad.Classes as MC
import Data.Bool (Bool(..))
import Data.Sequence (Seq)
import Data.Text.Buildable (Buildable(..))

import Language.LOL.Typing.Type
import Language.LOL.Typing.Solver.Common
import Language.LOL.Typing.Solver.Constraint
import Language.LOL.Typing.Solver.Monotype
import Language.LOL.Typing.Solver.Polytype
import Language.LOL.Typing.Solver.Class
import Language.LOL.Typing.Solver.Monad
import qualified Language.LOL.Typing.Lib.Control.Monad.Classes.StateInstance as MC

-- * Type 'Solver_Greedy_Finite'

type Solver_Greedy_Finite info m
   = Solver info m Substitution_Finite

solver_greedy_finite ::
 ( sol ~ Solver_Greedy_Finite info m
 , res ~ Solver_Result (Info sol) (Error sol)
 , Monad m
 , Solvable constraint sol
 , MC.CansMonadStateInstance State (MC.EffState ()) m ~ '[ 'False ]
 , Buildable info
 , Infoable Info_Monotype info
 , Infoable Info_Polytype info
 , Infoable (Info_Class info) info
 ) => Solver_Config -> Seq constraint -> sol res
solver_greedy_finite = solver

-- * Type 'Solver_Greedy_Fixpoint'

type Solver_Greedy_Fixpoint info m
 =   Solver info m Substitution_Fixpoint

solver_greedy_fixpoint ::
 ( sol ~ Solver_Greedy_Fixpoint info m
 , res ~ Solver_Result (Info sol) (Error sol)
 , Monad m
 , Solvable constraint sol
 , MC.CansMonadStateInstance State (MC.EffState ()) m ~ '[ 'False ]
 , Buildable info
 , Infoable Info_Monotype info
 , Infoable Info_Polytype info
 , Infoable (Info_Class info) info
 ) => Solver_Config -> Seq constraint -> sol res
solver_greedy_fixpoint = solver