-- | Evidence terms and coercions.
--
-- Evidence should be a first-class IR concept from day one.
-- Class constraints elaborate to dictionaries, equality constraints
-- elaborate to coercions.
module Aihc.Tc.Evidence
  ( -- * Evidence variables
    EvVar (..),

    -- * Evidence terms
    EvTerm (..),
    EvBinding (..),

    -- * Coercions
    Coercion (..),
  )
where

import Aihc.Tc.Types
import Data.Text (Text)

-- | An evidence variable, uniquely identified.
newtype EvVar = EvVar {evVarUnique :: Unique}
  deriving (Eq, Ord, Show, Read)

-- | Evidence terms.
--
-- Every wanted constraint gets an evidence variable; the solver fills it.
-- The evidence is then used during elaboration to produce dictionary-passing
-- and coercion-carrying core.
data EvTerm
  = -- | Reference to an evidence variable (given or previously solved).
    EvVarTerm !EvVar
  | -- | Given dictionary from a qualified type.
    EvGiven !Pred
  | -- | Dictionary construction: origin, dictionary name, type args, sub-evidence.
    EvDict !(Maybe (Text, Text)) !Text ![TcType] ![EvTerm]
  | -- | Coercion evidence (for equality constraints).
    EvCoercion !Coercion
  | -- | Superclass selection from a dictionary. The source class origin,
    -- predicate, and complete field layout make the projection explicit.
    EvSuperClass !EvTerm !(Maybe (Text, Text)) !Pred ![TcType] !Int
  | -- | Cast evidence through a coercion.
    EvCast !EvTerm !Coercion
  | -- | Compiler-synthesized structural runtime type representation.
    EvTypeable !(Maybe (Text, Text)) !TcType ![EvTerm]
  deriving (Eq, Show, Read)

-- | A binding of an evidence variable to its term.
data EvBinding = EvBinding
  { evBindVar :: !EvVar,
    evBindTerm :: !EvTerm
  }
  deriving (Eq, Show, Read)

-- | Coercions for type equality evidence.
--
-- The full coercion language will grow to support GADTs and type families.
-- For the MVP, only 'Refl' and 'CoVar' are actively produced by the solver.
data Coercion
  = -- | Coercion variable.
    CoVar !EvVar
  | -- | Reflexivity: @t ~ t@.
    Refl !TcType
  | -- | Symmetry: if @co : t1 ~ t2@ then @Sym co : t2 ~ t1@.
    Sym !Coercion
  | -- | Transitivity: @Trans co1 co2 : t1 ~ t3@.
    Trans !Coercion !Coercion
  | -- | Lift through type constructor: @T co1 ... con@.
    TyConAppCo !TyCon ![Coercion]
  | -- | Type family / newtype axiom instantiation (future).
    AxiomInstCo !Text ![TcType]
  deriving (Eq, Show, Read)
