Opened 4 years ago

Last modified 4 years ago

#10875 new bug

Unexpected defaulting of partial type signatures and inconsistent behaviour when -fdefer-typed-holes is set.

Reported by: holzensp Owned by:
Priority: normal Milestone:
Component: Compiler Version: 7.10.2
Keywords: PartialTypeSignatures TypedHoles Cc:
Operating System: MacOS X Architecture: x86_64 (amd64)
Type of failure: Incorrect warning at compile-time Test Case:
Blocked By: Blocking:
Related Tickets: Differential Rev(s):
Wiki Page:

Description (last modified by holzensp)

Maybe this should be one bug report and one feature request, but for now, I'll report them together. Consider the following program:

{-#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:

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.

Change History (5)

comment:1 Changed 4 years ago by holzensp

Description: modified (diff)

comment:2 Changed 4 years ago 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:

{-#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:

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!

comment:3 Changed 4 years ago 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 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

comment:4 Changed 4 years ago 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).

comment:5 Changed 4 years ago by holzensp

I found another interesting bit of behaviour, which I would argue is an error. Consider this program:

{-# 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.

Come to think of it, this is probably the exact same bug as the parenthesis-vs-$ case in comment:1.

Last edited 4 years ago by holzensp (previous) (diff)
Note: See TracTickets for help on using tickets.