{-# LANGUAGE TypeFamilies #-}
-- | The internal representation of types, created by the type checker
--   from the syntactic types in 'AST.Type'.
module Type.Internal (
  -- * Data definitions
  -- ** Types
  Quant(..), TyVar(..), Type(..), TyCon(..),
  -- ** Qualifiers
  QLit(..), QExp(..), QExpV,
  -- ** Type patterns
  TyPat(..),
  -- ** Kind re-exports
  Variance(..), Lattice(..), BoundedLattice(..), isQVariance,
  -- ** Names
  Name, TypId, QTypId, ConId, QConId, RowLabel, RecLabel,

  -- * Qualifiers
  Qualifier(..), qlitexp, qvarexp, extractQual, liftVQExp, mapQExp,

  -- * Type constructors
  abstractTyCon, mkTC,
  -- ** Built-in
  tcUnit, tcInt, tcChar, tcFloat, tcString, tcExn, tcTuple, tcFun,
  tcUn, tcAf, tcJoin, tcRowEnd, tcRecord, tcVariant, tcRowMap,
  tcRowDots, tcRowHole,
  -- ** Convenient constructors and projections
  fvTy, bvTy, fromFreeTV,
  -- ** Pre-constructed types
  tyNulOp, tyUnOp, tyBinOp,
  tyFun, tyArr, tyLol, tyTuple, tyQLit,
  tyAf, tyUn, tyUnit, tyInt, tyChar, tyFloat, tyString, tyExn,
  tyRecord, tyRowEnd, tyRowMap, tyRowHole,
  (.->.), (.-*.), (.*.),
  -- *** For testing
  tcCycle, tcConst, tcIdent, tcConsTup, tcOption, tcIdfun,
  tcSessOne, tcSessSend, tcSessRecv, tcSessSemi, tcSessDual,

  -- * Standard forms
  standardizeType, standardizeQuals,

  -- * Unfolds and folds
  -- ** Type folding
  foldType, foldTypeM, foldTypeEnv, mkBvF, mkQuF, mkMuF,
  -- ** Unfolds
  unfoldQu, unfoldRow, unfoldMu,
  -- ** Row operations
  foldRow, sortRow,

  -- * Locally nameless
  openTy, openTyN, closeTy, lcTy, lcTyK,
  closeRec, closeQuant,

  -- * Varieties
  TyConVariety(..), varietyOf,

  module Data.Empty,
) where

import Util
import Util.MonadRef
import Data.Empty
import Data.Lattice
import Error
import qualified Env
import qualified AST
import AST ( QLit(..), Variance(..), isQVariance )

import Prelude ()
import Control.Monad.ST
import Data.Generics (Typeable, Data)
import Data.STRef (STRef)
import qualified Data.List as List
import qualified Data.Map  as M
import qualified Data.Set  as S

---
--- DATA TYPES
---

-- | Everything should be renamed by now
type R        = AST.Renamed
type TypId    = AST.TypId R
type QTypId   = AST.QTypId R
type ConId    = AST.ConId R
type QConId   = AST.QConId R
type RowLabel = AST.Uid R
type RecLabel = AST.Lid R

-- | Optional names that don't affect α equivalence
type Name = Perhaps String

-- | Locally-nameless–style type variable occurrences in internal types
data TyVar tv
  -- | A free type variable
  = Free !tv
  -- | A bound type variable
  | Bound !Int !Int !Name
  deriving (Eq, Ord, Functor, Typeable, Data)

-- | Quantifiers
data Quant
  -- | Universal quantifier
  = Forall
  -- | Existential quantifier
  | Exists
  deriving (Eq, Ord, Typeable, Data)

-- | The internal representation of a type
data Type tv
  -- | A free type variable
  = TyVar !(TyVar tv)
  -- | A quantified (all or ex) type
  | TyQu  !Quant ![(Name, QLit)] !(Type tv)
  -- | A recursive (mu) type
  | TyMu  !Name !(Type tv)
  -- | A row type
  | TyRow !RowLabel !(Type tv) !(Type tv)
  -- | The application of a type constructor (possibly nullary).
  | TyApp !TyCon ![Type tv]
  deriving (Functor, Typeable, Data)

-- | Internal qualifier expressions
data QExp tv
  -- | The type qualifier expression
  = QeA
  -- | The join of a set of type variables
  | QeU !(S.Set tv)
  deriving (Eq, Typeable, Data)

-- | Qualifier expressions containing bound variables
type QExpV tv = QExp (TyVar tv)

-- | Information about a type constructor
data TyCon
  = TyCon {
      -- | Unique ID
      tcId        ∷ !Int,
      -- | Printable name
      tcName      ∷ !QTypId,
      -- | Variances for parameters, and correct length
      tcArity     ∷ ![Variance],
      -- | Bounds for parameters
      tcBounds    ∷ ![QLit],
      -- | Guards recursive types
      tcGuards    ∷ ![Bool],
      -- | Qualifier as a function of parameters
      tcQual      ∷ !(QExp Int),
      -- | For pattern-matchable types, the data constructors,
      -- where type parameters are bound at level 0
      tcCons      ∷ !(Env.Env ConId (Maybe (Type Empty))),
      -- | For type operators, the next head reduction
      tcNext      ∷ !(Maybe [([TyPat], Type Empty)])
    }
  deriving (Typeable, Data)

-- | A type pattern, for defining type operators
data TyPat
  -- | A type variable, matching any type and binding
  = TpVar !Name
  -- | A type application node, matching the given constructor
  --   and its parameters
  | TpApp !TyCon ![TyPat]
  -- | A row type pattern
  | TpRow !Name
  deriving (Typeable, Data)

instance Eq TyCon where
  tc == tc'  =  tcId tc == tcId tc'

instance Ord TyCon where
  compare tc tc'  = compare (tcName tc) (tcName tc')

