[GHC] #15305: Erroneous "non-exhaustive pattern match" using nested GADT with strictness annotation
GHC
ghc-devs at haskell.org
Thu Jul 26 11:04:49 UTC 2018
#15305: Erroneous "non-exhaustive pattern match" using nested GADT with strictness
annotation
-------------------------------------+-------------------------------------
Reporter: jkoppel | Owner: (none)
Type: bug | Status: new
Priority: normal | Milestone: Research
Component: Compiler (Type | needed
checker) | Version: 8.4.3
Resolution: | Keywords:
| PatternMatchWarnings
Operating System: Unknown/Multiple | Architecture:
Type of failure: Incorrect | Unknown/Multiple
error/warning at compile-time | Test Case:
Blocked By: | Blocking:
Related Tickets: | Differential Rev(s):
Wiki Page: |
-------------------------------------+-------------------------------------
Comment (by simonpj):
My strong instinct here is to go back to the paper. In rule [UConVar] and
friends we split up 'x' into a union of constructors {K x1, K2 x2 x3, K3}.
Each of those split constructors comes with an extended `Delta`, which
describes the constraints in scope. If these constraints prove
contradicatory we can drop the entire branch.
So for a strict constructor, say
{{{
data T a where
MkT :: a -> !a -> T a
}}}
we want to add a constraint to `Delta` that says that the type of that
second argument is non-void; that is, it contains at least one element
that terminates. So maybe we need a constraint `NonVoid( tau )`.
In the OP, `NonVoid( Bar A )` would be a contradiction.
In the implementation we have a simple "term oracle" that works alongside
the type oracle that is implemented by the constraint solver. Maybe we
could add the new constraint to the term oracle?
--
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/15305#comment:9>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler
More information about the ghc-tickets
mailing list