Opened 22 months ago

Closed 17 months ago

Last modified 17 months ago

#14547 closed bug (fixed)

Wrong warning by -Wincomplete-patterns

Reported by: YoshikuniJujo Owned by:
Priority: low Milestone: 8.6.1
Component: Compiler Version: 8.2.1
Keywords: incomplete-patterns OverloadedLists, PatternMatchWarnings TypeFamilies Cc: dfeuer
Operating System: Linux Architecture: x86
Type of failure: Incorrect error/warning at compile-time Test Case: deSugar/should_compile/T14547
Blocked By: Blocking:
Related Tickets: Differential Rev(s): Phab:D4624
Wiki Page:

Description

Wrong warning occur where I use -Wincomplete-patterns with OverloadedLists and TypeFamilies.

{-# LANGUAGE OverloadedLists #-}
{-# LANGUAGE TypeFamilies #-}
{-# OPTIONS_GHC -Wall -fno-warn-tabs #-}

class Foo f where
        type It f
        foo :: [It f] -> f

data List a = Empty | a :! List a deriving Show

instance Foo (List a) where
        type It (List a) = a
        foo [] = Empty
        foo (x : xs) = x :! foo xs

Pattern match(es) are non-exhaustive In an equation for `foo': Patterns not matched: []

Change History (17)

comment:1 Changed 22 months ago by simonpj

Keywords: PatternMatchWarnings added

comment:2 Changed 17 months ago by sighingnow

Differential Rev(s): Phab:D4624
Status: newpatch
Test Case: deSugar/should_compile/T14547

comment:3 Changed 17 months ago by simonpj

I'm a bit lost with this example. I think that, because of OverloadedLists it desugars as

        foo (toList -> []) = Empty
        foo (toList -> (x : xs)) = x :! foo xs

But then we actually need the [] (list) instance of toList which is the identity function? Then what? How does the bogus error message arise?

comment:4 Changed 17 months ago by sighingnow

During the exhaustiveness checking, we already know the type of [], we use splitListTyConApp_maybe to check whether it's type is [a] (list) or not and extract its element type.

splitListTyConApp_maybe :: Type -> Maybe Type
splitListTyConApp_maybe ty = case splitTyConApp_maybe ty of
  Just (tc,[e]) | tc == listTyCon -> Just e
  _other                          -> Nothing

Indeed we don't need to know the toList of [] instance is identity function, we know the type of the pattern is [] then the toList is omitted and it is enough to know [] is the nil pattern.

comment:5 Changed 17 months ago by simonpj

Indeed we don't need to know the toList of [] instance is identity function,

Good point. So this ticket is

  • not about overloaded strings
  • not about type functions

It's only about view patterns. Could you re-formulate the example to eliminate the unnecessary clutter, and focus just on view patterns?

And then (sorry to be slow) take us more slowly through what the problem is? It'll be something to do with the way that the pattern match checker deals with view patterns, I guess.

comment:6 Changed 17 months ago by sighingnow

My previous comment addresses on toList, leading to some confusion. The ticket IS about the type functions.

Look the ListPat case in translatePat (after the patch Phab:D4624):

  -- overloaded list
  ListPat x lpats elem_ty (Just (pat_ty, _to_list))
    | Just e_ty <- splitListTyConApp_maybe pat_ty
    , (_, norm_e_ty) <- normaliseType fam_insts Nominal e_ty
         -- e_ty can be a type family instance, like
         -- `It (List a)`, but we prefer `a`, see Trac #14547
    , (_, norm_elem_ty) <- normaliseType fam_insts Nominal elem_ty
         -- elem_ty is frequently something like
         -- `Item [Int]`, but we prefer `Int`
    , norm_elem_ty `eqType` norm_e_ty ->
        -- We have to ensure that the element types are exactly the same.
        -- Otherwise, one may give an instance IsList [Int] (more specific than
        -- the default IsList [a]) with a different implementation for `toList'
    
        translatePat fam_insts (ListPat x lpats e_ty Nothing)
      -- See Note [Guards and Approximation]
    | otherwise -> mkCanFailPmPat pat_ty

For pattern [] in foo [] = Empty, we have

pat_ty [It (List a_a2mv)]
e_ty It (List a_a2mv)
norm_e_ty a_a2mv
elem_ty GHC.Exts.Item [a_a2mv]
norm_elem_ty a_a2mv

Before Phab:4624, we compared norm_elem_ty with e_ty, rather than norm_e_ty, then we failed to know the [] is list's nil pattern. We need also normalize the e_ty and this ticket is only about the type function.

comment:7 Changed 17 months ago by simonpj

Ah, hmm, I think I see. Given something like

f (toList -> [])     = e1
f (toList -> (a:as)) = e2

we'd like to declare this function exhaustive. (Clearly it is!)

The ListPat case of Check.translatePat deals with a very special sub-case.

  • Using OverloadedLists, we generate a special kind of view pattern, encoded in the ListPat constructor of Pat:
      | ListPat     (XListPat p)
                    [LPat p]
                    (PostTc p Type)                      -- The type of the elements
                    (Maybe (PostTc p Type, SyntaxExpr p)) -- For rebindable syntax
                       -- For OverloadedLists a Just (ty,fn) gives
                       -- overall type of the pattern, and the toList
                       -- function to convert the scrutinee to a list value
    
  • You are checking that the function actually has type [t1] -> [t2], where normalise t1 = normalise t2.
  • In that case, you discard the toList view thing altogether, and pretend (for the purposes of pattern-match checking) that you wrote
    f [] = e1
    f (a:as) = e2
    

This would not be valid if you'd had

f (toList      -> [])     = e1
f (weirdToList -> (a:as)) = e2

with two different toList functions. But in this special case the view function was injected by the type-driven overloading machinery, so we can be confident (I think) that both functions are the same.

So at least all this should be explained in a Note.

But it also seems like a special case that is easily defeated. For example, what about this:

f :: T -> blah
f (toList -> [])    = ...
f (toList -> (x:xs) = ...

This too is exhaustive, but it won't be recorded as such, even if you use OverloadedLists.

And of course if you use explicit view patterns, things are even worse.

At least the Note should point out these deficiencies

comment:8 Changed 17 months ago by dfeuer

Cc: dfeuer added

In Simon's example,

f (toList -> [])     = e1
f (toList -> (a:as)) = e2

I don't see how it's at all relevant that toList is from an IsList instance. I imagine we always want to common up view patterns using the same function for coverage checking. For example, given

f (g -> P1) = e1
f P2 = e2
f (g -> P3) = e3

I imagine we want to transform that to something like

f x
  | P1 <- gx = e1
  | P2 <- x = e2
  | P3 <- gx = e3
  where gx = g x

when performing coverage checks. I don't know how the details work out for the pattern checker.

comment:9 in reply to:  7 Changed 17 months ago by sighingnow

Replying to simonpj:

Thanks for your explanation and analysis, Simon. I agree to add a note to explain this condition. Now I have some other thought with the ListPat case of translatePat.

You are checking that the function actually has type [t1] -> [t2], where normalise t1 = normalise t2.

I think in fact we don't need to do the check. For ListPat x lpats elem_ty (Just (pat_ty, _to_list)), we know the _to_list have type:

toList :: l -> [Item l]

If we know the pat_ty (the l in toList's signature) is [a] (the List type), then we can conclude that Item l = a, in other words, norm_elem_ty = norm_e_ty. Because in instance IsList [a], we have type (Item [a]) = a. Although we can give an instance IsList [Int] (more specific than the default IsList [a]), we can't overwrite the type family instance.

The original comment says:

-- We have to ensure that the element types are exactly the same.
-- Otherwise, one may give an instance IsList [Int] (more specific than
-- the default IsList [a]) with a different implementation for `toList'

However we can't achieve this goal without check the type of _to_list. In practice, we almost never define more specific IsList instance like instance IsList [Int], we don't need to concern that case. So we can simplify the code as

  ListPat x lpats elem_ty (Just (pat_ty, _to_list))
    | Just e_ty <- splitListTyConApp_maybe pat_ty
    -> translatePat fam_insts (ListPat x lpats e_ty Nothing)
    | otherwise
    -> mkCanFailPmPat pat_ty

Or should be check whether the type of _to_list is [a] -> [a] (the most general type) ? I don't think it's necessary for practical Haskell code. I'm not sure if I understand this correctly.

Another silly question is that I still can't see why we need to concern about the view pattern for exhaustiveness checking of overloaded list. I think the toList and the [a] instance of IsList are different with ordinary view functions in view pattern. I will mention this in the note.

comment:10 Changed 17 months ago by simonpj

Alas, with RebindableSyntax we don't know anything about toList. (Without RebindableSyntax I think your reasoning is correct.)

But now I am worried about

f (x:xs) = ..
f [p,q]  = ...

The (x:xs) pattern will translate as an ordinary cons pattern. The [p,q] pattern will be subject to overloaded lists. So if RebindableSyntax is on and toList does something strange, simply dropping the toList altogether, and desugaring to

f (x:xs)   = ..
f (p:q:[]) = ...

may not be right.

So in the presence of RebindableSyntax I think we should treat ListPat like any other view pattern; i.e. coverage/exhaustiveness does not help much.

In the absence of RebindableSyntax, but with -XOverloadedStrings, can we be sure that toList is the identity function if the pattern type is a list type? I think so. In which case your simplified version is fine.

Bottom line: check for NoRebindableSyntax!

Another silly question is that I still can't see why we need to concern about the view pattern for exhaustiveness checking of overloaded list. I think the toList and the [a] instance of IsList are different with ordinary view functions in view pattern.

I could not parse the question.

comment:11 in reply to:  10 Changed 17 months ago by sighingnow

Replying to simonpj:

I misread your previous comment, my bad.

Bottom line: check for NoRebindableSyntax!

I have revised the Phab:D4624. Now when RebindableSyntax is enabled we treat the overloaded list pattern as ordinary view pattern. I have added some comments about this problem.

comment:12 Changed 17 months ago by Ben Gamari <ben@…>

In 361d23a/ghc:

Normalize the element type of ListPat, fix #14547

The element type of `List` maybe a type family instacen, rather than a
trivial type.  For example in Trac #14547,

```
{-# LANGUAGE TypeFamilies, OverloadedLists #-}

class Foo f where
        type It f
        foo :: [It f] -> f

data List a = Empty | a :! List a deriving Show

instance Foo (List a) where
        type It (List a) = a
        foo [] = Empty
        foo (x : xs) = x :! foo xs
```

Here the element type of `[]` is `It (List a)`, we should also normalize
it as `a`.

Test Plan: make test TEST="T14547"

Reviewers: bgamari

Reviewed By: bgamari

Subscribers: thomie, carter

GHC Trac Issues: #14547

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

comment:13 Changed 17 months ago by bgamari

Milestone: 8.6.1
Resolution: fixed
Status: patchclosed

comment:14 Changed 17 months ago by Ben Gamari <ben@…>

In 280de0c/ghc:

Revert "Normalize the element type of ListPat, fix #14547"

This reverts commit 361d23a8ebb44f5df5167306d7b98d8bd1724e06.

comment:15 Changed 17 months ago by Ben Gamari <ben@…>

In 981bf47/ghc:

Normalize the element type of ListPat, fix #14547

The element type of `List` maybe a type family instacen, rather than a
trivial type.
For example in Trac #14547,

```
{-# LANGUAGE TypeFamilies, OverloadedLists #-}

class Foo f where
        type It f
        foo :: [It f] -> f

data List a = Empty | a :! List a deriving Show

instance Foo (List a) where
        type It (List a) = a
        foo [] = Empty
        foo (x : xs) = x :! foo xs
```

Here the element type of `[]` is `It (List a)`, we should also normalize
it as `a`.

Test Plan: make test TEST="T14547"

Reviewers: bgamari

Reviewed By: bgamari

Subscribers: thomie, carter

GHC Trac Issues: #14547

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

comment:16 Changed 17 months ago by Ben Gamari <ben@…>

In 849547b/ghc:

Revert "Normalize the element type of ListPat, fix #14547"

This reverts commit 981bf4718de7daef7817a363ccc14030c2688632.

comment:17 Changed 17 months ago by Ben Gamari <ben@…>

In ba6e445/ghc:

Normalize the element type of ListPat, fix #14547

Summary:
The element type of `List` maybe a type family instacen, rather than a trivial type.
For example in Trac #14547,

```
{-# LANGUAGE TypeFamilies, OverloadedLists #-}

class Foo f where
        type It f
        foo :: [It f] -> f

data List a = Empty | a :! List a deriving Show

instance Foo (List a) where
        type It (List a) = a
        foo [] = Empty
        foo (x : xs) = x :! foo xs
```

Here the element type of `[]` is `It (List a)`, we should also normalize
it as `a`.

Test Plan: make test TEST="T14547"

Reviewers: bgamari

Reviewed By: bgamari

Subscribers: thomie, carter

GHC Trac Issues: #14547

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