Exhaustiveness checking for pattern synonyms
ClosedPublic

Authored by mpickering on Nov 2 2016, 4:57 PM.

Details

Summary

This patch adds a new pragma so that users can specify COMPLETE sets of
ConLikes in order to sate the pattern match checker.

Things which need to be resolved:

  • Write a specification
  • Documentation in the user guide
  • Beef up typechecking to check the set of patterns in consistent
  • Persist constructor sets between modules
  • Allow COMPLETE sigs to mention imported ids.
  • Resolve what should become of the copied ListT code.
  • Move test files into the pmcheck directory.
  • Add annotations to the parser

Diff Detail

Repository
rGHC Glasgow Haskell Compiler
Lint
Automatic diff as part of commit; lint not applicable.
Unit
Automatic diff as part of commit; unit tests not applicable.
There are a very large number of changes, so older changes are hidden. Show Older Changes
nomeata added inline comments.Dec 7 2016, 12:13 PM
testsuite/tests/pmcheck/complete_sigs/completesig11.stderr
5

I would want to see a mention of C here as well, for symmetry. (This comment is JFTR, and should be handled in a separate ticket about improving the error messages.)

lelf added a subscriber: lelf.Dec 7 2016, 3:18 PM

@gkaracha I just added the nests you suggested if you want to look at the output.

Thanks @mpickering, I really wanted to see how the extension behaves. I took a look at the outputs and I have a couple more points to make:

  • About typing, if I understand the code correctly, I expect the following to work OK, please just confirm that indeed it does, by adding this test to the testsuite:
data G a where
  G1' :: G Int
  G2' :: G Bool

pattern G1 :: (a ~ Int) => G a
pattern G1 = G1'

pattern G2 :: (a ~ Bool) => G a
pattern G2 = G2'

