Opened 2 years ago

Last modified 2 years ago

#14141 new bug

Custom type errors don't trigger when matching on a GADT constructor with an error in the constraint

Reported by: Darwin226 Owned by:
Priority: normal Milestone:
Component: Compiler (Type checker) Version: 8.0.2
Keywords: CustomTypeErrors Cc:
Operating System: Unknown/Multiple Architecture: x86_64 (amd64)
Type of failure: GHC accepts invalid program Test Case:
Blocked By: Blocking:
Related Tickets: #11503 Differential Rev(s):
Wiki Page:

Description

The following code fails to compile (as it should)

data D where
    A :: C => D

type family C :: Constraint where
    C = 'True ~ 'False

f :: D -> ()
f A = ()

with the error "Couldn't match type 'True with 'False".

This code, however, does compile without an issue:

data D where
    A :: C => D

type family C :: Constraint where
    C = TypeError ('Text "error")

f :: D -> ()
f A = ()

I feel that this is a bug.

Change History (3)

comment:1 Changed 2 years ago by Darwin226

Keywords: CustomTypeErrors added

comment:2 Changed 2 years ago by Phyx-

Component: CompilerCompiler (Type checker)
Operating System: WindowsUnknown/Multiple

Thanks for the report, reclassifying it as this isn't a Windows specific error and I'm not too familiar with this feature.

comment:3 Changed 2 years ago by RyanGlScott

I think this ticket is #11503 in disguise (or at least shares a symptom with it).

Note: See TracTickets for help on using tickets.