Opened 3 years ago

Closed 2 years ago

Last modified 2 years ago

#10194 closed bug (fixed)

Shouldn't this require ImpredicativeTypes?

Reported by: kosmikus Owned by:
Priority: highest Milestone: 8.0.1
Component: Compiler (Type checker) Version: 7.8.4
Keywords: Cc: adamgundry, jstolarek, dfeuer
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: GHC accepts invalid program Test Case: typecheck/should_fail/T10194
Blocked By: Blocking:
Related Tickets: Differential Rev(s):
Wiki Page:

Description

The following program compiles:

{-# LANGUAGE RankNTypes #-}
module TestRN1 where

type X = forall a . a

comp :: (X -> c) -> (a -> X) -> (a -> c)
comp = (.)

But this one fails:

{-# LANGUAGE RankNTypes #-}
module TestRN2 where

comp :: ((forall a . a) -> c) -> (a -> (forall a . a)) -> (a -> c)
comp = (.)

Error:

    Cannot instantiate unification variable ‘b0’
    with a type involving foralls: forall a1. a1
      Perhaps you want ImpredicativeTypes
    In the expression: (.)
    In an equation for ‘comp’: comp = (.)

I would expect both to fail. Both seem to rely on impredicative types. I wouldn't expect expansion of a type synonym to make a difference between a type-checking program and one that does not typecheck.

Change History (18)

comment:1 Changed 3 years ago by adamgundry

Cc: adamgundry added

comment:2 Changed 3 years ago by jstolarek

Cc: jstolarek added

comment:3 Changed 3 years ago by dfeuer

Cc: dfeuer added

comment:4 Changed 3 years ago by Simon Peyton Jones <simonpj@…>

In 553c5182156c5e4c15e3bd1c17c6d83a95a6c408/ghc:

Look inside synonyms for foralls when unifying

This fixes Trac #10194

comment:5 Changed 3 years ago by simonpj

Status: newmerge
Test Case: typecheck/should_fail/T10194

Excellent point. Fixed.

(I doubt this is worth the trouble of merging to 7.10.2, but could be.)

Simon

comment:6 Changed 3 years ago by thoughtpolice

Milestone: 7.10.2
Resolution: fixed
Status: mergeclosed

comment:7 Changed 2 years ago by refold

Apparently this fix means that some programs that compiled with 7.10.1 now fail with 7.10.2. One reported example is xmonad-contrib.

comment:8 Changed 2 years ago by simonpj

Status: closedmerge

OK, Ben can you try to merge this?

comment:9 Changed 2 years ago by thoughtpolice

But it's already merged; should we un-merge it?

comment:10 Changed 2 years ago by adamgundry

@refold can you be more specific about what breaks? One would expect some programs that were previously (erroneously) accepted to now require -XImpredicativeTypes. That's not necessarily a reason to revert this patch.

comment:11 in reply to:  10 Changed 2 years ago by refold

Replying to adamgundry:

One would expect some programs that were previously (erroneously) accepted to now require -XImpredicativeTypes.

Yes, that's what seems to happen in the xmonad-contrib case:

XMonad/Layout/Groups/Helpers.hs:181:8:
    Cannot instantiate unification variable `a0'
    with a type involving foralls: G.ModifySpec
    Perhaps you want ImpredicativeTypes
    In the expression: sendMessage . G.Modify
    In an equation for `wrap': wrap = sendMessage . G.Modify

XMonad/Layout/Groups/Helpers.hs:181:22:
    Cannot instantiate unification variable `a0'
    with a type involving foralls: G.ModifySpec
    Perhaps you want ImpredicativeTypes
    In the second argument of `(.)', namely `G.Modify'
    In the expression: sendMessage . G.Modify

That's not necessarily a reason to revert this patch.

The issue doesn't affect me personally, so I'm not going to argue. My comment was JFYI.

comment:12 Changed 2 years ago by adamgundry

Thanks! Indeed, those look like impredicative instantiations of (.) that should require ImpredicativeTypes. I think we should keep the patch, and flag up this issue in the release notes, although the error message makes it fairly obvious how to fix the problem. :-)

Or should we be more concerned about maintaining support for existing programs, given that this is a bugfix release?

comment:13 Changed 2 years ago by simonpj

Well this _is_ a bugfix! It's just that fixing the bug makes some programs be rejected that should be rejected. I propose that we keep it.

Simon

comment:14 Changed 2 years ago by nomeata

Or should we be more concerned about maintaining support for existing programs, given that this is a bugfix release?

As a user, I would be upset if a bugfix release of a compiler suddenly stops compiling programs that it was compiling previously (unless the compilation was producing bogus results before, but that is not the case here, I believe).

comment:15 Changed 2 years ago by goldfire

Though I am not at all affected by this, I agree with Joachim (nomeata). I think this sort of wibble in a patch release just makes users groan, and for no great reason beyond pedantry. (I'm not using pedantry negatively there, as doing so would be quite hypocritical, but that really is the only reason for this change.)

I propose unmerging but surely keeping the fix in master. It is a bugfix, but just not one that needs to be released at the moment.

comment:16 Changed 2 years ago by simonpj

Priority: normalhighest

OK fair enough. Un-merging is fine with me.

Simon

comment:17 Changed 2 years ago by thoughtpolice

Milestone: 7.10.27.12.1
Status: mergeclosed

Reverted in 8fb101e49b86c0f8bb8931620c9c3cd3e6c57228 on ghc-7.10.

comment:18 Changed 2 years ago by thoughtpolice

Milestone: 7.12.18.0.1

Milestone renamed

Note: See TracTickets for help on using tickets.