{-# COMPLETE G1, G2 #-}

fa :: G a -> Int   -- exhaustive function
fa G1 = 1
fa G2 = 2

fb :: G Int -> Int -- exhaustive function
fb G1 = 1
-- fb G2 = 2       -- inaccessible clause
  • Could you also add a test for which the redundancy occurs for a pattern which does not appear in a COMPLETE declaration? E.g. add the following in testsuite/tests/pmcheck/complete_sigs/completesig07.hs:
data T = A | B | C
data S = D | E | F

m3 :: T -> ()
m3 C = ()
m3 C = ()
  • In testsuite/tests/pmcheck/complete_sigs/completesig10.hs, shouldn't m3 be exhaustive? Set {C,D} (2nd and 3rd clause together) forms a complete signature (which means that the two of them should give the smaller uncovered set possible --the empty one). Am I missing something here?
mpickering marked an inline comment as done.Dec 8 2016, 8:28 AM

@gkaracha I just added the nests you suggested if you want to look at the output.

Thanks @mpickering, I really wanted to see how the extension behaves. I took a look at the outputs and I have a couple more points to make:

  • About typing, if I understand the code correctly, I expect the following to work OK, please just confirm that indeed it does, by adding this test to the testsuite: ` data G a where G1' :: G Int G2' :: G Bool

    pattern G1 :: (a ~ Int) => G a pattern G1 = G1'

    pattern G2 :: (a ~ Bool) => G a pattern G2 = G2'

    {-# COMPLETE G1, G2 #-}

    fa :: G a -> Int -- exhaustive function fa G1 = 1 fa G2 = 2

    fb :: G Int -> Int -- exhaustive function fb G1 = 1
    • fb G2 = 2 -- inaccessible clause `
  • Could you also add a test for which the redundancy occurs for a pattern which does not appear in a COMPLETE declaration? E.g. add the following in testsuite/tests/pmcheck/complete_sigs/completesig07.hs: ` data T = A | B | C data S = D | E | F

    m3 :: T -> () m3 C = () m3 C = () `
  • In testsuite/tests/pmcheck/complete_sigs/completesig10.hs, shouldn't m3 be exhaustive? Set {C,D} (2nd and 3rd clause together) forms a complete signature (which means that the two of them should give the smaller uncovered set possible --the empty one). Am I missing something here?

I did not expect that first test to work but it actually did!

I added the second test and it looks like you are right about the output of the third example.

mpickering updated this revision to Diff 9852.Dec 8 2016, 8:30 AM
  • Add some more tests

The problem with completesig10 is that it is the first match which is redundant. There seems to be an assumption somewhere in the checker that allCompleteMatches returns the same result for each constructor with the same parent. Before I made these changes, this was of course true but now this invariant is violated.

I haven't investigated much as I thought that maybe @gkaracha could point me to the right place where this invariant is used.

The problem with completesig10 is that it is the first match which is redundant. There seems to be an assumption somewhere in the checker that allCompleteMatches returns the same result for each constructor with the same parent. Before I made these changes, this was of course true but now this invariant is violated.

I haven't investigated much as I thought that maybe @gkaracha could point me to the right place where this invariant is used.

Hmmmm, gimme some time to look at this and I'll come back at you.

PS. The first is not really redundant, I'd say it has an inaccessible RHS 'cause it forces the argument. I think the semantics is very puzzling in cases like this: since the COMPLETE definition is not really complete, I am not sure what does the first clause means.

The problem with completesig10 is that it is the first match which is redundant. There seems to be an assumption somewhere in the checker that allCompleteMatches returns the same result for each constructor with the same parent. Before I made these changes, this was of course true but now this invariant is violated.

I haven't investigated much as I thought that maybe @gkaracha could point me to the right place where this invariant is used.

Actually, you could say that this invariant is implicitly used everywhere and the extension should not violate it either. By definition, a signature is complete with respect to a type constructor.

That being said, like with simple DataCons, I think allCompleteMatches should look up with respect to the TyCon they correspond to, and not filter (call to relevantMatch) by checking in which sets the ConLike is in.

If PatSyns supported patSynTyCon (like dataConTyCon for DataCons), you could simply index CompleteMatch with the TyCon the signature corresponds to:

data CompleteMatch = CompleteMatch { cm_tc  :: TyCon
                                   , cm_cls :: [ConLike] }

and then look up based on the TyCon. As far as I know though, a pattern synonym can result in any type (not necessarily a TyConApp) which means that it is not always possible to do so.

To conclude, the only reasonable solution I see is to get the TyCon for which the signature is complete from the pragma. E.g. something like:

{-# COMPLETE A: A, B #-}
{-# COMPLETE A: C, D #-}

What are your thoughts on this?

The problem with completesig10 is that it is the first match which is redundant. There seems to be an assumption somewhere in the checker that allCompleteMatches returns the same result for each constructor with the same parent. Before I made these changes, this was of course true but now this invariant is violated.

I haven't investigated much as I thought that maybe @gkaracha could point me to the right place where this invariant is used.

Actually, you could say that this invariant is implicitly used everywhere and the extension should not violate it either. By definition, a signature is complete with respect to a type constructor.

That being said, like with simple DataCons, I think allCompleteMatches should look up with respect to the TyCon they correspond to, and not filter (call to relevantMatch) by checking in which sets the ConLike is in.

If PatSyns supported patSynTyCon (like dataConTyCon for DataCons), you could simply index CompleteMatch with the TyCon the signature corresponds to:

data CompleteMatch = CompleteMatch { cm_tc  :: TyCon
                                   , cm_cls :: [ConLike] }

and then look up based on the TyCon. As far as I know though, a pattern synonym can result in any type (not necessarily a TyConApp) which means that it is not always possible to do so.

To conclude, the only reasonable solution I see is to get the TyCon for which the signature is complete from the pragma. E.g. something like:

{-# COMPLETE A: A, B #-}
{-# COMPLETE A: C, D #-}

What are your thoughts on this?

I disagree with this definition. A complete match is a set of patterns such that if a user writes a function which matches on all the patterns, the function is total. One way to get a complete set of patterns is to look at the type of the argument and find all its data constructors but that isn't the only way.

Where else in the compiler are you thinking which requires this invariant?

The one case which is an actual problem is when you have a COMPLETE set which has no fixed type constructors..

For example,

pattern Nil :: ListLike k => k
pattern Nil <- (matchList -> True)
.....

pattern Cons :: LikeLike k => a -> k -> k
pattern Cons a k <- (matchCons -> Just (a, k))
.....

Perhaps the actual solution is to disallow users to write

{-# COMPLETE Nil, Cons #-}

and instead have to write

{-# COMPLETE Nil, Cons :: [] #-}

or... I can work out why this invariant is necessary in the current implementation of the pattern match checker and get rid of it. :)

I disagree with this definition. A complete match is a set of patterns such that if a user writes a function which matches on all the patterns, the function is total. One way to get a complete set of patterns is to look at the type of the argument and find all its data constructors but that isn't the only way.

I agree with you, you can have multiple definitions for this. It's just that this problem is very hard in general and actually undecidable. All checkers I know of are based on this behaviour (including mine), because there is no simple way to check what is missing or not (the problem corresponds to type inhabitation which is known to be undecidable). If you have an idea of a new approach I'd be happy to discuss it though, but I don't have any, if you are asking :-)

Where else in the compiler are you thinking which requires this invariant?

For efficient compilation of pattern matching I guess you also need it (I say efficient because a translation to guards would work with less information but it will never be as efficient as old fashioned pattern matching).

The one case which is an actual problem is when you have a COMPLETE set which has no fixed type constructors..

For example,

pattern Nil :: ListLike k => k
pattern Nil <- (matchList -> True)
.....

pattern Cons :: LikeLike k => a -> k -> k
pattern Cons a k <- (matchCons -> Just (a, k))
.....

Indeed, this is one of the cases I had in mind too.

Perhaps the actual solution is to disallow users to write

{-# COMPLETE Nil, Cons #-}

and instead have to write

{-# COMPLETE Nil, Cons :: [] #-}

I definitely agree on this one, I suggested the same (if we ignore my ugly, for-illustration-purposes-only syntax).

mpickering updated this revision to Diff 10136.Dec 20 2016, 4:03 PM
mpickering edited edge metadata.
  • Type sigs

Ok! Any more comments? I want to wrap this up before too long.

mpickering updated this revision to Diff 10138.Dec 20 2016, 4:10 PM
mpickering edited edge metadata.
  • Remove stray commit
mpickering updated this revision to Diff 10143.Dec 21 2016, 4:17 AM
mpickering edited edge metadata.
  • Fix warning

George, is an *inaccessible RHS* a pattern which is redundant but can't be removed without affecting strictness?

George, is an *inaccessible RHS* a pattern which is redundant but can't be removed without affecting strictness?

Yes, you could call it that. It is a clause which can never match but can crash (hence not strictly speaking redundant).

mpickering updated this revision to Diff 10145.Dec 21 2016, 9:23 AM
mpickering edited edge metadata.
  • Fix pprinting of conlikes'
  • Make the checker prefer matches which don't have inaccessible branches

@gkaracha

I talked with Reid about this in IRC and he suggested that complete matches arising from COMPLETE pragmas shouldn't emit redundant or inaccessible warnings. I think I agree with him, what do you think?

mpickering updated this revision to Diff 10304.Jan 6 2017, 10:29 AM
mpickering edited edge metadata.
  • Add presistence across modules
  • Refactoring
  • Alpha renaming
  • Allow COMPLETE sigs to mention imported ids
  • Add type checking
  • Remove trace
  • move tests
  • Add annotations to parser
  • Some comments
  • Revert changes to RnSource
  • Satisfy doggo
  • Add better explanation of getResult
  • Improve standard error
  • Fix rebase
  • Refactoring COMPLETE
  • Simplify interface file
  • Fix Module test
  • Remove whitespace
  • Add comment
  • Fix bad rebase
  • Refactor [ConLike] to CompleteMatch newtype
  • Renaming tests
  • Add missing files
  • Two more
  • Nested matching example
  • Complete sig 08
  • Missing stderr
  • Interaction between two pragams tests
  • Satisfy doggo
  • Joachim's example
  • Rework error message
  • First stab at documentation
  • Add some more tests
  • silly cange
  • Don't warn about redundancy when COMPLETE is involved
mpickering updated this revision to Diff 10318.Jan 6 2017, 12:48 PM
mpickering edited edge metadata.
  • Add presistence across modules
  • Refactoring
  • Alpha renaming
  • Allow COMPLETE sigs to mention imported ids
  • Add type checking
  • Remove trace
  • move tests
  • Add annotations to parser
  • Some comments
  • Revert changes to RnSource
  • Satisfy doggo
  • Add better explanation of getResult
  • Improve standard error
  • Fix rebase
  • Refactoring COMPLETE
  • Simplify interface file
  • Fix Module test
  • Remove whitespace
  • Add comment
  • Fix bad rebase
  • Refactor [ConLike] to CompleteMatch newtype
  • Renaming tests
  • Add missing files
  • Two more
  • Nested matching example
  • Complete sig 08
  • Missing stderr
  • Interaction between two pragams tests
  • Satisfy doggo
  • Joachim's example
  • Rework error message
  • First stab at documentation
  • Add some more tests
  • silly cange
  • Don't warn about redundancy when COMPLETE is involved
  • Type sigs
  • Fix warning
  • Fix pprinting of conlikes'
  • Make the checker prefer matches which don't have inaccessible branches
  • Update output
  • fix order of provenance
mpickering updated this revision to Diff 10319.Jan 6 2017, 12:57 PM
mpickering edited edge metadata.
  • missing file
alanz accepted this revision.Jan 7 2017, 9:35 AM
alanz edited edge metadata.

The annotations parts seem ok, by eyeballing it

This revision is now accepted and ready to land.Jan 7 2017, 9:35 AM
mpickering requested a review of this revision.Jan 13 2017, 9:37 AM
mpickering edited edge metadata.

I think this is finished. Can someone please review this patch so that I can land it well before the 8.2 freeze?

mpickering edited edge metadata.
  • rebase
  • Satisfy doggo
bgamari requested changes to this revision.Jan 17 2017, 11:12 AM
bgamari edited edge metadata.

This generally looks good. I've pointed out a number of places inline where clarity could be improved but once these are addressed I think this is ready.

Sorry again for the quite belated review, @mpickering, and thanks for your patience.

compiler/deSugar/Check.hs
204

Perhaps add a comment on this. For instance,

-- | Where we learned that a given match group is complete.
data Provenance = FromBuiltin   -- ^ ?
                | FromComplete  -- ^ from a user-provided @COMPLETE@ pragma
933

A comment explaining this would be helpful.

compiler/deSugar/DsMonad.hs
619

A Haddock comment here would be helpful:

-- | The @COMPLETE@ pragmas provided by the user for a given 'TyCon'.
compiler/main/HscTypes.hs
2987

It wouldn't hurt to make this a Haddock comment.

compiler/typecheck/TcBinds.hs
205

The typical style for a Note is,

Note [Typechecking Complete Matches]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Much like when a user bundled ...
`

Note that lack of colon between Note and the title. Consistency here ensures that notes can be easily grepped for.

213

Perhaps turn this into a Haddock comment so it's clear that it applies to CompleteSigType and is not a continuation of the Note above.

242

Are we to understand that this case is impossible? If so let's turn this into a panic with an identifiable message.

compiler/typecheck/TcRnTypes.hs
389

Generally it's best to use foldl' when constructing things like maps that can't be consumed incrementally (but admittedly there are plenty of places in the compiler which break this rule of thumb).

docs/users_guide/glasgow_exts.rst
12777

s/it's/its.

This revision now requires changes to proceed.Jan 17 2017, 11:12 AM
mpickering updated this revision to Diff 10544.Jan 19 2017, 6:41 AM
mpickering edited edge metadata.
  • Ben's suggestions
  • Fixup
  • Add file for polymorphic pat syn error
mpickering marked 8 inline comments as done.Jan 20 2017, 8:38 AM
mpickering added inline comments.
compiler/typecheck/TcBinds.hs
213

It wasn't clear to me how to do this properly so I added some more space between the two.

242

I missed this thanks. It is an actual error which is now reported properly to the user.

mpickering updated this revision to Diff 10555.Jan 20 2017, 8:59 AM
mpickering marked 2 inline comments as done.
mpickering edited edge metadata.
  • Add one more comment

There is one test that fails but I feel this is more due to Trac #11822 than my implementation. There shouldn't be a significant effect of these changes when no COMPLETE pragmas are specified but there could be some cost.

There is one test that fails but I feel this is more due to Trac #11822 than my implementation. There shouldn't be a significant effect of these changes when no COMPLETE pragmas are specified but there could be some cost.

Do you mean Trac #11195? I see that it gives a non-zero exit code. Trac #11822 has to do with exceeding the predefined number of iterations, so if that was the case I think it would just have a stderr difference only. Can you run locally and tell me what the output is? There is a chance I could help with it :)

There is one test that fails but I feel this is more due to Trac #11822 than my implementation. There shouldn't be a significant effect of these changes when no COMPLETE pragmas are specified but there could be some cost.

Do you mean Trac #11195? I see that it gives a non-zero exit code. Trac #11822 has to do with exceeding the predefined number of iterations, so if that was the case I think it would just have a stderr difference only. Can you run locally and tell me what the output is? There is a chance I could help with it :)

It is failing because of the timeout.

====> Scanning ./should_compile/all.T
=====> T11195(normal) 1 of 1 [0, 0, 0]
cd "./should_compile/T11195.run" &&  "/root/ghc/inplace/test   spaces/ghc-stage2" -c T11195.hs -dcore-lint -dcmm-lint -no-user-package-db -rtsopts -fno-warn-missed-specialisations -fshow-warning-groups -fdiagnostics-color=never -fno-diagnostics-show-caret -dno-debug-output  -package ghc -fwarn-incomplete-patterns -fwarn-overlapping-patterns +RTS -M1G -RTS
Timeout happened...killed process "cd "./should_compile/T11195.run" &&  "/root/ghc/inplace/test   spaces/ghc-stage2" -c T11195.hs -dcore-lint -dcmm-lint -no-user-package-db -rtsopts -fno-warn-missed-specialisations -fshow-warning-groups -fdiagnostics-color=never -fno-diagnostics-show-caret -dno-debug-output  -package ghc -fwarn-incomplete-patterns -fwarn-overlapping-patterns +RTS -M1G -RTS"...

Compile failed (exit code 99) errors were:

*** unexpected failure for T11195(normal)

Unexpected results from:
TEST="T11195"

If I remove the RTS options +RTS -M1G -RTS then it terminates in a reasonable amount of time. Why are these options added when running tests?

If I remove the RTS options +RTS -M1G -RTS then it terminates in a reasonable amount of time. Why are these options added when running tests?

Ah, I see. Well, this is a performance test, hence the limits. The problem is that I don't think I can have Trac #11195 fixed for 8.2 so we'll probably have to relax the limits for now to avoid getting errors from harbormaster.

mpickering updated this revision to Diff 10595.Jan 21 2017, 3:04 PM
mpickering edited edge metadata.
  • Bump heap limit to 2GB
bgamari accepted this revision.Jan 25 2017, 5:56 PM
bgamari edited edge metadata.

Looks good to me @mpickering! Let's merge this!

This revision is now accepted and ready to land.Jan 25 2017, 5:56 PM

Yay! I will update the commit message and then land it with the template haskell patch.

This revision was automatically updated to reflect the committed changes.