#!/usr/bin/env stack
-- stack script --resolver ghc-9.14.1 --package base
{-# LANGUAGE GHC2024 #-}

-- Two types: ints and functions
data Ty =
    TyInt
  | TyFun Ty Ty
  deriving stock (Show)

-- Our first attempt at an expression datatype:
-- vars, ints, addition, and lambdas
data Exp0 =
    ExpVar0 String
  | ExpInt0 Int
  | ExpPlus0 Exp0 Exp0
  | ExpLam0 String (Maybe Ty) Exp0
  -- Lambdas may have argument types
  deriving stock (Show)

-- We choose as many phases as we want:
-- Each phase determines a concrete variant
-- of our expression type.
data Phase = Parse | Infer
  deriving stock (Show)

-- After parsing, lambdas MAY have argument types.
-- After type inference, they MUST.
data ArgTy (p :: Phase) where
  ArgTyParse :: Maybe Ty -> ArgTy Parse
  ArgTyInfer :: Ty -> ArgTy Infer

-- GADTs require standalone deriving for this
deriving stock instance Show (ArgTy p)

-- Our final expression type is indexed by Phase.
-- The phase controls which constructors of
-- ArgTy are allowed.
data Exp (p :: Phase) =
    ExpVar String
  | ExpInt Int
  | ExpPlus (Exp p) (Exp p)
  | ExpLam String (ArgTy p) (Exp p)
  deriving stock (Show)

-- Compilation phases are reflected in
-- expression types. (Impls omitted below)

parseExp :: String -> Maybe (Exp Parse)
parseExp = const Nothing

inferTypes :: Exp Parse -> Maybe (Exp Infer)
inferTypes = const Nothing