compiler icon indicating copy to clipboard operation
compiler copied to clipboard

Constrained type variables in type aliases aren't respected

Open baffalop opened this issue 4 years ago • 1 comments

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.

baffalop avatar Sep 15 '21 13:09 baffalop

Thanks for reporting this! To set expectations:

  • Issues are reviewed in batches, so it can take some time to get a response.
  • Ask questions in a community forum. You will get an answer quicker that way!
  • If you experience something similar, open a new issue. We like duplicates.

Finally, please be patient with the core team. They are trying their best with limited resources.

github-actions[bot] avatar Sep 15 '21 13:09 github-actions[bot]