Opened 4 years ago

Closed 4 years ago

Last modified 2 years ago

#10619 closed bug (fixed)

Order matters when type-checking

Reported by: goldfire Owned by:
Priority: normal Milestone: 8.0.1
Component: Compiler Version: 7.10.1
Keywords: ImpredicativeTypes Cc: jstolarek
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: None/Unknown Test Case: typecheck/should_fail/T10619
Blocked By: Blocking:
Related Tickets: Differential Rev(s):
Wiki Page:

Description

When I say

{-# LANGUAGE RankNTypes #-}

module Bug where

foo True  = (\x -> x) :: (forall a. a -> a) -> forall b. b -> b
foo False = \y -> y

the module compiles. But when I say

{-# LANGUAGE RankNTypes #-}

module Bug where

foo False = \y -> y
foo True  = (\x -> x) :: (forall a. a -> a) -> forall b. b -> b

it doesn't, failing with

Bug.hs:6:13:
    Couldn't match type ‘b0 -> b0’ with ‘forall a. a -> a’
    Expected type: (forall a. a -> a) -> forall a. a -> a
      Actual type: (forall a. a -> a) -> b0 -> b0
    In the expression:
        (\ x -> x) :: (forall a. a -> a) -> forall b. b -> b
    In an equation for ‘foo’:
        foo True = (\ x -> x) :: (forall a. a -> a) -> forall b. b -> b

I believe this behavior stems from the special case in tcMonoBinds, for non-recursive functions without a type signature. I believe the bug would be fixed if that function also checks to make sure that there is precisely one clause to the function. Do you agree?

Change History (7)

comment:1 Changed 4 years ago by goldfire

It gets worse. The same problem happens between these two:

This succeeds:

{-# LANGUAGE RankNTypes #-}

module Bug where

foo _ = if True
        then ((\x -> x) :: (forall a. a -> a) -> forall b. b -> b)
        else \y -> y

This fails:

foo _ = if True
        then \y -> y
        else ((\x -> x) :: (forall a. a -> a) -> forall b. b -> b)

But the cause is different. This second case is caused by the fact that ReturnTvs can unify with polytypes, and the ReturnTv for the whole expression is just pushed into the if's branches. But even if the ReturnTv were replaced by a TauTv before pushing into the if's branches, it would still be broken because a TauTv with an OpenKind can also unify with polytypes.

I think the solution for this case is to create a new flavor of TauTv that truly insists on being a tau-type.

comment:2 Changed 4 years ago by jstolarek

Cc: jstolarek added

comment:3 Changed 4 years ago by Richard Eisenberg <eir@…>

In 2db18b81/ghc:

Visible type application

This re-working of the typechecker algorithm is based on
the paper "Visible type application", by Richard Eisenberg,
Stephanie Weirich, and Hamidhasan Ahmed, to be published at
ESOP'16.

This patch introduces -XTypeApplications, which allows users
to say, for example `id @Int`, which has type `Int -> Int`. See
the changes to the user manual for details.

This patch addresses tickets #10619, #5296, #10589.

comment:4 Changed 4 years ago by Richard Eisenberg <eir@…>

In 05e3541/ghc:

Test #10619 in typecheck/should_fail/T10619

comment:5 Changed 4 years ago by goldfire

Resolution: fixed
Status: newclosed
Test Case: typecheck/should_fail/T10619

comment:6 Changed 4 years ago by thomie

Milestone: 8.0.1

comment:7 Changed 2 years ago by simonpj

Keywords: ImpredicativeTypes added
Note: See TracTickets for help on using tickets.