[GHC] #10875: Unexpected defaulting of partial type signatures and inconsistent behaviour when -fdefer-typed-holes is set.

[GHC]

#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