#8739 closed bug (fixed)

($) returning kind # no longer type checks

Reported by: NeilMitchell Owned by:
Priority: normal Milestone: 7.8.1
Component: Compiler Version: 7.8.1-rc1
Keywords: Cc: ndmitchell@…, jwlato@…, mail@…, slyfox@…
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: None/Unknown Test Case: typecheck/should_run/T8739
Blocked By: Blocking:
Related Tickets: Differential Revisions:

Description

Given:

{-# LANGUAGE MagicHash #-}
module InnerLoop(go) where
import GHC.Exts
go :: () -> Int#
go () = go $ ()

This type checks fine on GHC 7.2.3, and I have a similar version that works fine with 7.4 and 7.6. However, with GHC 7.8.20140130, I get:

InnerLoop.hs:5:9:
    Kind incompatibility when matching types:
      s0 :: *
      Int# :: #
    In the expression: go $ ()
    In an equation for `go': go () = go $ ()

This code was reduced from this blog post, and code which triggers a similar bug can be found in Shake.

I know $ has special type checking rules, were they removed or changed?

Change History (9)

comment:1 Changed 19 months ago by jwlato

  • Cc jwlato@… added

comment:2 Changed 19 months ago by nh2

  • Cc mail@… added

comment:3 Changed 19 months ago by slyfox

  • Cc slyfox@… added

comment:4 Changed 19 months ago by thoughtpolice

  • Milestone set to 7.8.1

comment:5 Changed 19 months ago by goldfire

  • Status changed from new to infoneeded

The fact that this code worked in <= 7.2 is a bug: #5570. I was unable to get the example above to compile on 7.4.2 or 7.6.3. Do you have an example that works with these versions but fails with 7.8?

And, yes, the fix to #5570 did change the typing rules for ($), but seemingly in a good way.

comment:6 Changed 19 months ago by simonpj

It's absolutely right that the second argument to ($) must not have an unboxed kind. Because the code for ($) must move that argument around (pass to the function), so it must know its width, pointerhood ect.

But actually it would be ok for the result of the call (f $ x) to be unboxed, because the code for ($) doesn't mess with the result; it just tail-calls f.

It's a bit like the call (error "foo") which is allowed to have an unboxed type. So error has a rather magical type

error :: forall (a:OpenKind). String -> a

where the funny quantifier a:OpenKind allows a to be instantiated to Int# as well as to Int.

So we could regard ($) as having the type

($) :: forall (a:*) (r:OpenKind). (a->r) -> a -> r

reflecting the fact that the result kind can range over unboxed types.

Unless I'm being stupid here, the fix is simple in TcExpr, lines 329-ish:

  • Remove b_ty <- newPolyFlexiTyVarTy
  • Remove the unifyType op_res_ty b_ty
  • Replace the other reference to b_ty with op_res_ty

Would someone like to try? Of course this deserves an elaboration of Note [Typing rule for ($)], and a reference to this ticket.

Simon

comment:7 Changed 19 months ago by Simon Peyton Jones <simonpj@…>

In 5dd1cbbfc0a19e92d7eeff6f328abc7558992fd6/ghc:

Allow ($) to return an unlifted type (Trac #8739)

Since ($) simply returns its result, via a tail call, it can
perfectly well have an unlifted result type; e.g.
    foo $ True    where  foo :: Bool -> Int#
should be perfectly fine.

This used to work in GHC 7.2, but caused a Lint failure.  This patch
makes it work again (which involved removing code in TcExpr), but fixing
the Lint failure meant I had to make ($) into a wired-in Id.  Which
is not hard to do (in MkId).

comment:8 Changed 19 months ago by simonpj

  • Status changed from infoneeded to merge
  • Test Case set to typecheck/should_run/T8739

OK I've done this. Since ($) has a special typing rule anyway, it may as well be very special!

Simon

PS: Although 7.2 allowed it, if you used -dcore-lint it was rejected. I've fixed that too.

comment:9 Changed 19 months ago by thoughtpolice

  • Resolution set to fixed
  • Status changed from merge to closed

Merged.

Note: See TracTickets for help on using tickets.