#13006: Possible program should type check but does not using Implicit Parameters and Vectors -------------------------------------+------------------------------------- Reporter: clinton | Owner: Type: bug | Status: closed Priority: normal | Milestone: Component: Compiler | Version: 8.0.2-rc2 Resolution: invalid | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: GHC rejects | Unknown/Multiple valid program | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by simonpj): * status: new => closed * resolution: => invalid Comment: In {{{ f _ = let ?v = x in g }}} what type did you expect `f` to have? GHC infers {{{ f :: forall a n. (...) => a -> n () }}} because `g :: forall m. (PrimMonad m, ?v :: T m) => m ()`. (I've used `n` instead of `m` in `f`'s type to emphasise that it is different to `m`. What is the `(...)`? The body of `f` has a call `g`, which gives rise to the constraints `(PrimMonad n, ?v :: T n)`. Alas the `?v` binding in f's RHS binds `?v :: T m` (since `x :: T m`), and that is no help in discharging `?v :: T n`. So we end up with {{{ f :: forall a n. (PrimMonad n, ?v :: T n) => n () }}} and hence the error. By adding the signature you make `f` monomorphic (`-XMonoLocalBinds` has the same effect) which solves the problem. Perhaps we should be more aggressive in reporting an error when functional dependencies can't be satisfied, but I think the program should indeed be rejected. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13006#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler