[GHC] #10875: Unexpected defaulting of partial type signatures and inconsistent behaviour when -fdefer-typed-holes is set.
#10875: Unexpected defaulting of partial type signatures and inconsistent behaviour when -fdefer-typed-holes is set. -------------------------------------+------------------------------------- Reporter: holzensp | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.10.2 Keywords: | Operating System: MacOS X PartialTypeSignatures TypedHoles | Architecture: x86_64 | Type of failure: Incorrect (amd64) | warning at compile-time Test Case: | Blocked By: Blocking: | Related Tickets: Differential Revisions: | -------------------------------------+------------------------------------- Maybe this should be one bug report and one feature request, but for now, I'll report them together. Consider the following program: {{{#!hs {-#LANGUAGE PartialTypeSignatures #-} {-#LANGUAGE NamedWildCards #-} {-#LANGUAGE NoMonomorphismRestriction #-} foo :: _ => _outer foo x = round $ (undefined::_inner) (1 + x) }}} This produces the following output in GHCi: {{{ Foo.hs:5:8: Warning: Found hole ‘_’ with inferred constraints: (Integral b, Num a) In the type signature for ‘foo’: _ => _outer Foo.hs:5:13: Warning: Found hole ‘_outer’ with type: a -> b Where: ‘b’ is a rigid type variable bound by the inferred type of foo :: (Integral b, Num a) => a -> b at Foo.hs:6:1 ‘a’ is a rigid type variable bound by the inferred type of foo :: (Integral b, Num a) => a -> b at Foo.hs:6:1 In the type signature for ‘foo’: _ => _outer Foo.hs:6:29: Warning: Found hole ‘_inner’ with type: a -> Double Where: ‘a’ is a rigid type variable bound by the inferred type of foo :: (Integral b, Num a) => a -> b at Foo.hs:6:1 Relevant bindings include x :: a (bound at Foo.hs:6:5) foo :: a -> b (bound at Foo.hs:6:1) In an expression type signature: _inner In the expression: undefined :: _inner In the second argument of ‘($)’, namely ‘(undefined :: _inner) (1 + x)’ Ok, modules loaded: Main. }}} The inferred constraints for `_` (which I can't give a name, unfortunately) and the type reported in place of `_outer` are exactly what I expected. The type for `_inner` surprises me. Okay, the type is ambiguous, so for anything as general as `undefined`, arguably, it would need to default to something. Let's use a typed hole instead of `undefined`: {{{#!hs foo :: _ => _outer foo x = round $ _hole (1 + x) }}} gives {{{ Foo.hs:6:17: Found hole ‘_hole’ with type: a -> Double Where: ‘a’ is a rigid type variable bound by the inferred type of foo :: a -> b at Foo.hs:6:1 Relevant bindings include x :: a (bound at Foo.hs:6:5) foo :: a -> b (bound at Foo.hs:6:1) In the expression: _hole In the second argument of ‘($)’, namely ‘_hole (1 + x)’ In the expression: round $ _hole (1 + x) Failed, modules loaded: none. }}} Holy Guacamole, it still defaults to `Double`. I would consider this a bug, because GHC is telling me, that whatever I put there must result in a `Double`, which is too restrictive to be true. However, I seem to recall from the OutsideIn paper that there were some cases, even without GADTs, where principality was difficult. Was this one of them? Moving on, I was actually trying to get all my holes typed for me in one compiler execution. GHC behaves according to spec; typed holes produce errors by default and when something breaks on an error, it doesn't produce the warnings for partial type signatures. Let's `-fdefer-typed- holes` and compile again: {{{ Prelude> :set -fdefer-typed-holes Prelude> :r [1 of 1] Compiling Main ( Foo.hs, interpreted ) Foo.hs:5:8: Warning: Found hole ‘_’ with inferred constraints: () In the type signature for ‘foo’: _ => _outer Foo.hs:5:13: Warning: Found hole ‘_outer’ with type: a -> b Where: ‘b’ is a rigid type variable bound by the inferred type of foo :: a -> b at Foo.hs:6:1 ‘a’ is a rigid type variable bound by the inferred type of foo :: a -> b at Foo.hs:6:1 In the type signature for ‘foo’: _ => _outer Foo.hs:6:17: Warning: Found hole ‘_hole’ with type: a -> Double Where: ‘a’ is a rigid type variable bound by the inferred type of foo :: a -> b at Foo.hs:6:1 Relevant bindings include x :: a (bound at Foo.hs:6:5) foo :: a -> b (bound at Foo.hs:6:1) In the expression: _hole In the second argument of ‘($)’, namely ‘_hole (1 + x)’ In the expression: round $ _hole (1 + x) Ok, modules loaded: Main. }}} Surely, this must be wrong. Suddenly `()` is the inferred set of constraints and an unconstrained `a -> b` will do for `_outer`. I would argue that the `1 +` still demainds `Num a`, even if `round`'s `RealFrac` constraint is satisfied by `_hole` producing a `Double`. As said, maybe the erroneous types reported when `-fdefer-typed-holes` are a separate issue from the type of `_hole` not being the principal type, but I'm unsure, so I reported them together. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10875 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#10875: Unexpected defaulting of partial type signatures and inconsistent behaviour when -fdefer-typed-holes is set. -------------------------------------+------------------------------------- Reporter: holzensp | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.10.2 Resolution: | Keywords: | PartialTypeSignatures TypedHoles Operating System: MacOS X | Architecture: x86_64 Type of failure: Incorrect | (amd64) warning at compile-time | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Revisions: -------------------------------------+------------------------------------- Description changed by holzensp: Old description:
Maybe this should be one bug report and one feature request, but for now, I'll report them together. Consider the following program: {{{#!hs {-#LANGUAGE PartialTypeSignatures #-} {-#LANGUAGE NamedWildCards #-} {-#LANGUAGE NoMonomorphismRestriction #-}
foo :: _ => _outer foo x = round $ (undefined::_inner) (1 + x) }}} This produces the following output in GHCi: {{{ Foo.hs:5:8: Warning: Found hole ‘_’ with inferred constraints: (Integral b, Num a) In the type signature for ‘foo’: _ => _outer
Foo.hs:5:13: Warning: Found hole ‘_outer’ with type: a -> b Where: ‘b’ is a rigid type variable bound by the inferred type of foo :: (Integral b, Num a) => a -> b at Foo.hs:6:1 ‘a’ is a rigid type variable bound by the inferred type of foo :: (Integral b, Num a) => a -> b at Foo.hs:6:1 In the type signature for ‘foo’: _ => _outer
Foo.hs:6:29: Warning: Found hole ‘_inner’ with type: a -> Double Where: ‘a’ is a rigid type variable bound by the inferred type of foo :: (Integral b, Num a) => a -> b at Foo.hs:6:1 Relevant bindings include x :: a (bound at Foo.hs:6:5) foo :: a -> b (bound at Foo.hs:6:1) In an expression type signature: _inner In the expression: undefined :: _inner In the second argument of ‘($)’, namely ‘(undefined :: _inner) (1 + x)’ Ok, modules loaded: Main. }}} The inferred constraints for `_` (which I can't give a name, unfortunately) and the type reported in place of `_outer` are exactly what I expected. The type for `_inner` surprises me. Okay, the type is ambiguous, so for anything as general as `undefined`, arguably, it would need to default to something.
Let's use a typed hole instead of `undefined`: {{{#!hs foo :: _ => _outer foo x = round $ _hole (1 + x) }}} gives {{{ Foo.hs:6:17: Found hole ‘_hole’ with type: a -> Double Where: ‘a’ is a rigid type variable bound by the inferred type of foo :: a -> b at Foo.hs:6:1 Relevant bindings include x :: a (bound at Foo.hs:6:5) foo :: a -> b (bound at Foo.hs:6:1) In the expression: _hole In the second argument of ‘($)’, namely ‘_hole (1 + x)’ In the expression: round $ _hole (1 + x) Failed, modules loaded: none. }}} Holy Guacamole, it still defaults to `Double`. I would consider this a bug, because GHC is telling me, that whatever I put there must result in a `Double`, which is too restrictive to be true. However, I seem to recall from the OutsideIn paper that there were some cases, even without GADTs, where principality was difficult. Was this one of them?
Moving on, I was actually trying to get all my holes typed for me in one compiler execution. GHC behaves according to spec; typed holes produce errors by default and when something breaks on an error, it doesn't produce the warnings for partial type signatures. Let's `-fdefer-typed- holes` and compile again: {{{ Prelude> :set -fdefer-typed-holes Prelude> :r [1 of 1] Compiling Main ( Foo.hs, interpreted )
Foo.hs:5:8: Warning: Found hole ‘_’ with inferred constraints: () In the type signature for ‘foo’: _ => _outer
Foo.hs:5:13: Warning: Found hole ‘_outer’ with type: a -> b Where: ‘b’ is a rigid type variable bound by the inferred type of foo :: a -> b at Foo.hs:6:1 ‘a’ is a rigid type variable bound by the inferred type of foo :: a -> b at Foo.hs:6:1 In the type signature for ‘foo’: _ => _outer
Foo.hs:6:17: Warning: Found hole ‘_hole’ with type: a -> Double Where: ‘a’ is a rigid type variable bound by the inferred type of foo :: a -> b at Foo.hs:6:1 Relevant bindings include x :: a (bound at Foo.hs:6:5) foo :: a -> b (bound at Foo.hs:6:1) In the expression: _hole In the second argument of ‘($)’, namely ‘_hole (1 + x)’ In the expression: round $ _hole (1 + x) Ok, modules loaded: Main. }}} Surely, this must be wrong. Suddenly `()` is the inferred set of constraints and an unconstrained `a -> b` will do for `_outer`. I would argue that the `1 +` still demainds `Num a`, even if `round`'s `RealFrac` constraint is satisfied by `_hole` producing a `Double`.
As said, maybe the erroneous types reported when `-fdefer-typed-holes` are a separate issue from the type of `_hole` not being the principal type, but I'm unsure, so I reported them together.
New description: Maybe this should be one bug report and one feature request, but for now, I'll report them together. Consider the following program: {{{#!hs {-#LANGUAGE PartialTypeSignatures #-} {-#LANGUAGE NamedWildCards #-} {-#LANGUAGE NoMonomorphismRestriction #-} foo :: _ => _outer foo x = round $ (undefined::_inner) (1 + x) }}} This produces the following output in GHCi: {{{ Foo.hs:5:8: Warning: Found hole ‘_’ with inferred constraints: (Integral b, Num a) In the type signature for ‘foo’: _ => _outer Foo.hs:5:13: Warning: Found hole ‘_outer’ with type: a -> b Where: ‘b’ is a rigid type variable bound by the inferred type of foo :: (Integral b, Num a) => a -> b at Foo.hs:6:1 ‘a’ is a rigid type variable bound by the inferred type of foo :: (Integral b, Num a) => a -> b at Foo.hs:6:1 In the type signature for ‘foo’: _ => _outer Foo.hs:6:29: Warning: Found hole ‘_inner’ with type: a -> Double Where: ‘a’ is a rigid type variable bound by the inferred type of foo :: (Integral b, Num a) => a -> b at Foo.hs:6:1 Relevant bindings include x :: a (bound at Foo.hs:6:5) foo :: a -> b (bound at Foo.hs:6:1) In an expression type signature: _inner In the expression: undefined :: _inner In the second argument of ‘($)’, namely ‘(undefined :: _inner) (1 + x)’ Ok, modules loaded: Main. }}} The inferred constraints for `_` (which I can't give a name, unfortunately) and the type reported in place of `_outer` are exactly what I expected. The type for `_inner` surprises me. Okay, the type is ambiguous, so for anything as general as `undefined`, arguably, it would need to default to something. Let's use a typed hole instead of `undefined`: {{{#!hs foo :: _ => _outer foo x = round $ _hole (1 + x) }}} gives {{{ Foo.hs:6:17: Found hole ‘_hole’ with type: a -> Double Where: ‘a’ is a rigid type variable bound by the inferred type of foo :: a -> b at Foo.hs:6:1 Relevant bindings include x :: a (bound at Foo.hs:6:5) foo :: a -> b (bound at Foo.hs:6:1) In the expression: _hole In the second argument of ‘($)’, namely ‘_hole (1 + x)’ In the expression: round $ _hole (1 + x) Failed, modules loaded: none. }}} Holy Guacamole, it still defaults to `Double`. I would consider this a bug, because GHC is telling me, that whatever I put there must result in a `Double`, which is too restrictive to be true. However, I seem to recall from the OutsideIn paper that there were some cases, even without GADTs, where principality was difficult. Was this one of them? Moving on, I was actually trying to get all my holes typed for me in one compiler execution. GHC behaves according to spec; typed holes produce errors by default and when something breaks on an error, it doesn't produce the warnings for partial type signatures. Let's `-fdefer-typed- holes` and compile again: {{{ Prelude> :set -fdefer-typed-holes Prelude> :r [1 of 1] Compiling Main ( Foo.hs, interpreted ) Foo.hs:5:8: Warning: Found hole ‘_’ with inferred constraints: () In the type signature for ‘foo’: _ => _outer Foo.hs:5:13: Warning: Found hole ‘_outer’ with type: a -> b Where: ‘b’ is a rigid type variable bound by the inferred type of foo :: a -> b at Foo.hs:6:1 ‘a’ is a rigid type variable bound by the inferred type of foo :: a -> b at Foo.hs:6:1 In the type signature for ‘foo’: _ => _outer Foo.hs:6:17: Warning: Found hole ‘_hole’ with type: a -> Double Where: ‘a’ is a rigid type variable bound by the inferred type of foo :: a -> b at Foo.hs:6:1 Relevant bindings include x :: a (bound at Foo.hs:6:5) foo :: a -> b (bound at Foo.hs:6:1) In the expression: _hole In the second argument of ‘($)’, namely ‘_hole (1 + x)’ In the expression: round $ _hole (1 + x) Ok, modules loaded: Main. }}} Surely, this must be wrong. Suddenly `()` is the inferred set of constraints and an unconstrained `a -> b` will do for `_outer`. I would argue that the `1 +` still demainds `Num a` and that `round` still requires an instance of `Integral b`, even if `round`'s `RealFrac` constraint is satisfied by `_hole` producing a `Double`. As said, maybe the erroneous types reported when `-fdefer-typed-holes` are a separate issue from the type of `_hole` not being the principal type, but I'm unsure, so I reported them together. -- -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10875#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#10875: Unexpected defaulting of partial type signatures and inconsistent behaviour when -fdefer-typed-holes is set. -------------------------------------+------------------------------------- Reporter: holzensp | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.10.2 Resolution: | Keywords: | PartialTypeSignatures TypedHoles Operating System: MacOS X | Architecture: x86_64 Type of failure: Incorrect | (amd64) warning at compile-time | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Revisions: -------------------------------------+------------------------------------- Comment (by holzensp): I just realised that the above loss of the `RealFrac` constraint, may well be because GHC has nowhere to put it. I tried `(undefined::_ => _inner)`, but it seems the constraints hole is only used at top-level (i.e. GHC didn't output any message for this `_`). A further attempt using `ImplicitParams` also gave unexpected results. Consider this program: {{{#!hs {-#LANGUAGE NoMonomorphismRestriction #-} {-#LANGUAGE PartialTypeSignatures #-} {-#LANGUAGE NamedWildCards #-} {-#LANGUAGE ImplicitParams #-} foo :: _ => _outer foo x = round (?hole (1 + x)) }}} which yields {{{ Foo.hs:6:8: Warning: Found hole ‘_’ with inferred constraints: (Integral b, Num a, RealFrac a, ?hole::a -> a) In the type signature for ‘foo’: _ => _outer Foo.hs:6:13: Warning: Found hole ‘_outer’ with type: a1 -> b Where: ‘b’ is a rigid type variable bound by the inferred type of foo :: (Integral b, Num a1, RealFrac a, ?hole::a1 -> a) => a1 -> b at Foo.hs:7:1 ‘a1’ is a rigid type variable bound by the inferred type of foo :: (Integral b, Num a1, RealFrac a, ?hole::a1 -> a) => a1 -> b at Foo.hs:7:1 In the type signature for ‘foo’: _ => _outer Ok, modules loaded: Main. }}} Notice how the first message, regarding `_` is too restrictive, by demanding that `?hole::a -> a`. However, the second message is more general, stating `?hole::a1 -> a`. Could this just be a pretty printer issue, where the first message discards the subscript of the type variable? Another surprise occurs when I remove the parenthesis and use `$` instead: {{{#!hs foo x = round $ ?hole (1 + x) }}} results in {{{ Foo.hs:6:8: Warning: Found hole ‘_’ with inferred constraints: (Integral b, Num a, RealFrac r, ?hole::a -> r) In the type signature for ‘foo’: _ => _outer Foo.hs:6:13: Warning: Found hole ‘_outer’ with type: a -> b Where: ‘b’ is a rigid type variable bound by the inferred type of foo :: (Integral b, Num a, RealFrac r, ?hole::a -> r) => a -> b at Foo.hs:7:1 ‘a’ is a rigid type variable bound by the inferred type of foo :: (Integral b, Num a, RealFrac r, ?hole::a -> r) => a -> b at Foo.hs:7:1 In the type signature for ‘foo’: _ => _outer Ok, modules loaded: Main. }}} This is the result I was looking for! -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10875#comment:2 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#10875: Unexpected defaulting of partial type signatures and inconsistent behaviour when -fdefer-typed-holes is set. -------------------------------------+------------------------------------- Reporter: holzensp | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.10.2 Resolution: | Keywords: | PartialTypeSignatures TypedHoles Operating System: MacOS X | Architecture: x86_64 Type of failure: Incorrect | (amd64) warning at compile-time | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Revisions: -------------------------------------+------------------------------------- Comment (by simonpj): Interesting examples, thank you! As it happens I am in mid-flight on a significant refactoring of the wildcard implementation, so I'd like to park these examples and come back to them when I commit. It has turned out to be a much bigger job than I anticipated, I'm afraid. Just on the narrow question of defaulting, I think it's not unreasonable that wildcards don't affect type-class defaulting (i.e. in ambiguous cases, choose a particular type to fix the type, see [https://www.haskell.org/onlinereport/haskell2010/haskellch4.html#x10-750004.... 4.3.4 in the language definition]. Wouldn't people complain if adding wildcards changed the typing rules? Can you specify ''precisely'' what the new defaulting rules would then be? Simon -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10875#comment:3 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#10875: Unexpected defaulting of partial type signatures and inconsistent behaviour when -fdefer-typed-holes is set. -------------------------------------+------------------------------------- Reporter: holzensp | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.10.2 Resolution: | Keywords: | PartialTypeSignatures TypedHoles Operating System: MacOS X | Architecture: x86_64 Type of failure: Incorrect | (amd64) warning at compile-time | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Revisions: -------------------------------------+------------------------------------- Comment (by holzensp): If you're done with the refactoring and want someone to help test, by all means let me know. I see your point with regards to the defaulting rule from the language definition. In light of the typing rules, I'm unsure whether I would consider a typed hole to be like any other term. With a variable-typed term, like `undefined`, I agree that the typing rules should find ''whatever'' type satisfies. My interpretation of a typed hole, however, is that I'm asking GHC: "Please tell me what you expect me to put in here." After typing up my comment, though, I understand that `RealFrac b => a_bound_by_the_type_of_foo -> b` actually is not the correct type, because `round` actually binds `b`. In other words, it's not just that `round` imposes a `RealFrac` constraint on `b`, but the `b` of the hole should be precisely the same `b` as that of `round`. Somehow it should be something like `RealFrac b_bound_by_the_type_of_round => a_bound_by_the_type_of_foo -> b_bound_by_the_type_of_round`. I admit it's complicated, but purely from a TypedHoles user perspective, I think defaulting is... less then intuitive (fully aware of the subjectivity of that term). -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10875#comment:4 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#10875: Unexpected defaulting of partial type signatures and inconsistent behaviour when -fdefer-typed-holes is set. -------------------------------------+------------------------------------- Reporter: holzensp | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.10.2 Resolution: | Keywords: | PartialTypeSignatures TypedHoles Operating System: MacOS X | Architecture: x86_64 Type of failure: Incorrect | (amd64) warning at compile-time | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): -------------------------------------+------------------------------------- Comment (by holzensp): I found another interesting bit of behaviour, which I would argue is an error. Consider this program: {{{#!hs {-# LANGUAGE NoMonomorphismRestriction #-} {-# LANGUAGE PartialTypeSignatures #-} {-# LANGUAGE NamedWildCards #-} {-# LANGUAGE ImplicitParams #-} module Foo where foo :: _ => _outer foo = (+) ?a ?b ?c ?d }}} This produces the following output in GHCi: {{{ [1 of 1] Compiling Foo ( Foo.hs, interpreted ) Foo.hs:7:8: Warning: Found hole ‘_’ with inferred constraints: (Num (t -> t -> w_outer), ?a::t -> t -> w_outer, ?b::t -> t -> w_outer, ?c::t, ?d::t) In the type signature for ‘foo’: _ => _outer Foo.hs:7:13: Warning: Found hole ‘_outer’ with type: w_outer Where: ‘w_outer’ is a rigid type variable bound by the inferred type of foo :: (Num (t -> t1 -> w_outer), ?a::t -> t1 -> w_outer, ?b::t -> t1 -> w_outer, ?c::t, ?d::t1) => w_outer at Foo.hs:8:1 In the type signature for ‘foo’: _ => _outer Ok, modules loaded: Foo. }}} I would say the second warning is accurate, but in the first warning, the `t1` type variables are printed as `t`, which is too restrictive. Considering the validity of the second warning, I would say this is probably a ppr-bug. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10875#comment:5 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
participants (1)
-
GHC