Haskell doodle (dependently typed lambda calculus, very incomplete)

Hal.hs

-- https://www.youtube.com/watch?v=AT4JJm_ujRg
-- https://en.wikiversity.org/wiki/Foundations_of_Functional_Programming/Pure_type_systems

module Hal where

import Control.Monad
import Data.Set

type Name = String

data Expr
  = Var Name
  | Lam Name Type Expr
  | Pi Name Type Type
  | App Expr Expr
  | Type
  deriving (Eq, Show)

type Type = Expr

free :: Expr -> Set Name
free (Var x)     = singleton x
free (Lam x t y) = free t `union` delete x (free y)
free (Pi x t y)  = free t `union` delete x (free y)
free (App x y)   = free x `union` free y
free Type        = empty

check :: [(Name, Expr)] -> Expr -> Maybe Type
check env (Var x) = lookup x env
check env (Lam x t y) = do
  ty <- check ((x, t):env) y
  return $ Pi x t ty
check env (Pi x t y) = do
  t' <- check env t
  guard $ t' == Type
  ty <- check ((x, Type):env) y
  guard $ ty == Type
  return Type
check env (App x y) = do
  tx <- check env x
  ty <- check env y
  case tx of
    Pi x' t y' -> do
      guard $ t == ty
      return $ substitute x' y y'
    _ -> Nothing
check _ Type = return $ Type

substitute :: Name -> Expr -> Expr -> Expr
substitute = undefined