Opened 4 months ago

Closed 4 months ago

Last modified 3 months ago

#14086 closed bug (fixed)

Empty case does not detect kinds

Reported by: dfeuer Owned by:
Priority: low Milestone: 8.4.1
Component: Compiler (Type checker) Version: 8.2.1
Keywords: TypeInType Cc: RyanGlScott
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: Incorrect error/warning at compile-time Test Case: pmcheck/should_compile/T14086
Blocked By: Blocking:
Related Tickets: Differential Rev(s): Phab:D3819
Wiki Page:

Description

{-# language TypeInType, EmptyCase #-}
module Silly where
import Data.Kind

f :: Type -> Int
f x = case x of

GHC warns

    Pattern match(es) are non-exhaustive
    In a case alternative: Patterns not matched: _ :: *

In fact, Type is only a type because of TypeInType. It has no actual values, so the empty case is exhaustive.

To be honest, I kind of wish GHC would give me a warning for doing something so silly as to even give a function an argument of type Type, but I imagine that might be hard.

Change History (6)

comment:1 Changed 4 months ago by RyanGlScott

Cc: RyanGlScott added

I'm somewhat surprised this doesn't work, given that Type expands to TYPE LiftedRep, and TYPE is itself a datatype with no constructors. Granted, it is a somewhat magical datatype, but perhaps that just means we need to adjust the magicks appropriately for the EmptyCase pattern-match exhaustivity checker's purposes.

comment:2 Changed 4 months ago by goldfire

Keywords: TypeInType added

comment:3 Changed 4 months ago by RyanGlScott

Differential Rev(s): Phab:D3819
Status: newpatch

comment:4 Changed 4 months ago by Ryan Scott <ryan.gl.scott@…>

In a267580/ghc:

Don't warn when empty casing on Type

Summary:
`Type` (a.k.a. `TYPE LiftedRep`) can be used at the type level thanks
to `TypeInType`. However, expressions like

```lang=haskell
f :: Type -> Int
f x = case x of {}
```

were falsely claiming that the empty case on the value of type `Type` was
non-exhaustive. The reason is a bit silly: `TYPE` is technically not an empty
datatype in GHC's eyes, since it's a builtin, primitive type. To convince the
pattern coverage checker otherwise, this adds a special case for `TYPE`.

Test Plan: make test TEST=T14086

Reviewers: gkaracha, austin, bgamari, goldfire

Reviewed By: goldfire

Subscribers: goldfire, rwbarton, thomie

GHC Trac Issues: #14086

Differential Revision: https://phabricator.haskell.org/D3819

comment:5 Changed 4 months ago by RyanGlScott

Resolution: fixed
Status: patchclosed
Test Case: pmcheck/should_compile/T14086

comment:6 Changed 3 months ago by Ryan Scott <ryan.gl.scott@…>

In 4f1f9868/ghc:

Change isClosedAlgType to be TYPE-aware, and rename it to pmIsClosedType

Summary:
In a267580e4ab37115dcc33f3b8a9af67b9364da12, I somewhat awkwardly
inserted a special case for `TYPE` in the `EmptyCase` coverage checker.
Instead of placing it there, @mpickering noted that `isClosedAlgType` would
be a better fit for it. I do just that in this patch.

I also renamed `isClosedAlgType` to `pmIsClosedType`, reflecting the fact that
`TYPE` technically isn't an algebraic type (it's a primitive one), and that its
behavior is pattern-match coverage checking-oriented. I also moved it to
`Check`, which is a better home for this function than `Type`. Luckily,
the only call sites for `isClosedAlgType` were in the pattern-match coverage
checker anyways, so this change is simple enough.

Test Plan: ./validate

Reviewers: mpickering, austin, goldfire, bgamari

Reviewed By: goldfire

Subscribers: rwbarton, thomie, mpickering

GHC Trac Issues: #14086

Differential Revision: https://phabricator.haskell.org/D3830
Note: See TracTickets for help on using tickets.