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

13 Sep 2015

      #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