Opened 4 weeks ago

Last modified 4 weeks ago

#13768 new bug

Incorrect warnings generated by exhaustiveness checker with pattern synonyms / GADT combination

Reported by: kosmikus Owned by:
Priority: high Milestone:
Component: Compiler Version: 8.2.1-rc2
Keywords: PatternSynonyms Cc:
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: None/Unknown Test Case:
Blocked By: Blocking:
Related Tickets: Differential Rev(s):
Wiki Page:

Description

The module

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE ViewPatterns #-}
module PatSynEx where

data NS (f :: k -> *) (xs :: [k]) = NS Int

data IsNS (f :: k -> *) (xs :: [k]) where
  IsZ :: f x -> IsNS f (x ': xs)
  IsS :: NS f xs -> IsNS f (x ': xs)

isNS :: NS f xs -> IsNS f xs
isNS = undefined

pattern Z :: () => (xs' ~ (x ': xs)) => f x -> NS f xs'
pattern Z x <- (isNS -> IsZ x)

pattern S :: () => (xs' ~ (x ': xs)) => NS f xs -> NS f xs'
pattern S p <- (isNS -> IsS p)

{-# COMPLETE Z, S #-}

data SList :: [k] -> * where
  SNil  :: SList '[]
  SCons :: SList (x ': xs)

go :: SList ys -> NS f ys -> Int
go SCons (Z _) = 0
go SCons (S _) = 1
go SNil  _     = error "inaccessible"

produces the following warnings with both GHC 8.2 and 8.3:

PatSynEx.hs:31:1: warning: [-Woverlapping-patterns]
    Pattern match has inaccessible right hand side
    In an equation for ‘go’: go SCons (Z _) = ...
   |
31 | go SCons (Z _) = 0
   | ^^^^^^^^^^^^^^^^^^

PatSynEx.hs:32:1: warning: [-Woverlapping-patterns]
    Pattern match is redundant
    In an equation for ‘go’: go SCons (S _) = ...
   |
32 | go SCons (S _) = 1
   | ^^^^^^^^^^^^^^^^^^

Neither warning seems correct. The first case is not inaccessible, the second case is not redundant.

The catch-all case has always been required with GHC even though it is not really reachable, but that's not the subject of this issue.

I tried to simplify the issue further by getting rid of the f argument in NS and IsNS, but that made the issue disappear.

Change History (1)

comment:1 Changed 4 weeks ago by mpickering

Keywords: PatternSynonyms added
Priority: normalhigh

I think the problem here is in mkOneConFull which makes a substitution by zipping together the univ_tvs and tc_args.

If I print out what these values are in this example I find that..

univ_tvs [k_a133, xs'_aSi, f_aSj]
tc_args [k_a27Q, f_a27S, ys_a27R]

which then generates equalities like..

theta_cs [(f_a27S :: [k_a27Q]) ~ ((x_d2kG : xs_d2kH) :: [k_a27Q])]

and the constraint solver reports as unsatisfiable.

If I insert a hack to swap these type variables into the "right" order then the program compiles without warning as expected.

univ_tvs [k_a133, xs'_aSi, f_aSj]
tc_args [k_a27Q, f_a27S, ys_a27R]
theta_cs [(ys_a27R :: [k_a27Q]) ~ ((x_d2ky : xs_d2kz) :: [k_a27Q])]

I don't know what the right solution is here as in general there seems no reason for these two lists to appear in the right order.

Note: See TracTickets for help on using tickets.