Skip to content

GitLab

  • Menu
Projects Groups Snippets
  • Help
    • Help
    • Support
    • Community forum
    • Submit feedback
  • Sign in / Register
  • GHC GHC
  • Project information
    • Project information
    • Activity
    • Labels
    • Members
  • Repository
    • Repository
    • Files
    • Commits
    • Branches
    • Tags
    • Contributors
    • Graph
    • Compare
    • Locked Files
  • Issues 4,982
    • Issues 4,982
    • List
    • Boards
    • Service Desk
    • Milestones
    • Iterations
  • Merge requests 479
    • Merge requests 479
  • CI/CD
    • CI/CD
    • Pipelines
    • Jobs
    • Schedules
    • Test Cases
  • Deployments
    • Deployments
    • Releases
  • Analytics
    • Analytics
    • Value stream
    • CI/CD
    • Code review
    • Insights
    • Issue
    • Repository
  • Wiki
    • Wiki
  • Snippets
    • Snippets
  • Activity
  • Graph
  • Create a new issue
  • Jobs
  • Commits
  • Issue Boards
Collapse sidebar
  • Glasgow Haskell Compiler
  • GHCGHC
  • Issues
  • #8779
Closed
Open
Created Feb 13, 2014 by Joachim Breitner@nomeataDeveloper

Exhaustiveness checks for pattern synonyms

Pattern synonyms are great, as they decouple interface from implementation. Especially if #8581 is also implemented, it should be possible to change a type completely while retaining the existing interface. Exciting!

Another missing piece is exhaustiveness checks. Given this pattern

initLast [] = Nothing
initLast xs = Just (init xs, last xs)
pattern xs ::: x <- (initLast -> Just (xs,x))

we want the compiler to tell the programmer that

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

is complete, while

g (xs ::: x) = ...

is not.

With view pattern directly, this is impossible. But the programmer did not write view patterns!

So here is what I think might work well, inspired by the new MINIMAL pragma:

We add a new pragma COMPLETE_PATTERNS (any ideas for a shorter name). The syntax is essentially the same as for MINIMAL, i.e. a boolean formula, with constructors and pattern synonyms as atoms. In this case.

{-# COMPLETE_PATTERNS [] && (:::) #-}

Multiple pragmas are obviously combined with ||, and there is an implicit {-# COMPLETE_PATTERNS [] && (:) #-} listing all real data constructors.

When checking for exhaustiveness, this would be done before unfolding view patterns, and for g above we get a warning that [] is not matched. Again, the implementation is very much analogous to MINIMAL.

Clearly, a library author can mess up and give wrong COMPLETE_PATTERNS pragmas. I think that is ok (like with MINIMAL), and generally an improvement.

Edited Mar 10, 2019 by Ben Gamari
To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information
Assignee
Assign to
Time tracking