Opened 3 years ago
Last modified 3 years ago
#6065 new bug
Suggested type signature causes a type error (even though it appears correct)
Reported by: | tvynr | Owned by: | |
---|---|---|---|
Priority: | normal | Milestone: | ⊥ |
Component: | Compiler (Type checker) | Version: | 7.4.1 |
Keywords: | type signature typeclass instance forall | Cc: | zep_haskell_trac@…, rpglover64 |
Operating System: | Linux | Architecture: | x86_64 (amd64) |
Type of failure: | GHC rejects valid program | Test Case: | |
Blocked By: | Blocking: | ||
Related Tickets: | Differential Revisions: |
Description
The attached file, MWE.hs, contains an experiment attempting a rudimentary encoding of extensible ASTs in Haskell (without using compdata or a similar package relying upon OverlappingInstances and so forth). The definition of the upcast function appears to be correct. Compiling without a type signature produces a warning and the suggestion to include a type signature. Including the suggested type signature (which appears to be the correct one) causes a type error.
Attachments (2)
Change History (9)
Changed 3 years ago by tvynr
comment:1 Changed 3 years ago by rpglover64
- Cc rpglover64 added
comment:2 Changed 3 years ago by guest
I reduced your test case. The following file compiles, but if inferred type signature to "upcast" is added, it doesn't.
{-# LANGUAGE MultiParamTypeClasses, FlexibleContexts, FlexibleInstances #-} class AstOp ast result where astop :: ast -> result -- upcast :: AstOp ast ((ast -> t) -> t) => ast -> t upcast ast = astop ast upcast
comment:3 Changed 3 years ago by simonpj
- difficulty set to Unknown
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!
comment:4 Changed 3 years ago by simonpj
- Milestone set to _|_
Changed 3 years ago by tvynr
comment:5 Changed 3 years ago by tvynr
Unfortunately, it seems that the reduced example has lost something; applying the typecast to the upcast function in the original MWE.hs (as shown in the newly-attached MWE2.hs) does not work; the same type error is raised. Does MWE2.hs have the appropriate typecast or did I do something wrong?
comment:6 Changed 3 years ago by simonpj
Type variables only scope if you have an explicit forall. So you need
upcast :: forall ast1 ast2. (AstOp HomOp ast1 ((ast1 -> ast2) -> ast2)) => ast1 -> ast2
That compiles fine.
comment:7 Changed 3 years ago by tvynr
Fair point; sorry about that. :) It compiles fine on my machine as well. Thanks for the workaround!
Example Source