// Disable warning about the same constructor for different types
@@warning("-30")

  | Unit // 1
  | Var(string) // α
  | Existential(string) // â
  | Polytype(string, typ) // ∀α.A
  | Arrow(typ, typ) // A -> B

  | TUnit // 1
  | TVar(string) // α
  | TExistential(string) // â
  | TPolytype(string, typ) // ∀α.A
  | TArrow(typ, typ) // A -> B

  | Unit // 1
  | Var(string) // α
  | Existential(string) // â
  | Arrow(monotyp, monotyp) // τ -> σ

  | MUnit // 1
  | MVar(string) // α
  | MExistential(string) // â
  | MArrow(monotyp, monotyp) // τ -> σ

  | TypeVar(string) // Ω,α
  | TermAnnot(string, typ) // Ω,x:A
  | ExistentialSolved(string, monotyp) // Ω,â=τ
  | Marker(string) // Ω,🢒â

  | CCTypeVar(string) // Ω,α
  | CCTermAnnot(string, typ) // Ω,x:A
  | CCExistentialSolved(string, monotyp) // Ω,â=τ
  | CCMarker(string) // Ω,🢒â

@@warning("+30")

let rec lookupTypeVariable = (ctx: list<contextEntry>, name: string): typ => {

let rec lookupTypeVariable = (ctx: list<contextEntry>, name: string): result<typ, string> => {

  | list{} => failwith("L")
  | list{TermAnnot(n, t), ..._} if n == name => t

  | list{} => Error(`could not find name ${name}`)
  | list{TermAnnot(n, t), ..._} if n == name => Ok(t)

  `${prefix}${Int.toString(num)}`

  `${prefix}${num->Int.toString}`

  | (Unit, Unit) => Ok(ctx)

  | (Unit, TUnit) => Ok(ctx)

  | (e, Polytype(x, tyA)) => failwith("TODO")

  | (e, TPolytype(x, tyA)) => failwith("TODO ∀I-rule")

  | (Lam(x, e), Arrow(tyA, tyB)) =>

  | (Lam(x, e), TArrow(tyA, tyB)) =>

  // TODO: Subtyping rule???
  | (Var(_) | Lam(_, _) | App(_, _) | Annot(_, _), _) => failwith("TODO")
  | _ => Error("could not resolve")

  | (_, _) =>
    let tyA = synthesize(ctx, term)
    let tyA' = applyContext(ctx, tyA)

  | Var(name) => Ok(lookupTypeVariable(ctx, name), ctx)

  | Var(name) => lookupTypeVariable(ctx, name)->Result.map(ty => (ty, ctx))

  | Unit => Ok(Unit, ctx)

  | Unit => Ok(TUnit, ctx)

    Ok(Arrow(Existential(exA), Existential(exB)), ctx)

    let augmentedCtx = list{TermAnnot(x, TVar(exA)), TypeVar(exB), TypeVar(exA), ...ctx}
    typecheck(augmentedCtx, e, TVar(exB))->Result.map(_ => (
      TArrow(TExistential(exA), TExistential(exB)),
      ctx,
    ))

  | App(e1, e2) => failwith("TODO")

  | App(e1, e2) => synthesize(ctx, e1)->Result.flatMap(((tyA, ctx)) => appSynthesize(ctx, tyA, e2))

  | (Arrow(tyA, tyC), e) => typecheck(ctx, e, tyA)->Result.map(_ => (tyC, ctx))

  | (TArrow(tyA, tyC), e) => typecheck(ctx, e, tyA)->Result.map(_ => (tyC, ctx))

  | (Polytype(a, tyA), e) => failwith("TODO")

  | (TPolytype(a, tyA), e) => failwith("TODO")

  | (Existential(_), _) => failwith("TODO")

  | (TExistential(_), _) => failwith("TODO")

  | (Unit | Var(_), _) => Error("trying to appSynthesize with a non-function type")

  | (TUnit | TVar(_), _) => Error("trying to appSynthesize with a non-function type")

let rec applyContext = (ctx: context, typ: typ): typ => {

and applyContext = (ctx: context, typ: typ): typ => {

  | Unit => Unit
  | Var(x) => Var(x)
  | Existential(_) => failwith("TODO")
  | Polytype(_) => failwith("TODO")
  | Arrow(a, b) => Arrow(applyContext(ctx, a), applyContext(ctx, b))

  | TUnit => TUnit
  | TVar(x) => TVar(x)
  | TExistential(_) => failwith("TODO")
  | TPolytype(_) => failwith("TODO")
  | TArrow(a, b) => TArrow(applyContext(ctx, a), applyContext(ctx, b))

    "res:dev": "rescript build -w"

    "res:dev": "rescript build -w",
    "test": "retest lib/**/*.mjs"

    "rescript": "^10.1.4"

    "@glennsl/bs-jest": "^0.7.0",
    "jest": "^29.7.0",
    "rescript": "^10.1.4",
    "rescript-js": "^1.0.0-beta.2",
    "rescript-test": "^5.0.0"

{
  "verbose": true,
  "moduleFileExtensions": ["js", "mjs"],
  "extensionsToTreatAsEsm": [".bs.mjs"],
  "testMatch": ["**/__tests__/**/*_test.mjs", "**/__tests__/**/*_test.bs.js"],
  "transform": {
    "^.+.m?js$": "babel-jest"
  },
  "transformIgnorePatterns": ["node_modules/(?!(rescript)/)"]
}

  "bsc-flags": [],

    {
      "dir": "src",
      "subdirs": true
    }

    { "dir": "src", "subdirs": true },
    { "dir": "__tests__", "subdirs": true, "type": "dev" }

      "module": "es6",

      "module": "commonjs",

  "bs-dependencies": []

  "bs-dependencies": [],
  "bs-dev-dependencies": ["@glennsl/bs-jest"]

= Expressions
- $ id : forall a. a arrow.r a $

module.exports = {
  presets: [
    [
      "@babel/preset-env",
      { targets: { node: "current", esmodules: false }, modules: "cjs" },
    ],
  ],
  plugins: [],
};

open Jest
open Belt
open Data
open Bidir
open Expect
open! Expect.Operators
let mapFirst = a => a->Result.map(((x, _)) => x)
test("id", () => {
  let id: term = Lam("x", Var("x"))
  let ctx = list{}
  let typ = synthesize(ctx, id)->mapFirst
  Js.Console.error2("output: ", typ)
  expect(typ) === Ok(TPolytype("ex0", TArrow(TVar("ex0"), TVar("ex0"))))
})

*.bs.mjs

lib/bs

lib/bs
__tests__/**/*.mjs
src/**/*.mjs