#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