Opened 2 years ago

Last modified 23 months 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 Difficulty: Unknown
Test Case: Blocked By:
Blocking: Related Tickets:

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)

MWE.hs (2.1 KB) - added by tvynr 2 years ago.
Example Source
MWE2.hs (2.1 KB) - added by tvynr 23 months ago.

Download all attachments as: .zip

Change History (9)

Changed 2 years ago by tvynr

Example Source

comment:1 Changed 2 years ago by rpglover64

  • Cc rpglover64 added

comment:2 Changed 23 months 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 23 months 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 23 months ago by simonpj

  • Milestone set to _|_

Changed 23 months ago by tvynr

comment:5 Changed 23 months 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 23 months 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 23 months ago by tvynr

Fair point; sorry about that. :) It compiles fine on my machine as well. Thanks for the workaround!

Note: See TracTickets for help on using tickets.