---
--- Abstracting type constructors
---

-- | Remove the representation from a type constructor
abstractTyCon ∷ TyCon → TyCon
abstractTyCon tc = tc { tcCons = mempty, tcNext = Nothing }

---
--- Built-in types
---

class ExtTC r where
  extTC ∷ TyCon → r

instance ExtTC TyCon where
  extTC = id

instance ExtTC r ⇒ ExtTC (QTypId → r) where
  extTC tc x = extTC (tc { tcName = x })

instance (v ~ Variance, ql ~ QLit, ExtTC r) ⇒
         ExtTC ([(v, ql, Bool)] → r) where
  extTC tc x = extTC tc {
                 tcArity  = sel1 <$> x,
                 tcBounds = sel2 <$> x,
                 tcGuards = sel3 <$> x
               }

instance (tv ~ Int, ExtTC r) ⇒ ExtTC (QExp tv → r) where
  extTC tc x = extTC (tc { tcQual = x })

instance (a ~ Type Empty, ExtTC r) ⇒
         ExtTC (Env.Env ConId (Maybe a) → r) where
  extTC tc x = extTC (tc { tcCons = x })

instance (t ~ Type Empty, ExtTC r) ⇒
         ExtTC ([([TyPat], t)] → r) where
  extTC tc x = extTC (tc { tcNext = Just x })

mkTC ∷ ExtTC r ⇒ Int → AST.QTypId R → r
mkTC i ql
  = extTC TyCon {
    tcId        = i,
    tcName      = ql,
    tcArity     = [],
    tcBounds    = [],
    tcGuards    = [],
    tcQual      = minBound,
    tcCons      = Env.empty,
    tcNext      = Nothing
  }

internalTC ∷ ExtTC r ⇒ Int → String → r
internalTC i s = mkTC i (AST.J [] (AST.identT (AST.Ren_ i) s))

tcUnit, tcInt, tcChar, tcFloat, tcString,
  tcExn, tcUn, tcAf, tcJoin, tcTuple, tcFun,
  tcRowEnd, tcRecord, tcVariant, tcRowMap, tcRowDots, tcRowHole ∷ TyCon

tcFun        = internalTC (-1) "->"     (qvarexp 1)
                                        [(Contravariant, Qa, False),
                                         (QCovariant,    Qa, False),
                                         (Covariant,     Qa, False)]
tcUnit       = internalTC (-2) "unit"
                 (Env.fromList [(AST.ident "()" ∷ ConId, Nothing)])
tcInt        = internalTC (-3) "int"
tcChar       = internalTC (-4) "char"
tcFloat      = internalTC (-5) "float"
tcString     = internalTC (-6) "string"
tcExn        = internalTC (-7) "exn"    QeA
tcUn         = internalTC (-8) "U"
tcAf         = internalTC (-9) "A"      QeA
tcJoin       = internalTC (-10) "\\/"   (qvarexp 0 ⊔ qvarexp 1)
                                        [(Covariant,     Qa, False),
                                         (Covariant,     Qa, False)]
