Constrained type variables in type aliases aren't respected

Quick Summary:

A type alias with a constrained type variable—like number, appendable, etc.—can have that variable bound to concrete type which violates the constraint, when used in an annotation. The same is technically true of custom types with a constrained type variable, though in practice this isn't such a problem because the inferred type of any values will have the constraint, resulting in a mismatch.

SSCCE

Type alias used in an annotation:

> type alias A appendable = { a : appendable }
> a : A Int
| a = { a = 0 }
|
{ a = 0 } : A Int

However, the constraint holds for the generated constructor:

> a = A 0
-- TYPE MISMATCH ---------------------------------------------------------- REPL

The 1st argument to `A` is not what I expect:

6| a = A 0
          ^
This argument is a number of type:

  number

But `A` needs the 1st argument to be:

  appendable

Hint: There are no values in Elm that are both a number and appendable.

Annotating a custom type in the same way causes a type mismatch with the inferred type of the value:

> type B appendable = With appendable | Without
> b : B Int
| b = With 0
|
-- TYPE MISMATCH ---------------------------------------------------------- REPL

The 1st argument to `With` is not what I expect:

8| b = With 0
            ^
This argument is a number of type:

   number

But `With` needs the 1st argument to be:

   appendable

Hint: There are no values in Elm that are both a number and appendable.

> b : B Int
| b = Without
|
-- TYPE MISMATCH ---------------------------------------------------------- REPL

Something is off with the body of the `b` definition:

8| b = Without
       ^^^^^^^
This `Without` value is a:

   B appendable

But the type annotation on `b` says it should be:

   B Int

Hint: I only know how to append strings and lists.

However, it's interesting to note that the compiler doesn't consider the annotation B Int problematic in itself:

> f : () -> B Int
| f () = Debug.todo "when ints are appendable"
|
<function> : () -> B Int

Elm: 0.19.1
Browser: N/A
Operating System: macOS 11.2.3

Additional Details

This issue was pointed out by @SiriusStarr on Slack. I did some probing in the REPL.

When researching this I learned that Haskell doesn't provide any way to express typeclass constraints with a type alias. Moreover, typeclass constraints can only be used on data with GADTs enabled. So I appreciate that maybe Elm is somewhat more advanced in this regard. But the type alias result is surprising and doesn't seem internally consistent.

elm / compiler

Constrained type variables in type aliases aren't respected #2225

SSCCE

Additional Details