#6065: Suggested type signature causes a type error (even though it appears
correct)
---------------------------------------------------------+------------------
Reporter: tvynr | Owner:
Type: bug | Status: new
Priority: normal | Milestone:
Component: Compiler (Type checker) | Version: 7.4.1
Keywords: type signature typeclass instance forall | Os: Linux
Architecture: x86_64 (amd64) | Failure: GHC rejects valid program
Difficulty: Unknown | Testcase:
Blockedby: | Blocking:
Related: |
---------------------------------------------------------+------------------
Changes (by simonpj):
* difficulty: => Unknown
Comment:
Generally speaking GHC is now much better about ''not'' suggesting a type
signature that then doesn't work. But it's not perfect and there's a good
reason for that. Here's why, if you care, but partly just to record the
thinking in the ticket.
I'll use a yet-simpler example that demonstrates the problem
{{{
{-# LANGUAGE MultiParamTypeClasses, FlexibleContexts, FlexibleInstances
#-}
module T6065 where
class AstOp a b where
astop :: a -> b -> Int
-- upcast :: AstOp a (a -> Int) => a -> Int
upcast ast = astop ast upcast
}}}
When GHC typechecks the RHS of `upcast` it provisionally gives `upcast`
the (monomorphic) type `upcast :: alpha -> beta`, where `alpha` and `beta`
are fresh unification variables. Then it typechecks the RHS of `upcast`,
getting
{{{
(\ast -> astop ast upcast)
Type :: alpha -> Int
Constraint :: AstOp alpha (alpha -> Int)
(arising from the call to 'astop')
}}}
(`beta` gets unified to `Int`.) Now it generalises that type to get
{{{
upcast :: forall c. AstOp c (c -> Int) => c -> Int
}}}
And that is the type GHE suggests:
{{{
T6065.hs:9:1: Warning:
Top-level binding with no type signature:
upcast :: forall a. AstOp a (a -> Int) => a -> Int
}}}
BUT if we ''provide'' this type signature, and then re-type-check the
entire definition, we typecheck it with `upcast` having the above
''polymorphic'' type, NOT the old ''monomorphic'' type. So the recursive
call to `upcast` is instantiated by instantiating `c` with a fresh unknown
type, say `gamma`.
So we get this:
{{{
(\ast -> astop ast upcast)
Type :: alpha -> beta
Constraint :: AstOp alpha (gamma -> Int)
(arising from the call to 'astop')
AstOp gamma (gamma -> Int)
(arising from the recursive call to 'upcast')
}}}
And we can't solve these from the given constraint `(AstOp alpha (alpha ->
Int))`, because nothing forces `gamma` and `alpha` to be unified.
The problem is that when the recursive call is polymorphic, we get more
unknown types (arising from instantiating the type variables of the
recursive call to `upcast`). We can fix that with a type signature such as
{{{
upcast :: forall a. AstOp a (a -> Int) => a -> Int
upcast ast = astop ast (upcast :: a -> Int)
}}}
where the type signature on the RHS fixes `gamma`. (Needs
`ScopedTypeVariables`.)
But that is not the point. The point is that it's very unhelpful for GHC
to suggest a type that doesn't work. But
* Even realising that the suggested type doesn't work requires re-
generating the constraints from scratch, which is a major (and non-linear)
pain.
* Even if we knew that the suggested type didn't work, it's not clear
what complaint to give.
So I'm a bit stuck here, and for now I propose to do nothing. Nice bug
report though!
--
Ticket URL: <
http://hackage.haskell.org/trac/ghc/ticket/6065#comment:3>
GHC <
http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler
_______________________________________________
Glasgow-haskell-bugs mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/glasgow-haskell-bugs
Locked