tcTuple      = internalTC (-11) "*"     (qvarexp 0 ⊔ qvarexp 1)
                                        [(Covariant,     Qa, False),
                                         (Covariant,     Qa, False)]
tcRowEnd     = internalTC (-12) "rowend"
tcVariant    = internalTC (-13) "variant" (qvarexp 0)
                                          [(Covariant, Qa, False)]
tcRecord     = internalTC (-14) "record"  (qvarexp 1)
                                          [(QCovariant, Qa, False),
                                           (Covariant, Qa, False)]
tcRowMap     = internalTC (-15) "rowmap#"  (qvarexp 0 ⊔ qvarexp 1)
                                           [(Covariant, Qa, False),
                                           (Invariant, Qa, False)]
tcRowDots    = internalTC (-16) "rowdots#" (qvarexp 0)
                                           [(Covariant, Qa, True)]
tcRowHole    = internalTC (-17) "rowhole#" (qvarexp 0)
                                           [(Covariant, Qa, True)]

-- Types for testing

tcCycle, tcConst, tcIdent, tcConsTup, tcOption, tcIdfun ∷ TyCon
tcCycle      = internalTC (-51) "cycle" [(Invariant,     Qa, True)]
tcConst      = internalTC (-52) "const" [(Omnivariant, Qa, False)]
                 [([TpVar Nope], tyUnit)]
tcIdent      = internalTC (-53) "ident" (qvarexp 0)
                                        [(Covariant, Qa, False)]
                 [([TpVar Nope], TyVar (Bound 0 0 Nope))]
tcConsTup    = internalTC (-54) "cons"  (qvarexp 0 ⊔ qvarexp 1)
                                        [(Covariant, Qa, False),
                                         (Covariant, Qa, False)]
                 [([TpVar Nope, TpApp tcTuple [TpVar Nope, TpVar Nope]],
                   TyApp tcTuple [TyApp tcConsTup [TyVar (Bound 0 0 Nope),
                                                   TyVar (Bound 0 1 Nope)],
                                  TyVar (Bound 0 2 Nope)]),
                  ([TpVar Nope, TpVar Nope],
                   TyApp tcTuple [TyVar (Bound 0 0 Nope),
                                  TyVar (Bound 0 1 Nope)])]
tcOption     = internalTC (-55) "option" (qvarexp 0)
                                         [(Covariant, Qa, False)]
                 (Env.fromList [(AST.ident "None" ∷ ConId, Nothing),
                                (AST.ident "Some", Just (bvTy 0 0 Nope))])
tcIdfun      = internalTC (-55) "idfun" [(Invariant, Qa, False)]
                 (Env.fromList [(AST.ident "Mono" ∷ ConId,
                                 Just (bvTy 0 0 Nope .->. bvTy 0 0 Nope)),
                                (AST.ident "Poly",
                                 Just (TyQu Forall [(Nope, Qa)]
                                        (bvTy 0 0 Nope .->. bvTy 0 0 Nope)))])

tcSessOne, tcSessSend, tcSessRecv, tcSessSemi, tcSessDual ∷ TyCon
tcSessOne        = internalTC (-56) "1"
tcSessSend       = internalTC (-57) "!" [(-1, Qa, False)]
tcSessRecv       = internalTC (-58) "?" [(1, Qa, False)]
tcSessSemi       = internalTC (-59) ";" [(1, Qu, False), (1, Qu, True)]
tcSessDual       = internalTC (-60) "dual" [(-1, Qu, False)]
     [([TpApp tcSessOne []],
       TyApp tcSessOne []),
      ([TpApp tcSessSemi [TpApp tcSessSend [TpVar Nope], TpVar Nope]],
       TyApp tcSessSemi [TyApp tcSessRecv [TyVar (Bound 0 0 Nope)],
                         TyApp tcSessDual [TyVar (Bound 0 1 Nope)]]),
      ([TpApp tcSessSemi [TpApp tcSessRecv [TpVar Nope], TpVar Nope]],
       TyApp tcSessSemi [TyApp tcSessSend [TyVar (Bound 0 0 Nope)],
                         TyApp tcSessDual [TyVar (Bound 0 1 Nope)]])]

---
--- Convenience constructors
---

-- | Make a free type variable into a type
fvTy ∷ tv → Type tv
fvTy = TyVar . Free

-- | Make a bound type variable type
bvTy ∷ Optional f ⇒ Int → Int → f String → Type tv
bvTy i j n = TyVar (Bound i j (foldOpt Nope Here n))

-- | Project a free type variable from a 'TyVar'
fromFreeTV ∷ TyVar tv → tv
fromFreeTV (Free r)     = r
fromFreeTV _            = throw $
  almsBug StaticsPhase "fromFreeTV" "Got bound type variable"

-- | Make a type from a nullary type constructor
tyNulOp ∷ TyCon → Type tv
tyNulOp tc = TyApp tc []

-- | Make a type from a unary type constructor
tyUnOp ∷ TyCon → Type tv → Type tv
tyUnOp tc t1 = TyApp tc [t1]

-- | Make a type from a binary type constructor
tyBinOp ∷ TyCon → Type tv → Type tv → Type tv
tyBinOp tc t1 t2 = TyApp tc [t1, t2]

-- | A function type
tyFun ∷ Qualifier qe tv ⇒ Type tv → qe → Type tv → Type tv
tyFun t1 qe t2 = TyApp tcFun [t1, qualToType qe, t2]

-- | Constructor for unlimited arrow types
tyArr ∷ Type tv → Type tv → Type tv
tyArr = tyFun <-> Qu

-- | Constructor for affine arrow types
tyLol ∷ Type tv → Type tv → Type tv
tyLol = tyFun <-> Qa

-- | Type from a 'QLit'
tyQLit ∷ QLit → Type tv
tyQLit Qa = tyAf
tyQLit Qu = tyUn

-- | Binary types
tyTuple, tyRowMap, tyRecord ∷ Type tv → Type tv → Type tv

tyTuple  = tyBinOp tcTuple
tyRowMap = tyBinOp tcRowMap
tyRecord = tyBinOp tcRecord

-- | Nullary types
tyAf, tyUn, tyUnit, tyInt, tyChar, tyFloat, tyString, tyExn,
  tyRowEnd, tyRowHole ∷ Type tv

tyAf     = tyNulOp tcAf
tyUn     = tyNulOp tcUn
tyUnit   = tyNulOp tcUnit
tyInt    = tyNulOp tcInt
tyChar   = tyNulOp tcChar
tyFloat  = tyNulOp tcFloat
tyString = tyNulOp tcString
tyExn    = tyNulOp tcExn
tyRowEnd = tyNulOp tcRowEnd
tyRowHole= tyNulOp tcRowHole

(.*.), (.->.), (.-*.) ∷ Type tv → Type tv → Type tv
(.*.)    = tyTuple
(.->.)   = tyArr
(.-*.)   = tyLol

infixr 6 .->., .-*., `tyArr`, `tyLol`
infixl 7 .*., `tyTuple`

---
--- Qualifiers
---

instance Ord tv ⇒ Lattice (QExp tv) where
  QeA     ⊔ _        = QeA
  _       ⊔ QeA      = QeA
  QeU tvs ⊔ QeU tvs' = QeU (tvs `S.union` tvs')
  --
  QeA     ⊓ qe'      = qe'
  qe      ⊓ QeA      = qe
  QeU tvs ⊓ QeU tvs' = QeU (tvs `S.intersection` tvs')
  --
  _       ⊑ QeA      = True
  QeA     ⊑ _        = False
  QeU tvs ⊑ QeU tvs' = tvs `S.isSubsetOf` tvs'

instance Bounded (QExp tv) where
  minBound = QeU S.empty
  maxBound = QeA

class Qualifier q tv | q → tv where
  qualToType     ∷ q → Type tv
  qualifierEnv   ∷ Ord tv ⇒ [[QLit]] → q → QExpV tv
  qualifier      ∷ Ord tv ⇒ q → QExpV tv
  qualifierEnv   = const qualifier
  qualifier      = qualifierEnv []

instance Qualifier q tv ⇒ Qualifier (Maybe q) tv where
  qualToType   = maybe tyUn qualToType
  qualifierEnv = maybe minBound . qualifierEnv

instance (Ord tv, Qualifier q tv) ⇒ Qualifier [q] tv where
  qualToType   = qualToType . qualifier
  qualifierEnv = bigJoin <$$> map . qualifierEnv

instance Qualifier QLit tv where
  qualToType Qa     = tyAf
  qualToType Qu     = tyUn
  qualifier Qa      = QeA
  qualifier Qu      = QeU S.empty

instance Qualifier AST.Occurrence tv where
  qualToType = qualToType . AST.occToQLit
  qualifier  = qualifier . AST.occToQLit

instance Ord tv ⇒ Qualifier (Type tv) tv where
  qualToType        = qualToType . qualifier
  qualifierEnv env0 = foldTypeEnv (Left <$$> env0)
                                  fquant fbvar ffvar fcon frow frec
    where
    fquant ∷ Quant → [(Name, QLit)] →
             ([Either QLit QLit] → (QExpV tv → QExpV tv) → a) → a
    frec   ∷ Name → (Either QLit QLit → (QExpV tv → QExpV tv) → a) → a
    fquant Forall αs k     = k (Right Qu <$ αs) bumpQExp
    fquant Exists αs k     = k (Right . snd <$> αs) bumpQExp
    fbvar _ _    (Just (Right ql)) = qlitexp ql
    fbvar _ _    (Just (Left Qu))  = qlitexp Qu
    fbvar (i,j) n _                = qvarexp (Bound i j n)
    ffvar                  = qvarexp . Free
    fcon tc qes            = extractQual (tcQual tc) qes
    frow _ qe1 qe2         = qe1 ⊔ qe2
    frec _ k               = k (Right Qu) bumpQExp
    --
    bumpQExp QeA           = QeA
    bumpQExp (QeU tvs)     = QeU (S.map (bumpVar (-1)) tvs)
    bumpVar _ (Free r)     = Free r
    bumpVar k (Bound i j n)= Bound (i + k) j n

instance Qualifier (QExpV tv) tv where
  qualToType QeA       = TyApp tcAf []
  qualToType (QeU tvs)
    | S.null tvs       = TyApp tcUn []
    | otherwise        = foldr1 (\t1 t2 → TyApp tcJoin [t1, t2])
                                (TyVar <$> S.toList tvs)
  qualifier = id

instance Qualifier (S.Set tv) tv where
  qualifier αs   = QeU (S.mapMonotonic Free αs)
  qualToType αs  = qualToType (QeU (S.mapMonotonic Free αs))

-- | Make a qualifier expression from a single literal
qlitexp ∷ QLit → QExp tv
qlitexp Qa = QeA
qlitexp Qu = QeU S.empty

-- | Make a qualifier expression from a single type variable
qvarexp ∷ tv → QExp tv
qvarexp = QeU . S.singleton

-- | Build a qualifier from a list of qualifiers using an
--   integer-numbered qualifier.
extractQual ∷ Ord tv ⇒ QExp Int → [QExp tv] → QExp tv
extractQual QeA      _   = QeA
extractQual (QeU zs) qes = bigJoin (fst <$> filter ((`elem` zs) . snd)
                                                   (zip qes [0 ..]))

-- | Lift a free-variable q-expression to a 'QExpV'
liftVQExp ∷ QExp tv → QExpV tv
liftVQExp QeA           = QeA
liftVQExp (QeU αs)      = QeU (S.mapMonotonic Free αs)

-- | Modify the set of a 'QeU' 'QExp"
mapQExp ∷ (S.Set tv → S.Set tv') → QExp tv → QExp tv'
mapQExp _ QeA      = QeA
mapQExp f (QeU αs) = QeU (f αs)

---
--- Folds and unfolds
---

foldTypeEnv
         ∷ Ord tv ⇒
           -- | Initial environment
           [[s]] →
           -- | For quantifiers
           (∀a. Quant → [(Name, QLit)] → ([s] → (r → r) → a) → a) →
           -- | For bound variables
           ((Int, Int) → Name → Maybe s → r) →
           -- | For free variables
           (tv → r) →
           -- | For constructor applications
           (TyCon → [r] → r) →
           -- | For row type labels
           (RowLabel → r → r → r) →
           -- | For recursive types
           (∀a. Name → (s → (r → r) → a) → a) →
           -- | Type to fold
           Type tv →
           r
foldTypeEnv env0 fquant fbvar ffvar fcon frow frec σ0 =
  runReader (loop σ0) env0
  where
  loop (TyQu q αs σ)            =
    fquant q αs $ \ss f → f `liftM` local (ss:) (loop σ)
  loop (TyVar (Bound i j n))    = do
    env ← ask
    return (fbvar (i, j) n (look i j env))
  loop (TyVar (Free v))         = return (ffvar v)
  loop (TyApp tc ts)            =
    fcon tc <$> sequence
      [ if isQVariance v
          then loop (qualToType t)
          else loop t
      | t ← ts
      | v ← tcArity tc ]
  loop (TyRow n t1 t2)          =
    frow n `liftM` loop t1 `ap` loop t2
  loop (TyMu n t)               =
    frec n (\s f → f `liftM` local ([s]:) (loop t))
  --
  look i j env
    | rib:_ ← drop i env
    , elt:_ ← drop j rib = Just elt
  look _ _ _             = Nothing

foldType ∷ Ord tv ⇒
           -- | For quantifiers
           (∀a. Quant → [(Name, QLit)] → ([s] → (r → r) → a) → a) →
           -- | For bound variables
           ((Int, Int) → Name → Maybe s → r) →
           -- | For free variables
           (tv → r) →
           -- | For constructor applications
           (TyCon → [r] → r) →
           -- | For row type labels
           (RowLabel → r → r → r) →
           -- | For recursive types
           (∀a. Name → (s → (r → r) → a) → a) →
           -- | Type to fold
           Type tv →
           r
foldType = foldTypeEnv []

-- | Helper for constructing bound variable case for 'foldType'
mkBvF   ∷ (Int → Int → Name → r) →
          (Int, Int) → Name → a → r
mkBvF f (i, j) pn _ = f i j pn

-- | Helper for constructing quantifier case for 'foldType'
mkQuF
  ∷ (Quant → [(Name, QLit)] → r → s) →
    (∀a. Quant → [(Name, QLit)] → ([(Int, Int)] → (r → s) → a) → a)
mkQuF f q αs k = k [ (0, j) | j ← [0 .. length αs - 1] ] (f q αs)

-- | Helper for constructing recursive case for 'foldType'
mkMuF ∷ (Name → r → s) →
        (∀a. Name → ((Int, Int) → (r → s) → a) → a)
mkMuF f pn k = k (0, 0) (f pn)

foldTypeM ∷ (Monad m, Ord tv) ⇒
            -- | For quantifiers
            (∀a. Quant → [(Name, QLit)] → ([s] → (r → m r) → a) → a) →
            -- | For bound variables
            ((Int, Int) → Name → Maybe s → m r) →
            -- | For free variables
            (tv → m r) →
            -- | For constructor applications
            (TyCon → [r] → m r) →
            -- | For row type labels
            (RowLabel → r → r → m r) →
            -- | For recursive types
            (∀a. Name → (s → (r → m r) → a) → a) →
            -- | Type to fold
            Type tv →
            m r
foldTypeM fquant fbvar ffvar fapp frow frec =
  foldType (\qu ns k → fquant qu ns (\s k' → k s (>>= k')))
           fbvar
           ffvar
           (\tc mrs → sequence mrs >>= fapp tc)
           (\lab mr1 mr2 → mr1 >>= \r1 → mr2 >>= frow lab r1)
           (\n k → frec n (\s k' → k s (>>= k')))

--
-- Other unfolds
--

-- To strip off as many of the specified quantifier as possible,
-- building a qualifier bound environment for the layers.
unfoldQu ∷ Quant → Type tv → ([[QLit]], Type tv)
unfoldQu u0 = first reverse . loop where
  loop (TyQu u tvs t)
    | u0 == u || lcTyK 0 t = first (map snd tvs:) (loop t)
  loop t                   = ([], t)

-- To find the labels and fields of a row type, and the extension,
-- in standard order
unfoldRow ∷ Type tv → ([(RowLabel, Type tv)], Type tv)
unfoldRow = first (List.sortBy (compare <$> fst <$.> fst)) . loop where
  loop (TyRow n t1 t2) = first ((n, t1):) (loop t2)
  loop t               = ([], t)

-- Unfold leading μ (recursive type) binders.
unfoldMu ∷ Type tv → ([Name], Type tv)
unfoldMu (TyMu pn t) = first (pn:) (unfoldMu t)
unfoldMu t           = ([], t)

---
--- Row operations
---

-- Construct a row from a list of label/type pairs and a tail type.
foldRow ∷ [(RowLabel, Type a)] → Type a → Type a
foldRow = flip (foldr (uncurry TyRow))

-- Sort a row by its labels
sortRow ∷ Type a → Type a
sortRow = uncurry foldRow . unfoldRow

---
--- Type standardization
---

-- | @standardize@ puts a type in standard form.
--   A type is in standard form if three conditions are met:
--    
--   * All bound type variables actually appear in their scope.  That
--     is, ‘∀ α β γ. α → γ’ is not standard, but ‘∀ α γ. α → γ’ is.
--
--   * The same quantifier never nests directly inside itself.  That is,
--     ‘∀ α β. ∀ γ. C α β γ’ is not standard, but ‘∀ α β γ. C α β γ’ is.
--
--   * The bound type variables of each quantifier are listed in the
--     order that they appear in its scope.  That is,
--     ‘∀ α β γ. C α γ β’ is not standard, but ‘∀ α β γ. C α β γ’ is.
--
--   * Type variables bound by μ appear in their scope, and there are
--     never multiple, immediately nested μs.
--
--  Type standardization is necessary as a post-pass after parsing,
--  because it's difficult to parse into standard form directly.
standardizeType  ∷ Ord tv ⇒ Type tv → Type tv
standardizeType  = standardizeQuals M.empty

-- | Used in the definition of 'standardizeQuals' below.
type StdizeEnv s = [[(Int, STRef s [((Int, Int), (Name, QLit))], Bool, QLit)]]

-- | Standardize a type while cleaning up qualifiers.
standardizeQuals ∷ ∀tv. Ord tv ⇒ M.Map tv QLit → Type tv → Type tv
standardizeQuals qm t00 = runST (loop 0 [] t00) where
  loop ∷ ∀s. Int → StdizeEnv s → Type tv → ST s (Type tv)
  loop depth g t0 = case t0 of
    TyQu u _ _ → do
      rn ← newRef []
      let (qls, t) = unfoldQu u t0
          i        = length qls
          g'       = (depth + i, rn, False,) <$$> qls
      t' ← loop (depth + i) (g' ++ g) t
      nl ← readRef rn
      return $ case nl of
        [] → openTyN i (-1) [] t'
        _  → TyQu u [ n | (_,n) ← nl ] (openTyN (i - 1) (i - 1) [] t')
    TyApp tc ts          → TyApp tc <$> sequence
      [ if isQVariance v
          then doQual depth g t
          else loop depth g t
      | t ← ts
      | v ← tcArity tc ]
    TyVar v               → TyVar . fst <$> doVar depth g (const True) v
    TyRow _ _ _           → do
      let (row, ext) = unfoldRow t0
      row' ← sequence
        [ (ni,) <$> loop depth g ti
        | (ni, ti) ← row ]
      ext' ← loop depth g ext
      return (foldRow row' ext')
    TyMu pn _            → do
      rn ← newRef []
      let (pns, t) = unfoldMu t0
          i        = length pns
          g'       = (depth + i, rn, True,) <$$> replicate i [Qa]
      t' ← loop (depth + i) (g' ++ g) t
      nl ← readRef rn
      return $
        if null nl
          then openTyN i (-1) [] t'
          else TyMu pn (openTyN (i - 1) (i - 1) [] t')
  --
  doVar ∷ ∀s. Int → StdizeEnv s →
              (QLit → Bool) → TyVar tv → ST s (TyVar tv, Bool)
  doVar depth g keep v0 = case v0 of
    Bound i j n
      | rib:_                    ← drop i g
      , (olddepth, r, rec, ql):_ ← drop j rib
                          → do
        s  ← readRef r
        if rec
          then do
            case List.findIndex ((== (depth - i)) . fst . fst) s of
              Just _  → return ()
              Nothing → writeRef r (s ++ [((depth - i, 0), (n, ql))])
            return (Bound (depth - olddepth) 0 n, True)
          else do
            j' ← case List.findIndex ((== (depth - i, j)) . fst) s of
              Just j' → return j'
              Nothing → do
                when (keep ql) $
                  writeRef r (s ++ [((depth - i, j), (n, ql))])
                return (length s)
            return (Bound (depth - olddepth) j' n, keep ql)
      | otherwise   → return (v0, True)
    Free r       → return (Free r,
                              keep (M.findWithDefault maxBound r qm))
  --
  doQual ∷ ∀s. Ord tv ⇒ Int → StdizeEnv s → Type tv → ST s (Type tv)
  doQual depth g t =
    qualToType <$> case qualifier t of
      QeA     → return QeA
      QeU tvs → do
        tvbs' ← mapM (doVar depth g (== Qa)) (S.toList tvs)
        return (QeU (S.fromList (fst <$> filter snd tvbs')))

---
--- Locally-nameless operations
---

-- | @openTy k τs τ@ substitutes @τs@ for the bound type variables at
--   rib level @k@.  DeBruijn indices higher than @k@ are adjusted downward,
--   since opening a type peels off a quantifier.
openTy ∷ Int → [Type a] → Type a → Type a
openTy  = openTyN 1

-- | Generalization of 'openTy': the first argument specifies how much
--   to adjust indices that exceed @k@.
openTyN ∷ Int → Int → [Type a] → Type a → Type a
openTyN n k vs σ0 = case σ0 of
  TyQu u e σ       → TyQu u e (next σ)
  TyVar v          → openTV_N n k vs v
  TyApp name σs    → TyApp name (map this σs)
  TyRow name σ1 σ2 → TyRow name (this σ1) (this σ2)
  TyMu name σ      → TyMu name (next σ)
  where
    this = openTyN n k vs
    next = openTyN n (k + 1) vs

openTV_N ∷ Int → Int → [Type a] → TyVar a → Type a
openTV_N n k vs (Bound i j name)
  | i > k      = TyVar (Bound (i - n) j name)
  | i == k, Just σ ← listNth j vs
              = σ
  | otherwise = TyVar (Bound i j name)
openTV_N _ _ _  (Free v) = TyVar (Free v)

-- | @closeTy k αs τ@ finds the free variables @αs@ and replaces them
--   with bound variables at rib level @k@.  The position of each type
--   variable in @αs@ gives the index of each bound variable into the
--   new rib.
closeTy ∷ Eq a ⇒ Int → [a] → Type a → Type a
closeTy k vs σ0 = case σ0 of
  TyQu u e σ   → TyQu u e (next σ)
  TyVar (Bound i j n)
    | i >= k    → TyVar (Bound (i + 1) j n)
    | otherwise → TyVar (Bound i j n)
  TyVar (Free v)
    | Just j ← List.findIndex (== v) vs
                → TyVar (Bound k j Nope)
    | otherwise → TyVar (Free v)
  TyApp n σs    → TyApp n (map this σs)
  TyRow n σ1 σ2 → TyRow n (this σ1) (this σ2)
  TyMu n σ     → TyMu n (next σ)
  where
    this = closeTy k vs
    next = closeTy (k + 1) vs

-- | Build a recursive type by closing and binding the given variable
closeRec ∷ Ord tv ⇒ tv → Type tv → Type tv
closeRec α σ = standardizeType (TyMu Nope (closeTy 0 [α] σ))

-- | Add the given quantifier while binding the given list of variables
closeQuant ∷ Ord tv ⇒ Quant → [(tv, QLit)] → Type tv → Type tv
closeQuant qu αqs ρ = standardizeType (TyQu qu nqs (closeTy 0 αs ρ))
  where
    αs  = fst <$> αqs
    nqs = zip (repeat Nope) (snd <$> αqs)

-- | Is the given type locally closed to level k?  A type is locally closed
--   if none of its bound variables point to quantifiers "outside" the
--   type.
--
--   ASSUMPTION: No bound variables are lurking behind an apparent free
--   variable, because @lcTy@ doesn't attempt to dereference free
--   variables.  This should be an invariant, because it would come
--   about only as a result of a capturing substitution.
lcTy ∷ Int → Type a → Bool
lcTy  = loop where
  loop k (TyQu _ _ t)          = loop (k + 1) t
  loop k (TyVar (Bound i _ _)) = k > i
  loop _ (TyVar (Free _))      = True
  loop k (TyApp _ ts)          = all (loop k) ts
  loop k (TyRow _ t1 t2)       = loop k t1 && loop k t2
  loop k (TyMu _ t)            = loop (k + 1) t

-- | Are there no bound vars of level k?
lcTyK ∷ Int → Type tv → Bool
lcTyK  = loop where
  loop k (TyQu _ _ t)            = loop (k + 1) t
  loop k (TyVar (Bound i _ _)) = k /= i
  loop _ (TyVar (Free _))      = True
  loop k (TyApp _ ts)             = all (loop k) ts
  loop k (TyRow _ t1 t2)          = loop k t1 && loop k t2
  loop k (TyMu _ t)              = loop (k + 1) t

---
--- TyCon Varieties
---

data TyConVariety
  = AbstractType
  | DataType
  | OperatorType
  deriving (Eq, Ord)

-- | Find out the variety of a type constructor
varietyOf ∷ TyCon → TyConVariety
varietyOf tc
  | isJust (tcNext tc)          = OperatorType
  | Env.isEmpty (tcCons tc)     = AbstractType
  | otherwise                   = DataType