[GHC] #15558: Locally handling an empty constraint
GHC
ghc-devs at haskell.org
Tue Feb 5 18:55:50 UTC 2019
#15558: Locally handling an empty constraint
-------------------------------------+-------------------------------------
Reporter: Ericson2314 | Owner: (none)
Type: task | Status: closed
Priority: normal | Milestone: ⊥
Component: Compiler | Version: 8.0.1
Resolution: fixed | Keywords:
Operating System: Unknown/Multiple | Architecture:
Type of failure: Incorrect | Unknown/Multiple
error/warning at compile-time | Test Case: gadt/T15558
Blocked By: | Blocking:
Related Tickets: | Differential Rev(s):
Wiki Page: |
-------------------------------------+-------------------------------------
Comment (by goldfire):
I think we need an `impossible` that has a type like `Absurdity => a`,
where `Absurdity` is a special constraint that the type checker can
satisfy only when an absurdity is in the context (that is, in inaccessible
code). If an absurdity is used to prove `Absurdity`, then the
"inaccessible code" warning is squelched. This would need custom support
for the `Absurdity` prover, but I don't actually think it would be all
that hard.
I'm not sure what the Core evidence would look like. Perhaps we need
`contra`, tucked without comment in the appendix of the
[https://repository.brynmawr.edu/cgi/viewcontent.cgi?referer=&httpsredir=1&article=1010&context=compsci_pubs
Coercible paper]. The `contra` there is to allow us to assert that `case`
matches are total. GHC's Core, though, doesn't require `case` to be total,
meaning that this has never been implemented.
--
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/15558#comment:14>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler
More information about the ghc-tickets
mailing list