#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

#11670: Generalisation behaviour of partial type signatures -------------------------------------+------------------------------------- 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 Simon Peyton Jones <simonpj@…>): In [changeset:"15b9bf4ba4ab47e6809bf2b3b36ec16e502aea72/ghc" 15b9bf4b/ghc]: {{{ #!CommitTicketReference repository="ghc" revision="15b9bf4ba4ab47e6809bf2b3b36ec16e502aea72" Improve typechecking of let-bindings This major commit was initially triggered by #11339, but it spiraled into a major review of the way in which type signatures for bindings are handled, especially partial type signatures. On the way I fixed a number of other bugs, namely #12069 #12033 #11700 #11339 #11670 The main change is that I completely reorganised the way in which type signatures in bindings are handled. The new story is in TcSigs Note [Overview of type signatures]. Some specific: * Changes in the data types for signatures in TcRnTypes: TcIdSigInfo and new TcIdSigInst * New module TcSigs deals with typechecking type signatures and pragmas. It contains code mostly moved from TcBinds, which is already too big * HsTypes: I swapped the nesting of HsWildCardBndrs and HsImplicitBndsrs, so that the wildcards are on the oustide not the insidde in a LHsSigWcType. This is just a matter of convenient, nothing deep. There are a host of other changes as knock-on effects, and it all took FAR longer than I anticipated :-). But it is a significant improvement, I think. Lots of error messages changed slightly, some just variants but some modest improvements. New tests * typecheck/should_compile * SigTyVars: a scoped-tyvar test * ExPat, ExPatFail: existential pattern bindings * T12069 * T11700 * T11339 * partial-sigs/should_compile * T12033 * T11339a * T11670 One thing to check: * Small change to output from ghc-api/landmines. Need to check with Alan Zimmerman }}} -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/11670#comment:4> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler