Opened 4 years ago

Last modified 10 months ago

#11503 new bug

TypeError woes (incl. pattern match checker)

Reported by: goldfire Owned by:
Priority: normal Milestone: 8.10.1
Component: Compiler Version: 8.1
Keywords: PatternMatchWarnings, CustomTypeErrors Cc: dfeuer
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: Incorrect error/warning at compile-time Test Case:
Blocked By: Blocking:
Related Tickets: #14141, #16377 Differential Rev(s):
Wiki Page:

Description

When I say

{-# LANGUAGE DataKinds, GADTs, KindSignatures, TypeFamilies,
             UndecidableInstances #-}
{-# OPTIONS_GHC -fwarn-incomplete-patterns #-}

module Bug where

import GHC.TypeLits
import GHC.Exts ( Constraint )

type family NotInt a where
  NotInt Int = TypeError (Text "That's Int, silly.")
  NotInt _   = (() :: Constraint)

data T a where
  MkT1 :: a -> T a
  MkT2 :: NotInt a => T a

foo :: T Int -> Int
foo (MkT1 x) = x

I get

Bug.hs:19:1: warning:
    Pattern match(es) are non-exhaustive
    In an equation for ‘foo’: Patterns not matched: MkT2

But I shouldn't.

Even worse, perhaps, GHC accepts my pattern-match against MkT2 if I add it. If I change the TypeError to False ~ True, I get the correct behavior.

Change History (8)

comment:1 Changed 4 years ago by simonpj

Keywords: PatternMatchWarnings added

I think you are saying that

type family NotInt a where
  NotInt Int = False ~ True
  NotInt _   = (() :: Constraint)

makes everything work. That's because the pattern-match warning infrastructure treats False ~ True as definitely insoluble.

But apparently it doesn't treat TypeErorr blah as definitely insoluble. That's because when we solve [G] NotInt Int, we get [G] TypeError ... ~ fsk, [G] fsk, and neither is treated as insoluble.

I'm sure this can be dealt with, but it'll need a little care.

comment:2 Changed 2 years ago by RyanGlScott

Keywords: CustomTypeErrors added

comment:3 Changed 2 years ago by dfeuer

I ran into this issue a few days ago, and it really is annoying. We're forced to choose between a constraint the pattern checker will work with properly ('True ~ 'False) and a constraint that will give a good error message when accidentally matching against MkT2 (TypeError ...). There's a sort of workaround, but it's really horrible: instead of 'True ~ 'False, use something like "" ~ "This is an error message!".

comment:4 Changed 2 years ago by dfeuer

Cc: dfeuer added
Milestone: 8.6.1
Type of failure: None/UnknownIncorrect error/warning at compile-time

comment:5 Changed 2 years ago by dfeuer

Simon, I imagine there's a broad reason somewhere for

[G] c ~ fsk, [G] fsk

not to be simplified to

[G] c

Assuming that's the case I suspect maybe we should track known insoluble constraints the way we track known-bottoming expressions. Since TypeError ... ~ fsk and TypeError ... is insoluble, we could conclude that fsk is insoluble.

comment:6 Changed 18 months ago by bgamari

Milestone: 8.6.18.8.1

These won't be fixed for 8.6, bumping to 8.8.

comment:7 Changed 12 months ago by osa1

Milestone: 8.8.18.10.1

Bumping milestones of low-priority tickets.

comment:8 Changed 10 months ago by RyanGlScott

Note: See TracTickets for help on using tickets.