[GHC] #11670: Can't infer type

[GHC]

#11670: Can't infer type
-------------------------------------+-------------------------------------
        Reporter:  Iceland_jack      |                Owner:
            Type:  bug               |               Status:  new
        Priority:  normal            |            Milestone:
       Component:  Compiler          |              Version:  7.10.3
      Resolution:                    |             Keywords:
Operating System:  Unknown/Multiple  |         Architecture:
                                     |  Unknown/Multiple
 Type of failure:  None/Unknown      |            Test Case:
      Blocked By:                    |             Blocking:
 Related Tickets:                    |  Differential Rev(s):
       Wiki Page:                    |
-------------------------------------+-------------------------------------

Comment (by simonpj):

 Well this is confusing, I agree.  It's useful to open up the question of
 what partial type signatures mean.  Remember
 {{{
 castPtr :: Ptr a -> Ptr b
 peekElemOff :: Storable a => Ptr a -> Int -> IO a
 }}}
 So what is the type of the sub-expression `peekElemOff (castPtr ptr) 0`?
 Clearly it is
 {{{
 peekElemOff (castPtr ptr) :: forall a. Storable a => IO a
 }}}
 If, in the program in comment:1, we had tried this
 {{{
   peekElemOff (castPtr ptr) 0 :: IO a
 }}}
 we would clearly expect the error message above, because that means
 {{{
   peekElemOff (castPtr ptr) 0 :: forall a. IO a
 }}}
 and the sub-expression doesn't have that type.

 So what do we expect when we write
 {{{
   peekElemOff (castPtr ptr) 0 :: IO _
 }}}
 You intended "don't generalise this; just substitute `CLong` for `_`".
 But we ''do'' generalise even partial signatures.

 I did toy with ''not'' generalising partial signatures.  So if you wrote
 {{{
  f :: _ -> a -> _
 }}}
 that would mean
 {{{
  f :: forall a. _ -> a -> _
 }}}
 and the `_` might get filled in with `a` or with `Int` or perhaps with
 some other type -- ''but it would not be generalised''.  So if I wrote
 {{{
  f :: _ -> _
  f x = x
 }}}
 I'd get a ''monomorphic'' identity function, not a polymorphic one.  Is
 that what we expect?  On the whole I think that would be better.  What do
 you think?

 However currently I ''do'' generalise those wildcards, for reasons
 explained towards the end of this Note. Maybe we should revisit this
 decision?
 {{{
 {- Note [Which type variables to quantify]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 When choosing type variables to quantify, the basic plan is to
 quantify over all type variables that are
  * free in the tau_tvs, and
  * not forced to be monomorphic (mono_tvs),
    for example by being free in the environment.

 However, for a pattern binding, or with wildcards, we might
 be doing inference *in the presence of a type signature*.
 Mostly, if there is a signature we use CheckGen, not InferGen,
 but with pattern bindings or wildcards we might do InferGen
 and still have a type signature.  For example:
    f :: _ -> a
    f x = ...
 or
    g :: (Eq _a) => _b -> _b
 or
    p :: a -> a
    (p,q) = e
 In all these cases we use plan InferGen, and hence call simplifyInfer.
 But those 'a' variables are skolems, and we should be sure to quantify
 over them, regardless of the monomorphism restriction etc.  If we
 don't, when reporting a type error we panic when we find that a
 skolem isn't bound by any enclosing implication.

 Moreover we must quantify over all wildcards that are not free in
 the environment.  In the case of 'g' for example, silly though it is,
 we want to get the inferred type
    g :: forall t. Eq t => Int -> Int
 and then report ambiguity, rather than *not* quantifying over 't'
 and getting some much more mysterious error later.  A similar case
 is
   h :: F _a -> Int

 That's why we pass sigs to simplifyInfer, and make sure (in
 quantify_tvs) that we do quantify over them.  Trac #10615 is
 a case in point.
 }}}

--
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/11670#comment:2>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler