Pattern guards give false exhaustivity errors

[paf31]

Example:

module Main where

import Prelude

data X = X Int | Y

x :: X -> Int
x = case _ of
      Y -> 0
      X n | 1 <- n -> 1
          | otherwise -> 2

which gives:

Error found:
in module Main
at src/Main.purs line 9, column 5 - line 12, column 26

  A case expression could not be determined to cover all inputs.
  The following additional cases are required to cover all inputs:

    Y

  Alternatively, add a Partial constraint to the type of the enclosing value.

while applying a function __unused
  of type Partial => t0 -> t0
  to argument case $0 of              
                (X n) | otherwise -> 2
while inferring the type of __unused (case $0 of              
                                        (X n) | otherwise -> 2
                                     )                        
in value declaration x

where t0 is an unknown type

It looks like the desugaring is at fault here, since X n is the only alternative left after things are expanded.

@alexbiehl Any ideas here?

[alexbiehl]

x is transformed into

x :: X -> Int 
x y = case y of 
    Y -> 0 
    _ -> let 
           k _ = case y of 
                 X n | otherwise -> 2
          in case y of 
            X n -> case n of -- guard 1 <- n
                1 -> 1
                _ -> k true 

We scrutinize y multiple times here but only bind to X n, missing Y in those cases.

[alexbiehl]

Lets see if I can come up with something better.

btw. I know its a bad excuse but in this example you can change the order of matches to:

x :: X -> Int
x = case _ of
      X n | 1 <- n -> 1
          | otherwise -> 2
      Y -> 0

and it works.

[alexbiehl]

I think the transformation is right, the exhaustivity checker just doesn't know that in subsequent matches missing cases can be ruled out.

We have different alternatives I guess:

• Remember what constructors we already matched and generate "unreached" alternatives. I think we lack a notion of "unreached" alternative and I am not sure we want such thing. We can't just use wildcard binders alone as that would result false-exhaustive cases which is even worse.
• Just don't desugar cases before exhaustivity checking. Desugar them in the ps2core pass instead. I had the part for type checking and exhaustivity around when developing the original feature so this should be no big deal.

btw. Are there any written down notes on invariants of case expressions in surface language?

[paf31]

Thanks for looking at this.

If it's possible to move the transformation after linting and/or type-checking, I think that would be the way to go.

[matthewleon]

I am still having this problem on 0.11.2.

Code:

head :: forall a. Stream a -> a
head xs | Cons x _ <- step xs = x

error:

in module Main
at src/Main.purs line 35, column 1 - line 35, column 33

  A case expression could not be determined to cover all inputs.
  The following additional cases are required to cover all inputs:

    _

  Alternatively, add a Partial constraint to the type of the enclosing value.

while applying a function __unused
  of type Partial => t1 -> t1
  to argument case xs of                     
                xs | Cons x _ <- step xs -> x
while checking that expression __unused (case xs of                     
                                           xs | Cons x _ <- step xs -> x
                                        )                               
  has type a0
in value declaration head

where a0 is a rigid type variable
        bound at line 35, column 1 - line 35, column 33
      t1 is an unknown type

[alexbiehl]

Oh boy, I should have more and better tests. This time it's the exhaustiveness checker at [1]. It checks for irrefutable binders which by definition [2] doesn't look into the structure of the data type. We need to take a look into the definition of the data type and check if its a product type, and if constructor binders are exhaustive. [1] https://github.com/purescript/purescript/blob/master/src/Language/PureScript/Linter/Exhaustive.hs#L206 [2] https://github.com/purescript/purescript/blob/0ee5b7495fae6319ca6f33a6691cf6cae1110466/src/Language/PureScript/AST/Binders.hs#L85 . Matthew Leon <notifications@github.com> schrieb am Mo., 3. Apr. 2017 um 18:19 Uhr:

…

I am still having this problem on 0.11.2. Code: head :: forall a. Stream a -> a head xs | Cons x _ <- step xs = x error: in module Main at src/Main.purs line 35, column 1 - line 35, column 33 A case expression could not be determined to cover all inputs. The following additional cases are required to cover all inputs: _ Alternatively, add a Partial constraint to the type of the enclosing value. while applying a function __unused of type Partial => t1 -> t1 to argument case xs of xs | Cons x _ <- step xs -> x while checking that expression __unused (case xs of xs | Cons x _ <- step xs -> x ) has type a0 in value declaration head where a0 is a rigid type variable bound at line 35, column 1 - line 35, column 33 t1 is an unknown type — You are receiving this because you were mentioned. Reply to this email directly, view it on GitHub <#2795 (comment)>, or mute the thread <https://github.com/notifications/unsubscribe-auth/AByiia_jdPVyBO2cAZlKCMG3JGbiKxUmks5rsRv_gaJpZM4MtxRQ> .

[paf31]

Let's open a new issue for this one.