Type checking a phantom type succeeds when it should not

[joneshf]

Might be a duplicate, but I couldn't find a similar example.

With the following example, broken should not type check because (OnePlus m, m) is not the same type as (m, m). However, the compiler gives it a type of a.

I am not sure how to make this example smaller, but there's probably a way to do so.

OS: Linux 4.7.2-1-ARCH #1 SMP PREEMPT Sat Aug 20 23:02:56 CEST 2016 x86_64 GNU/Linux
Browser: Chromium Version 53.0.2785.101 (64-bit)
Elm: 0.17.1

module Vect exposing (..)

type OnePlus m
    = OnePlus

type Vect m a
    = Vect (List a)

nil : Vect ( m, m ) a
nil =
    Vect []

head : Vect ( OnePlus m, m ) a -> a
head (Vect xs) =
    Maybe.withDefault (Debug.crash "") (List.head xs)

broken =
    head nil

[process-bot]

Thanks for the issue! Make sure it satisfies this checklist. My human colleagues will appreciate it!

Here is what to expect next, and if anyone wants to comment, keep these things in mind.

[JoeyEremondi]

I haven't looked at your example in detail, but you might be interested in
my Safe-Lists library:
http://package.elm-lang.org/packages/JoeyEremondi/safelist/latest
http://package.elm-lang.org/packages/JoeyEremondi/typenats/latest

On Fri, Sep 23, 2016 at 6:57 AM, Process Bot [email protected]
wrote:

Thanks for the issue! Make sure it satisfies this checklist
https://github.com/process-bot/contribution-checklist/blob/master/issues.md.
My human colleagues will appreciate it!

Here is what to expect next
https://github.com/process-bot/contribution-checklist/blob/master/expectations.md,
and if anyone wants to comment, keep these things
https://github.com/process-bot/contribution-checklist/blob/master/participation.md
in mind.

—
You are receiving this because you are subscribed to this thread.
Reply to this email directly, view it on GitHub
#1491 (comment),
or mute the thread
https://github.com/notifications/unsubscribe-auth/ACzn0mmoE2BzGOedkUrWZjq_VSP3QBISks5qs9rRgaJpZM4KFAgP
.

[joneshf]

I'm very interested :). We should discuss elsewhere though.