Re: [GHC] #7264: Adding GHC's inferred type signatures to a working program can make it fail with Rank2Types
#7264: Adding GHC's inferred type signatures to a working program can make it
fail
with Rank2Types
--+-
Reporter: guest| Owner:
Type: bug | Status: closed
Priority: normal | Milestone:
Component: Compiler |Version: 7.4.1
Resolution: fixed| Keywords:
Os: Unknown/Multiple | Architecture: Unknown/Multiple
Failure: None/Unknown | Difficulty: Unknown
Testcase: typecheck/should_fail/T7264 | Blockedby:
Blocking: |Related:
--+-
Changes (by simonpj):
* status: new => closed
* testcase: => typecheck/should_fail/T7264
* resolution: => fixed
Comment:
Now GHC does not instantiate `mmap` at a polymorphic type, and we get this
error message from the program without the type signature
{{{
T7264.hs:11:19:
Couldn't match type `a' with `forall r. r -> String'
`a' is a rigid type variable bound by
the inferred type of mkFoo2 :: a -> Maybe Foo at T7264.hs:11:1
Expected type: a -> Foo
Actual type: (forall r. r -> String) -> Foo
Relevant bindings include
mkFoo2 :: a -> Maybe Foo (bound at T7264.hs:11:1)
val :: a (bound at T7264.hs:11:8)
In the first argument of `mmap', namely `Foo'
In the expression: mmap Foo (Just val)
In an equation for `mkFoo2': mkFoo2 val = mmap Foo (Just val)
}}}
It's not a fantastic message, but it's on the money, and (without
`-XImpredicativeTypes`) the program should certainly be rejected.
Simon
--
Ticket URL:
GHC
Re: [GHC] #7264: Adding GHC's inferred type signatures to a working program can make it fail with Rank2Types
#7264: Adding GHC's inferred type signatures to a working program can make it
fail
with Rank2Types
-+--
Reporter: guest | Owner:
Type: bug | Status: new
Priority: normal| Milestone:
Component: Compiler | Version: 7.4.1
Keywords:| Os: Unknown/Multiple
Architecture: Unknown/Multiple | Failure: None/Unknown
Difficulty: Unknown |Testcase:
Blockedby:|Blocking:
Related:|
-+--
Comment(by simonpj@…):
commit 10f83429ba493699af95cb8c3b16d179d78b7749
{{{
Author: Simon Peyton Jones
Date: Wed Oct 31 09:08:39 2012 +
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(-)
}}}
--
Ticket URL:
GHC
Re: [GHC] #7264: Adding GHC's inferred type signatures to a working program can make it fail with Rank2Types
#7264: Adding GHC's inferred type signatures to a working program can make it
fail
with Rank2Types
-+--
Reporter: guest | Owner:
Type: bug | Status: new
Priority: normal| Milestone:
Component: Compiler | Version: 7.4.1
Keywords:| Os: Unknown/Multiple
Architecture: Unknown/Multiple | Failure: None/Unknown
Difficulty: Unknown |Testcase:
Blockedby:|Blocking:
Related:|
-+--
Changes (by simonpj):
* cc: dimitris@… (added)
* difficulty: => Unknown
Comment:
This is bad. Here's a slightly cut down example:
{{{
{-# LANGUAGE Rank2Types #-}
module T7264 where
data Foo = Foo (forall r . r -> String)
mmap :: (a->b) -> Maybe a -> Maybe b
mmap f (Just x) = f x
mmap f Nothing = Nothing
-- mkFoo2 :: (forall r. r -> String) -> Maybe Foo
mkFoo2 val = mmap Foo (Just val)
}}}
* The commented-out type sig is inferred, because GHC assigns unknown
type `alpha` to `val`; then instantiates `mmap`'s type with `beta` and
`gamma`; then unifies `beta`:=`forall r. r->String`.
* But when the commented out type sig is provided ghc ''instantiates'' it
at the occurrence of `val`.
You need to call `mmap` at a polymorphic type, which means you need
impredicativity. Lacking `ImpredicativeTypes` the no-signature program
should be rejected. The fact that it isn't is a bug.
Even if that bug is fixed, the progam shows, again, how tricky
impredicativity is. We don't have a decent implementation of
`ImpredicativeTypes`.
At least it's not a show-stopper for anyone.
Simon
--
Ticket URL:
GHC
[GHC] #7264: Adding GHC's inferred type signatures to a working program can make it fail with Rank2Types
#7264: Adding GHC's inferred type signatures to a working program can make it
fail
with Rank2Types
--+-
Reporter: guest | Owner:
Type: bug | Status: new
Priority: normal| Component: Compiler
Version: 7.4.1 | Keywords:
Os: Unknown/Multiple | Architecture: Unknown/Multiple
Failure: None/Unknown | Testcase:
Blockedby:| Blocking:
Related:|
--+-
{{{
{-# LANGUAGE Rank2Types #-}
module Test where
data Foo = Foo { unFoo :: forall r . (RealFrac r) => r -> String }
mkFoo1 :: (forall r. RealFrac r => r -> String) -> Maybe Foo
mkFoo1 val = Just $ Foo val
--mkFoo2 :: (forall r. RealFrac r => r -> String) -> Maybe Foo
mkFoo2 val = Foo `fmap` Just val
}}}
Without the commented-out type signature, the program typechecks without
complaint. With it, the program fails to compile with the error:
{{{
Test.hs:10:30:
Couldn't match expected type `forall r. RealFrac r => r -> String'
with actual type `r0 -> String'
In the first argument of `Just', namely `val'
In the second argument of `fmap', namely `Just val'
In the expression: Foo `fmap` Just val
}}}
Note that the commented-out type is exactly what's inferred by GHC.
Also note that (with ImpredicativeTypes also enabled), this is fine (but
mkFoo2 still fails if its type signature is included):
{{{
mkFoo3 :: (forall r. RealFrac r => r -> String) -> Maybe Foo
mkFoo3 val = Foo `fmap` (Just :: (forall s. RealFrac s => s -> String) ->
(Maybe (forall s. RealFrac s => s -> String))) val
}}}
It's confusing that adding a valid, GHC-inferred type signature to a
program can break it, and the error message leaves something to be
desired.
--
Ticket URL:
GHC
