Opened 14 months ago

Last modified 8 months ago

#12652 new bug

Type checker no longer accepting code using function composition and rank-n types

Reported by: ezyang Owned by: simonpj
Priority: normal Milestone: 8.4.1
Component: Compiler (Type checker) Version: 8.1
Keywords: Cc: simonpj
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: None/Unknown Test Case:
Blocked By: Blocking:
Related Tickets: Differential Rev(s):
Wiki Page:

Description (last modified by bgamari)

The following program (reduced from Cabal code that uses HasCallStack) typechecks in GHC 8.0, but not on HEAD:

{-# LANGUAGE RankNTypes #-} 
{-# LANGUAGE ImplicitParams #-} 
module Foo where 

type T a = (?x :: Int) => a 
type M a = T (IO a) 

f :: T (T a -> a) 
f x = x 

g :: Int -> M () 
g = undefined 

h :: Int -> M () 
-- h x = f (g x) -- works on HEAD
h = f . g -- fails on HEAD, works on GHC 8.0

It's possible that this is just fall out from the recent impredicativity changes but I just wanted to make sure that this was on purpose.

Change History (8)

comment:1 Changed 14 months ago by bgamari

Cc: simonpj added
Milestone: 8.2.1

comment:2 Changed 14 months ago by bgamari

Description: modified (diff)
Owner: set to simonpj

comment:3 Changed 14 months ago by ezyang

Confirmed that b612da667fe8fa5277fc78e972a86d4b35f98364 is the regressing commit.

comment:4 Changed 14 months ago by goldfire

The new behavior looks correct to me. g's type expands to Int -> (?x :: Int) => IO (), and it's critical that the (?x :: Int) bit does not get instantiated for this to type-check. Accordingly, the type parameters to (.) would have to be qualified types for this to work, so I say this is an improvement in behavior.

Of course, it might just be time to extend the ($) hack to work with (.), too. Until we do so, though, we should reject the original program.

Simon, what do you think?

comment:5 Changed 14 months ago by simonpj

Richard is right on all counts. This works

h = (.) @(M ()) @(M ()) @Int f g 

recalling that (.) has type

(.) :: forall b c a. (b -> c) -> (a -> b) -> a -> c
  	-- Defined in ‘GHC.Base’

It seems to me that if a special case for ($) is justified, then having one for (.) as well would make sense. Perhaps using it should require -XImpredicativeTypes though?

Simon

comment:6 Changed 14 months ago by goldfire

I'm all for making (.) special in the type-checker, but I don't think it should require ImpredicativeTypes.

comment:7 Changed 12 months ago by RyanGlScott

Agree with Richard. If we can impredicatively use ($) without ImpredicativeTypes, I don't see why we'd need it for (.).

comment:8 Changed 8 months ago by bgamari

Milestone: 8.2.18.4.1

Given that 8.2.1-rc1 is imminent, I'm bumping these off to the 8.4

Note: See TracTickets for help on using tickets.