amuletml / amulet

An ML-like functional programming language
https://amulet.works/
BSD 3-Clause "New" or "Revised" License
324 stars 14 forks source link

Mitigate exponential behaviour of inhabitance checker #296

Closed SquidDev closed 3 years ago

SquidDev commented 3 years ago

This adds a simpler version of the inhabitance checker in pmcheck. Unlike pmcheck's, this does not use any contextual information, which means it can be memoized.

There are some cases where the exponential behaviour is still present. For instance, consider the chain of sum types:

type t1 'a = T1 of 'a
type t2 'a 'b = T1L of (t1 'a) | T1R of (t1 'a)
type t3 'a 'b = T3L of (t2 'a) | T3R of (t2 'a)
(* ... *)

We cannot statically tell if tn is inhabited for any type variable. I guess we could compile this to a predicate based on the type variables, but that may be going a bit far :).

Fixes #294