[commit: ghc] master: Testsuite: add ImpredicativeTypes to T7861 (#7861) (4c96e7c)

git at git.haskell.org git at git.haskell.org
Mon Jul 20 15:06:05 UTC 2015


Repository : ssh://git@git.haskell.org/ghc

On branch  : master
Link       : http://ghc.haskell.org/trac/ghc/changeset/4c96e7cf56fc67ad09efaf8c5de1c8d7a0f5cedd/ghc

>---------------------------------------------------------------

commit 4c96e7cf56fc67ad09efaf8c5de1c8d7a0f5cedd
Author: Thomas Miedema <thomasmiedema at gmail.com>
Date:   Mon Jul 20 15:39:52 2015 +0200

    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


>---------------------------------------------------------------

4c96e7cf56fc67ad09efaf8c5de1c8d7a0f5cedd
 testsuite/tests/typecheck/should_run/T7861.hs     | 12 +++++++-----
 testsuite/tests/typecheck/should_run/T7861.stderr | 13 +++++++------
 2 files changed, 14 insertions(+), 11 deletions(-)

diff --git a/testsuite/tests/typecheck/should_run/T7861.hs b/testsuite/tests/typecheck/should_run/T7861.hs
index 9ff9a43..19a9c9d 100644
--- a/testsuite/tests/typecheck/should_run/T7861.hs
+++ b/testsuite/tests/typecheck/should_run/T7861.hs
@@ -1,20 +1,22 @@
 {-# 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
diff --git a/testsuite/tests/typecheck/should_run/T7861.stderr b/testsuite/tests/typecheck/should_run/T7861.stderr
index f9f2386..62b0dcd 100644
--- a/testsuite/tests/typecheck/should_run/T7861.stderr
+++ b/testsuite/tests/typecheck/should_run/T7861.stderr
@@ -1,10 +1,11 @@
-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)



More information about the ghc-commits mailing list