LAINTYPES: Good enough descriptive types for Common Lisp

I've created a repo for the package which implements an MVP of this system, using algorithms from the paper The Simple Essence of Algebraic Subtyping, specifically implementing Simple-Sub.

I also asked around on reddit for opinions and interest, seems that it would be a nice to have for many people.

Currently the main entrypoint is #'deftun which admits a function and immediately typechecks it, returning both it and a reified type specifier:

CL-USER> (in-package #:laintype)
#<PACKAGE "LAINTYPE">
LAINTYPE> (deftun foo (x) (+ x x))
FOO
(FUNCTION (NUMBER) NUMBER)

And it already checks for some things which the built-in SBCL inference won't handle. Take the type of identity for example. It is quite nondescript:

LAINTYPE> (deftun id (x) x)
ID
(FUNCTION (T) T)

(function (t) t) tells us nothing, yet even when id shadows the usage of a type, laintype still manages to figure out that a number is required:

LAINTYPE> (deftun idadd (x) (id (+ (id x) 1)))
IDADD
(FUNCTION (NUMBER) NUMBER)

While the SBCL description only knows about T:

LAINTYPE> (describe #'idadd)
#<FUNCTION IDADD>
  [compiled function]


Lambda-list: (X)
Derived type: (FUNCTION (T) *)

Ideally I think we'd have a system vaguely similar to Unison's lovely code manager:

LAINTYPE> (defun union (x) (if x 20 "a"))
UNION
; Types:
;	  union :: (α) -> (or string integer)

LAINTYPE> (defun foo (x) x)
FOO
; Types:
;	  foo :: (α) -> α

LAINTYPE> (defun bar () (foo 20))
BAR
; Types:
;	  bar :: () -> number

LAINTYPE> (defun foo (x) "A")
FOO
; Types:
;	  foo :: (α) -> string
;	  bar :: () -> string

LAINTYPE> (defun bar () (+ 1 (foo 20)))
BAR
; Types:
;	  bar :: !
; Culprits:
;	  in: DEFUN BAR
;
;	  type mismatch:
;		  The second argument to #'+ in:
;
;		  (+ 1 (foo 20))
;
;		  Requires a type with upper bound `number`,
;		  however `(foo 20)` has type `string`.

! stands for Fail i.e. "this does not typecheck"

Similar to Rust's usage such a function will never return in standard cases.

The type of bar is printed even when admitting foo because its type changes.

A function failing its typecheck is still admitted (perhaps unless an option is set), to preserve as much of standard CL behaviour as possible, we aim to be descriptive not prescriptive. The error will persist on screen until it is fixed by the programmer or hidden using some mechanism.

List of special forms that need to be handled, other symbols are either functions or macros. Thse can be input into the type database, and don't need their own cases in the code-walker.