{-# LANGUAGE GeneralizedNewtypeDeriving #-}
module Type 
  ( module Type
  , Id(..)
  ) where

import Control.Monad.Reader
import Control.Monad.State
import Control.Monad.Except

import Data.Map (Map)
import Data.Set (Set)
import Data.Text (Text)

import Hm.Abs (Id(..))

data PolyT
  = Forall (Set Id) MonoT -- ^ ∀ σ₁ σ₂ … σₙ. τ
  | Mono MonoT        -- ^ τ
  deriving Show

infixr `TArr`
data MonoT
  = TArr MonoT MonoT -- ^ function
  | TVar Id          -- ^ variable
  | TCon Id          -- ^ constant
  deriving Show

type Pos = Maybe (Int, Int)

type TL = TL' Pos
data TL' a
  = TypeDef a Id [Id]  TypeEnv -- ^ name, parameters, constructors and recursor
  | VarDef  a Id PolyT Exp     -- ^ name, declared type, expression

type Exp = Exp' Pos
data Exp' a
  = Typed a Exp MonoT
  | Let a [(Id, Exp)] Exp
  | Abs a [Id] Exp
  | App a Exp [Exp]
  | Var a Id

data TypeError
  = Oop -- ^ compiler error (oops)
  | UnificationFailure MonoT MonoT
  | InfiniteType Id MonoT
  | UnboundVariable Id
  | Unimplemented Text
  | InvalidTypeDecl Pos
  | InvalidConstructor Pos
  deriving Show

type TypeEnv = Map Id PolyT

type Subst = Map Id MonoT

data CheckState = CS { variables :: [Id] 
                     , lastPos :: Pos
                     , typeEnv :: TypeEnv
                     } deriving Show

newtype Check a = Check { getCheck :: ExceptT TypeError (State CheckState) a }
  deriving (Functor, Applicative, Monad, MonadError TypeError, MonadState CheckState)

instance MonadFail Check where
  fail _ = throwError Oop