[GHC] #15558: Locally handling an empty constraint
#15558: Locally handling an empty constraint -------------------------------------+------------------------------------- Reporter: Ericson2314 | Owner: (none) Type: task | Status: new Priority: normal | Milestone: ⊥ Component: Compiler | Version: 8.0.1 Keywords: | 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: -------------------------------------+------------------------------------- I need something like `\case {}` for constraints. See the code below. There's nothing I can replace the `undefined` with that will satisfy the type checker. The dead code warning also bubbled up out of the field incorrectly. I think this will require new language features tangentially related to Lambdas for `forall`. (Both `forall _.` and `=>` are invisible quantifiers.) I will link this ticket in that GHC proposal, but am making it's own issue in the first place in case this is a genuine bug that can be fixed by less intrusive means. {{{ {-# LANGUAGE RankNTypes #-} {-# LANGUAGE EmptyCase #-} {-# LANGUAGE LambdaCase #-} {-# LANGUAGE GADTs #-} {-# LANGUAGE TypeOperators #-} {-# LANGUAGE ScopedTypeVariables #-} module Asdf where import Data.Kind import Data.Type.Equality data Sing a where X :: Sing Int Y :: Sing [Bool] data Foo a = Foo a (forall b. [b] :~: a -> b) data Bar a = Bar a (forall b. [b] ~ a => b) f, f' :: forall a. Sing a -> Foo a f s = Foo a b where a :: a a = case s of X -> 0 Y -> [] b :: forall b. [b] :~: a -> b b = case s of X -> \case {} Y -> \Refl -> False f' = \case X -> Foo 0 (\case {}) Y -> Foo [] (\Refl -> False) g, g' :: forall a. Sing a -> Bar a g s = Bar a b where a :: a a = case s of X -> 0 Y -> [] b :: forall b. [b] ~ a => b b = case s of Y -> False g' = \case X -> Bar 0 undefined -- can't make this happy Y -> Bar [] False }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15558 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#15558: Locally handling an empty constraint -------------------------------------+------------------------------------- Reporter: Ericson2314 | Owner: (none) Type: task | Status: new Priority: normal | Milestone: ⊥ Component: Compiler | Version: 8.0.1 Resolution: | Keywords: 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 Ashley Yakeley): Hmm, this seemed to work with 8.4.3: {{{ bar :: Bar Int bar = Bar 0 undefined g' = \case X -> bar Y -> Bar [] False }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15558#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#15558: Locally handling an empty constraint -------------------------------------+------------------------------------- Reporter: Ericson2314 | Owner: (none) Type: task | Status: new Priority: normal | Milestone: ⊥ Component: Compiler | Version: 8.0.1 Resolution: | Keywords: 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 Ashley Yakeley): I've wanted something like this once in the past when I was using preprocessor conditional compilation. Logically, ex falso quodlibet, every type should match with every other type in "inaccessible" code... -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15558#comment:2 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#15558: Locally handling an empty constraint -------------------------------------+------------------------------------- Reporter: Ericson2314 | Owner: (none) Type: task | Status: new Priority: normal | Milestone: ⊥ Component: Compiler | Version: 8.0.1 Resolution: | Keywords: 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: | -------------------------------------+------------------------------------- Description changed by Ericson2314: Old description:
I need something like `\case {}` for constraints. See the code below. There's nothing I can replace the `undefined` with that will satisfy the type checker. The dead code warning also bubbled up out of the field incorrectly.
I think this will require new language features tangentially related to Lambdas for `forall`. (Both `forall _.` and `=>` are invisible quantifiers.) I will link this ticket in that GHC proposal, but am making it's own issue in the first place in case this is a genuine bug that can be fixed by less intrusive means.
{{{ {-# LANGUAGE RankNTypes #-} {-# LANGUAGE EmptyCase #-} {-# LANGUAGE LambdaCase #-} {-# LANGUAGE GADTs #-} {-# LANGUAGE TypeOperators #-} {-# LANGUAGE ScopedTypeVariables #-} module Asdf where
import Data.Kind import Data.Type.Equality
data Sing a where X :: Sing Int Y :: Sing [Bool]
data Foo a = Foo a (forall b. [b] :~: a -> b) data Bar a = Bar a (forall b. [b] ~ a => b)
f, f' :: forall a. Sing a -> Foo a
f s = Foo a b where a :: a a = case s of X -> 0 Y -> [] b :: forall b. [b] :~: a -> b b = case s of X -> \case {} Y -> \Refl -> False
f' = \case X -> Foo 0 (\case {}) Y -> Foo [] (\Refl -> False)
g, g' :: forall a. Sing a -> Bar a
g s = Bar a b where a :: a a = case s of X -> 0 Y -> [] b :: forall b. [b] ~ a => b b = case s of Y -> False
g' = \case X -> Bar 0 undefined -- can't make this happy Y -> Bar [] False
}}}
New description: I need something like `\case {}` for constraints. See the code below. The undefined won't satisfy the type checker, nor is there anything total I found that I could replace it with that would. The dead code warning also bubbled up out of the field incorrectly. I think this will require new language features tangentially related to Lambdas for `forall`. (Both `forall _.` and `=>` are invisible quantifiers.) I will link this ticket in that GHC proposal, but am making it's own issue in the first place in case this is a genuine bug that can be fixed by less intrusive means. {{{ {-# LANGUAGE RankNTypes #-} {-# LANGUAGE EmptyCase #-} {-# LANGUAGE LambdaCase #-} {-# LANGUAGE GADTs #-} {-# LANGUAGE TypeOperators #-} {-# LANGUAGE ScopedTypeVariables #-} module Asdf where import Data.Kind import Data.Type.Equality data Sing a where X :: Sing Int Y :: Sing [Bool] data Foo a = Foo a (forall b. [b] :~: a -> b) data Bar a = Bar a (forall b. [b] ~ a => b) f, f' :: forall a. Sing a -> Foo a f s = Foo a b where a :: a a = case s of X -> 0 Y -> [] b :: forall b. [b] :~: a -> b b = case s of X -> \case {} Y -> \Refl -> False f' = \case X -> Foo 0 (\case {}) Y -> Foo [] (\Refl -> False) g, g' :: forall a. Sing a -> Bar a g s = Bar a b where a :: a a = case s of X -> 0 Y -> [] b :: forall b. [b] ~ a => b b = case s of Y -> False g' = \case X -> Bar 0 undefined -- can't make this happy Y -> Bar [] False }}} -- -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15558#comment:3 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#15558: Locally handling an empty constraint -------------------------------------+------------------------------------- Reporter: Ericson2314 | Owner: (none) Type: task | Status: new Priority: normal | Milestone: ⊥ Component: Compiler | Version: 8.0.1 Resolution: | Keywords: 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: | -------------------------------------+------------------------------------- Description changed by Ericson2314: Old description:
I need something like `\case {}` for constraints. See the code below. The undefined won't satisfy the type checker, nor is there anything total I found that I could replace it with that would. The dead code warning also bubbled up out of the field incorrectly.
I think this will require new language features tangentially related to Lambdas for `forall`. (Both `forall _.` and `=>` are invisible quantifiers.) I will link this ticket in that GHC proposal, but am making it's own issue in the first place in case this is a genuine bug that can be fixed by less intrusive means.
{{{ {-# LANGUAGE RankNTypes #-} {-# LANGUAGE EmptyCase #-} {-# LANGUAGE LambdaCase #-} {-# LANGUAGE GADTs #-} {-# LANGUAGE TypeOperators #-} {-# LANGUAGE ScopedTypeVariables #-} module Asdf where
import Data.Kind import Data.Type.Equality
data Sing a where X :: Sing Int Y :: Sing [Bool]
data Foo a = Foo a (forall b. [b] :~: a -> b) data Bar a = Bar a (forall b. [b] ~ a => b)
f, f' :: forall a. Sing a -> Foo a
f s = Foo a b where a :: a a = case s of X -> 0 Y -> [] b :: forall b. [b] :~: a -> b b = case s of X -> \case {} Y -> \Refl -> False
f' = \case X -> Foo 0 (\case {}) Y -> Foo [] (\Refl -> False)
g, g' :: forall a. Sing a -> Bar a
g s = Bar a b where a :: a a = case s of X -> 0 Y -> [] b :: forall b. [b] ~ a => b b = case s of Y -> False
g' = \case X -> Bar 0 undefined -- can't make this happy Y -> Bar [] False
}}}
New description: I need something like `\case {}` for constraints. See the code below. The `undefined` won't satisfy the type checker, nor is there anything total I found that would. The dead code warning also bubbled up out of the field incorrectly. I think this will require new language features tangentially related to Lambdas for `forall`. (Both `forall _.` and `=>` are invisible quantifiers.) I will link this ticket in that GHC proposal, but am making it's own issue in the first place in case this is a genuine bug that can be fixed by less intrusive means. {{{ {-# LANGUAGE RankNTypes #-} {-# LANGUAGE EmptyCase #-} {-# LANGUAGE LambdaCase #-} {-# LANGUAGE GADTs #-} {-# LANGUAGE TypeOperators #-} {-# LANGUAGE ScopedTypeVariables #-} module Asdf where import Data.Kind import Data.Type.Equality data Sing a where X :: Sing Int Y :: Sing [Bool] data Foo a = Foo a (forall b. [b] :~: a -> b) data Bar a = Bar a (forall b. [b] ~ a => b) f, f' :: forall a. Sing a -> Foo a f s = Foo a b where a :: a a = case s of X -> 0 Y -> [] b :: forall b. [b] :~: a -> b b = case s of X -> \case {} Y -> \Refl -> False f' = \case X -> Foo 0 (\case {}) Y -> Foo [] (\Refl -> False) g, g' :: forall a. Sing a -> Bar a g s = Bar a b where a :: a a = case s of X -> 0 Y -> [] b :: forall b. [b] ~ a => b b = case s of Y -> False g' = \case X -> Bar 0 undefined -- can't make this happy Y -> Bar [] False }}} -- -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15558#comment:4 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#15558: Locally handling an empty constraint -------------------------------------+------------------------------------- Reporter: Ericson2314 | Owner: (none) Type: task | Status: new Priority: normal | Milestone: ⊥ Component: Compiler | Version: 8.0.1 Resolution: | Keywords: 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 RyanGlScott): I'm not quite sure I understand what this ticket is about, but it's worth noting that inaccessible code turned from an error to a warning in GHC 8.6.1, so your code does in fact compile as-is on 8.6.1: {{{ $ /opt/ghc/8.6.1/bin/ghci Bug.hs GHCi, version 8.6.0.20180810: http://www.haskell.org/ghc/ :? for help Loaded GHCi configuration from /home/rgscott/.ghci [1 of 1] Compiling Asdf ( Bug.hs, interpreted ) Bug.hs:49:3: warning: [-Winaccessible-code] • Couldn't match type ‘[b]’ with ‘Int’ Inaccessible code in a pattern with constructor: X :: Sing Int, in a case alternative • In the pattern: X In a case alternative: X -> Bar 0 undefined In the expression: \case X -> Bar 0 undefined Y -> Bar [] False | 49 | X -> Bar 0 undefined -- can't make this happy | ^ }}} Does this satisfy your use case? -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15558#comment:5 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#15558: Locally handling an empty constraint -------------------------------------+------------------------------------- Reporter: Ericson2314 | Owner: (none) Type: task | Status: new Priority: normal | Milestone: ⊥ Component: Compiler | Version: 8.0.1 Resolution: | Keywords: 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 Ericson2314): That's better, but I'd still like to remove the type error and the `undefined`: Being able to write `\ @_ -> undefined` would be better, and if we had a `witnessEq :: a ~ b => a :~ b`, I could do `\ @b -> case witnessEq @[b] @a of {}` which would be better still. Best of all with "absurd constraint lambda-case" would be: {{{ g' = \case X -> Bar 0 (\ @_b -> \@case {}) Y -> Bar [] False }}} Which avoids `witnessEq`. Generalizing to all constraints, that's avoidingg some dictionary singleton thing to do the normal term level empty case by doing empty case on the constraint directly. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15558#comment:6 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#15558: Locally handling an empty constraint -------------------------------------+------------------------------------- Reporter: Ericson2314 | Owner: (none) Type: task | Status: new Priority: normal | Milestone: ⊥ Component: Compiler | Version: 8.0.1 Resolution: | Keywords: 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 Ericson2314): @RyanGlScott Also, I'm a bit queasy with what GHC thinks the inaccessable code is. Is it the entire `X -> Bar 0 ...`, or just the final field? -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15558#comment:7 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#15558: Locally handling an empty constraint -------------------------------------+------------------------------------- Reporter: Ericson2314 | Owner: (none) Type: task | Status: new Priority: normal | Milestone: ⊥ Component: Compiler | Version: 8.0.1 Resolution: | Keywords: 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 RyanGlScott): You're right, there's definitely something fishy going on with this warning. Here's a simplified example: {{{#!hs {-# LANGUAGE GADTs #-} {-# LANGUAGE RankNTypes #-} module Bug where data T a where MkT :: T Int data Foo a = MkFoo ((a ~ Bool) => ()) f :: T a -> Foo a f MkT = MkFoo () g :: Foo Int g = f MkT }}} {{{ $ /opt/ghc/8.6.1/bin/ghci Bug.hs GHCi, version 8.6.0.20180810: http://www.haskell.org/ghc/ :? for help Loaded GHCi configuration from /home/rgscott/.ghci [1 of 1] Compiling Bug ( Bug.hs, interpreted ) Bug.hs:11:3: warning: [-Winaccessible-code] • Couldn't match type ‘Int’ with ‘Bool’ Inaccessible code in a pattern with constructor: MkT :: T Int, in an equation for ‘f’ • In the pattern: MkT In an equation for ‘f’: f MkT = MkFoo () | 11 | f MkT = MkFoo () | ^^^ }}} While there //is// inaccessible code here, the warning is highlighting the wrong spot: it should be the argument to `MkFoo`, not the argument to `f`. (The fact that `g` typechecks at all is a testament to this fact.) I suspect that we're using the wrong `SrcSpan` somewhere in GHC, which causes the reported location to be incorrect. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15558#comment:8 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#15558: Locally handling an empty constraint
-------------------------------------+-------------------------------------
Reporter: Ericson2314 | Owner: (none)
Type: task | Status: new
Priority: normal | Milestone: ⊥
Component: Compiler | Version: 8.0.1
Resolution: | Keywords:
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 Simon Peyton Jones
#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: | -------------------------------------+------------------------------------- Changes (by simonpj): * status: new => closed * testcase: => gadt/T15558 * resolution: => fixed Comment: Good points. Now fixed. For comment:8, the error is now attributed to the `()` argument to `MkFoo` as it should be. Thank you for a nice clean example. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15558#comment:10 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#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 Ericson2314): What about the issue of what to put there when the inaccessible code has an uninhabitted type? Is writing the code with the "type warning" the best one can do? -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15558#comment:11 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#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 simonpj):
Is writing the code with the "type warning" the best one can do?
I don't know. I'd love to improve it further. The patch does the best I can within the current setup -- but doubtless one could do better. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15558#comment:12 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#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 Ericson2314): OK. I guess new syntax for eliminating an uninhabited constraint is indeed needed. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15558#comment:13 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#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
participants (1)
-
GHC