Opened 8 years ago

Closed 7 years ago

#6069 closed bug (fixed)

Rank 2 Polymorphism Compile Error

Reported by: clinton Owned by: simonpj
Priority: normal Milestone: 7.8.1
Component: Compiler Version: 7.4.1
Keywords: Cc:
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: None/Unknown Test Case: typecheck/should_fail/T6069
Blocked By: Blocking:
Related Tickets: Differential Rev(s):
Wiki Page:

Description

Not sure if this is a bug, perhaps this should be a feature request.

Given the following code:

{-# LANGUAGE Rank2Types #-}

import Control.Monad.ST
import Data.STRef

fourty_two :: forall s. ST s Int
fourty_two = do
  x <- newSTRef (42::Int)
  readSTRef x

main = (print . runST) fourty_two -- (1)
main = (print . runST) $ fourty_two -- (2)
main = ((print . runST) $) fourty_two -- (3)

(1) and (3) compile successfully, but (2) does not. I'm not sure why this is the case.

Change History (5)

comment:1 Changed 8 years ago by clinton

Architecture: x86_64 (amd64)Unknown/Multiple
Operating System: WindowsUnknown/Multiple

comment:2 Changed 7 years ago by igloo

difficulty: Unknown
Milestone: 7.8.1
Owner: set to simonpj

Simon, this looks like your area.

comment:3 Changed 7 years ago by simonpj

Really all three should be rejected without -XImpredicativeTypes, because all require instantiating (.) at a polymorphic type. The inconsistent behaviour is a bug.

Simon

comment:4 Changed 7 years ago by simonpj@…

commit 10f83429ba493699af95cb8c3b16d179d78b7749

Author: Simon Peyton Jones <simonpj@microsoft.com>
Date:   Wed Oct 31 09:08:39 2012 +0000

    Do not instantiate unification variables with polytypes
    
    Without -XImpredicativeTypes, the typing rules say that a function
    should be instantiated only at a *monotype*.  In implementation terms,
    that means that a unification variable should not unify with a type
    involving foralls.  But we were not enforcing that rule, and that
    gave rise to some confusing error messages, such as
      Trac #7264, #6069
    
    This patch adds the test for foralls.  There are consequences
    
     * I put the test in occurCheckExpand, since that is where we see if a
       type can unify with a given unification variable.  So
       occurCheckExpand has to get DynFlags, so it can test for
       -XImpredicativeTypes
    
     * We want this to work
          foo :: (forall a. a -> a) -> Int
          foo = error "foo"
       But that means instantiating error at a polytype!  But error is special
       already because you can instantiate it at an unboxed type like Int#.
       So I extended the specialness to allow type variables of openTypeKind
       to unify with polytypes, regardless of -XImpredicativeTypes.
    
       Conveniently, this works in TcUnify.matchExpectedFunTys, which generates
       unification variable for the function arguments, which can be polymorphic.
    
     * GHC has a special typing rule for ($) (see Note [Typing rule
       for ($)] in TcExpr).  It unifies the argument and result with a
       unification variable to exclude unboxed types -- but that means I
       now need a kind of unificatdion variable that *can* unify with a
       polytype.
    
       So for this sole case I added PolyTv to the data type TcType.MetaInfo.
       I suspect we'll find mor uses for this, and the changes are tiny,
       but it still feel a bit of a hack.  Well the special rule for ($)
       is a hack!
    
    There were some consequential changes in error reporting (TcErrors).

 compiler/typecheck/TcCanonical.lhs |   21 +++---
 compiler/typecheck/TcErrors.lhs    |   62 +++++++++++++------
 compiler/typecheck/TcExpr.lhs      |    9 ++-
 compiler/typecheck/TcHsType.lhs    |   15 +++--
 compiler/typecheck/TcMType.lhs     |   10 +++-
 compiler/typecheck/TcType.lhs      |  118 ++++++++++++++++++++++++-----------
 compiler/typecheck/TcUnify.lhs     |   79 +++++++++++++++++++-----
 7 files changed, 223 insertions(+), 91 deletions(-)

comment:5 Changed 7 years ago by simonpj

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

Now all three fail, as they should, and fail in the same way:

T6069.hs:13:15:
    Couldn't match type `ST s0 Int' with `forall s. ST s b0'
    Expected type: ST s0 Int -> b0
      Actual type: (forall s. ST s b0) -> b0
    In the second argument of `(.)', namely `runST'
    In the expression: print . runST
    In the expression: (print . runST) fourty_two

T6069.hs:14:15:
    Couldn't match type `ST s1 Int' with `forall s. ST s b1'
    Expected type: ST s1 Int -> b1
      Actual type: (forall s. ST s b1) -> b1
    In the second argument of `(.)', namely `runST'
    In the expression: (print . runST)
    In the expression: (print . runST) $ fourty_two

T6069.hs:15:16:
    Couldn't match type `ST s2 Int' with `forall s. ST s b2'
    Expected type: ST s2 Int -> b2
      Actual type: (forall s. ST s b2) -> b2
    In the second argument of `(.)', namely `runST'
    In the first argument of `($)', namely `(print . runST)'
    In the expression: (print . runST) $
Note: See TracTickets for help on using tickets.