Commit 4c96e7cf authored by thomie's avatar thomie Committed by Ben Gamari

Testsuite: add ImpredicativeTypes to T7861 (#7861)

The test was failing with:

    T7861: T7861.hs:15:13:
        Cannot instantiate unification variable ‘t0’
        with a type involving foralls: A a0 -> a0
          GHC doesn't yet support impredicative polymorphism
        In the first argument of ‘seq’, namely ‘f’
        In a stmt of a 'do' block: f `seq` print "Hello 2"

It requires ImpredicativeTypes, at least since 7.8, because we
instantiate seq's type (c->d->d) with f's type (c:= (forall b. a) -> a),
which is polymorphic (it has foralls).

I simplified the test a bit by removing the type synonym, and verified
that ghc-7.6.3 still panics on this test.

Reviewers: simonpj, austin, bgamari

Reviewed By: bgamari

Subscribers: thomie

Differential Revision: https://phabricator.haskell.org/D1080

GHC Trac Issues: #7861
parent 9834fea4
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ImpredicativeTypes #-}
{-# OPTIONS_GHC -fdefer-type-errors #-}
module Main where
type A a = forall b. a
doA :: A a -> [a]
doA :: (forall b. a) -> [a]
doA = undefined
f :: A a -> a
f :: (forall b. a) -> a
f = doA
main = do { print "Hello 1"
; f `seq` print "Hello 2"
-- The casts are pushed inside the lambda
-- for f, so this seq succeds fine
-- for f, so this seq succeeds fine
-- It does require ImpredicativeTypes, because we instantiate
-- seq's type (c->d->d) with f's type (c:= (forall b. a) -> a),
-- which is polymorphic (it has foralls).
; f (error "urk") `seq` print "Bad"
-- But when we *call* f we get a type error
......
T7861: T7861.hs:11:5:
T7861: T7861.hs:10:5: error:
Couldn't match type ‘a’ with ‘[a]’
‘a’ is a rigid type variable bound by
the type signature for: f :: A a -> a at T7861.hs:10:6
Expected type: A a -> a
Actual type: A a -> [a]
Relevant bindings include f :: A a -> a (bound at T7861.hs:11:1)
‘a’ is a rigid type variable bound by
the type signature for: f :: (forall b. a) -> a at T7861.hs:9:6
Expected type: (forall b. a) -> a
Actual type: (forall b. a) -> [a]
Relevant bindings include
f :: (forall b. a) -> a (bound at T7861.hs:10:1)
In the expression: doA
In an equation for ‘f’: f = doA
(deferred type error)
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment