Commit c93ad554 authored by Simon Peyton Jones's avatar Simon Peyton Jones Committed by Ben Gamari

Fix impredicativity (again)

This patch fixes Trac #12616.

Dignosis.  In TcUnify.tc_sub_type_ds we were going to some trouble to
support co- and contra-variance even for impredicative types.  With
-XImpredicativeTYpes, this allowed a unification variable to be
unified with a polytype (probably wrongly) and that caused later
trouble in the constraint solver, where -XImpredicativeTypes was /not/
on.  In effect, -XImpredicativeTypes can't be switched on locally.

Why did we want ImpredicativeTypes locally?  Because the program
generated by GND for a higher-rank method involved impredicative
instantation of 'coerce':
      op = coerce op   -- where op has a higher rank type
See Note [Newtype-deriving instances] in TcGenDeriv.

Cure.

1.  It is ghastly to rely on ImpredicativeTypes (a 100% flaky
    feature) to instantiate coerce polymorphically.  Happily we
    now have Visible Type Application, so I've used that instead
    which should be solid and reliable.

2.  I deleted the code in tc_sub_type_ds that allows the constraint
    solver to "look through" a unification variable to find a
    polytype.  That used to be essential in the days of ReturnTv,
    but it's utterly unreliable and should be consigned to the dustbin
    of history.  (We have ExpType now for the essential uses.)

Tests involving ImpredicativeTypes are affected, but I'm not worried
about them... it's advertised as a feature you can't rely on, and
I want to reform it outright.

(cherry picked from commit b612da66)
parent cec50665
......@@ -32,7 +32,7 @@ module HsUtils(
nlHsIntLit, nlHsVarApps,
nlHsDo, nlHsOpApp, nlHsLam, nlHsPar, nlHsIf, nlHsCase, nlList,
mkLHsTupleExpr, mkLHsVarTuple, missingTupArg,
toLHsSigWcType,
typeToLHsType,
-- * Constructing general big tuples
-- $big_tuples
......@@ -603,14 +603,14 @@ mkClassOpSigs sigs
fiddle (L loc (TypeSig nms ty)) = L loc (ClassOpSig False nms (dropWildCards ty))
fiddle sig = sig
toLHsSigWcType :: Type -> LHsSigWcType RdrName
typeToLHsType :: Type -> LHsType RdrName
-- ^ Converting a Type to an HsType RdrName
-- This is needed to implement GeneralizedNewtypeDeriving.
--
-- Note that we use 'getRdrName' extensively, which
-- generates Exact RdrNames rather than strings.
toLHsSigWcType ty
= mkLHsSigWcType (go ty)
typeToLHsType ty
= go ty
where
go :: Type -> LHsType RdrName
go ty@(ForAllTy (Anon arg) _)
......
......@@ -2267,6 +2267,8 @@ genInst spec@(DS { ds_tvs = tvs, ds_tc = rep_tycon
, ib_pragmas = []
, ib_extensions = [ LangExt.ImpredicativeTypes
, LangExt.RankNTypes ]
-- Both these flags are needed for higher-rank uses of coerce
-- See Note [Newtype-deriving instances] in TcGenDeriv
, ib_derived = True } }
, emptyBag
, Just $ getName $ head $ tyConDataCons rep_tycon ) }
......
......@@ -535,7 +535,7 @@ unliftedCompare lt_op eq_op a_expr b_expr lt eq gt
-- mean more tests (dynamically)
nlHsIf (ascribeBool $ genPrimOpApp a_expr eq_op b_expr) eq gt
where
ascribeBool e = nlExprWithTySig e (toLHsSigWcType boolTy)
ascribeBool e = nlExprWithTySig e boolTy
nlConWildPat :: DataCon -> LPat RdrName
-- The pattern (K {})
......@@ -2153,10 +2153,8 @@ coercing from. So from, say,
(op :: a -> [<rep-ty>] -> Int)
) :: a -> [T x] -> Int
Notice that we give the 'coerce' call two type signatures: one to
fix the of the inner call, and one for the expected type. The outer
type signature ought to be redundant, but may improve error messages.
The inner one is essential to fix the type at which 'op' is called.
Notice that we give the 'coerce' two explicitly-visible type arguments
to say how it should be instantiated. Recall
See #8503 for more discussion.
......@@ -2194,19 +2192,21 @@ gen_Newtype_binds loc cls inst_tvs cls_tys rhs_ty
where
Pair from_ty to_ty = mkCoerceClassMethEqn cls inst_tvs cls_tys rhs_ty meth_id
-- See "wrinkle" in Note [Newtype-deriving instances]
(_, _, from_ty') = tcSplitSigmaTy from_ty
meth_RDR = getRdrName meth_id
rhs_expr = ( nlHsVar coerce_RDR
`nlHsApp`
(nlHsVar meth_RDR `nlExprWithTySig` toLHsSigWcType from_ty'))
`nlExprWithTySig` toLHsSigWcType to_ty
rhs_expr = nlHsVar coerce_RDR `nlHsAppType` from_ty
`nlHsAppType` to_ty
`nlHsApp` nlHsVar meth_RDR
nlHsAppType :: LHsExpr RdrName -> Type -> LHsExpr RdrName
nlHsAppType e s = noLoc (e `HsAppType` hs_ty)
where
hs_ty = mkHsWildCardBndrs (typeToLHsType s)
nlExprWithTySig :: LHsExpr RdrName -> LHsSigWcType RdrName -> LHsExpr RdrName
nlExprWithTySig e s = noLoc (ExprWithTySig e s)
nlExprWithTySig :: LHsExpr RdrName -> Type -> LHsExpr RdrName
nlExprWithTySig e s = noLoc (e `ExprWithTySig` hs_ty)
where
hs_ty = mkLHsSigWcType (typeToLHsType s)
mkCoerceClassMethEqn :: Class -- the class being derived
-> [TyVar] -- the tvs in the instance head
......
......@@ -718,27 +718,13 @@ tc_sub_type_ds eq_orig inst_orig ctxt ty_actual ty_expected
; tc_sub_type_ds eq_orig inst_orig ctxt ty_a' ty_e }
Unfilled _ -> unify }
go ty_a (TyVarTy tv_e)
= do { dflags <- getDynFlags
; tclvl <- getTcLevel
; lookup_res <- lookupTcTyVar tv_e
; case lookup_res of
Filled ty_e' ->
do { traceTc "tcSubTypeDS_NC_O following filled exp meta-tyvar:"
(ppr tv_e <+> text "-->" <+> ppr ty_e')
; tc_sub_tc_type eq_orig inst_orig ctxt ty_a ty_e' }
Unfilled details
| canUnifyWithPolyType dflags details
&& isTouchableMetaTyVar tclvl tv_e -- don't want skolems here
-> unify
-- We've avoided instantiating ty_actual just in case ty_expected is
-- polymorphic. But we've now assiduously determined that it is *not*
-- polymorphic. So instantiate away. This is needed for e.g. test
-- typecheck/should_compile/T4284.
| otherwise
-> inst_and_unify }
-- Historical note (Sept 16): there was a case here for
-- go ty_a (TyVarTy alpha)
-- which, in the impredicative case unified alpha := ty_a
-- where th_a is a polytype. Not only is this probably bogus (we
-- simply do not have decent story for imprdicative types), but it
-- caused Trac #12616 because (also bizarrely) 'deriving' code had
-- -XImpredicativeTypes on. I deleted the entire case.
go (ForAllTy (Anon act_arg) act_res) (ForAllTy (Anon exp_arg) exp_res)
| not (isPredTy act_arg)
......@@ -1325,7 +1311,7 @@ uUnfilledVar origin t_or_k swapped tv1 ty2
-- Zonk to expose things to the
-- occurs check, and so that if ty2
-- looks like a type variable then it
-- is a type variable
-- /is/ a type variable
; uUnfilledVar1 origin t_or_k swapped tv1 ty2 }
----------
......
{-# OPTIONS_GHC -XImpredicativeTypes -fno-warn-deprecated-flags #-}
module Base1 where
-- basic examples of impredicative instantiation of variables
-- Sept 16: now failing, beause I've furter reduced the scop
-- of impredicative types
data MEither a b = MLeft a
| MRight b
module Base1 where
-- basic examples of impredicative instantiation of variables
data MEither a b = MLeft a
| MRight b
| MEmpty
type Sid = forall a. a -> a
type Sid = forall a. a -> a
-- no need for impredicativity
test0 = MRight id
-- no need for impredicativity
test0 = MRight id
-- requires impredicativity
-- requires impredicativity
test1 :: Sid -> MEither Sid b
test1 fid = MLeft fid
test1 fid = MLeft fid
test2 :: MEither b Sid -> Maybe (Sid,Sid)
test2 m = case (test1 id) of
MLeft x -> case m of
MRight y -> Just (x,y)
_ -> Nothing
test2 :: MEither b Sid -> Maybe (Sid,Sid)
test2 m = case (test1 id) of
MLeft x -> case m of
MRight y -> Just (x,y)
_ -> Nothing
_ -> Nothing
test3 :: MEither a b -> b
test3 (MRight x) = x
test3 (MRight x) = x
test4 = test3 (test1 id)
test4 = test3 (test1 id)
Base1.hs:20:13: error:
• Couldn't match type ‘a0 -> a0’ with ‘forall a. a -> a’
Expected type: MEither Sid b
Actual type: MEither (a0 -> a0) b
• In the expression: MLeft fid
In an equation for ‘test1’: test1 fid = MLeft fid
Base1.hs:25:39: error:
• Couldn't match type ‘a1 -> a1’ with ‘forall a. a -> a’
Expected type: Maybe (Sid, Sid)
Actual type: Maybe (a1 -> a1, a2 -> a2)
• In the expression: Just (x, y)
In a case alternative: MRight y -> Just (x, y)
In the expression:
case m of {
MRight y -> Just (x, y)
_ -> Nothing }
{-# OPTIONS_GHC -XImpredicativeTypes -fno-warn-deprecated-flags #-}
-- Sept 16: now scraping through with -XImpredicateTypes
module Main where
data Foo x y = Foo {foo1 :: x, foo2 :: y}
......
# Boxy-type tests
test('Base1', normal, compile, [''])
test('Base1', normal, compile_fail, [''])
test('Church1', expect_broken(4295), compile, [''])
test('Church2', expect_broken(1330), compile_fail, [''])
test('PList1', expect_broken(4295), compile, [''])
......@@ -8,4 +8,4 @@ test('PList2', expect_broken(4295), compile, [''])
test('SystemF', expect_broken(4295), compile, [''])
test('boxy', expect_broken(4295), compile, [''])
test('Compose', normal, compile, [''])
test('T2193', expect_broken(4295), compile_and_run, [''])
test('T2193', normal, compile_and_run, [''])
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeOperators #-}
module T12616 where
type m ~> n = forall a. m a -> n a
class MonadTrans t where
-- > this line works:
-- lift :: (Monad m) => m a -> t m a
-- > this line doesn't:
lift :: (Monad m) => m ~> t m
data StateT s m a = StateT { runStateT :: s -> m (a, s) }
instance MonadTrans (StateT s) where
lift xM = StateT $ \ s -> do { x <- xM ; return (x,s) }
newtype OtherStateT s m a = OtherStateT { runOtherStateT :: StateT s m a }
deriving (MonadTrans)
......@@ -73,3 +73,4 @@ test('T11833', normal, compile, [''])
test('T11837', normal, compile, [''])
test('T12399', normal, compile, [''])
test('T12583', normal, compile, [''])
test('T12616', normal, compile, [''])
......@@ -3,9 +3,9 @@ T4846.hs:29:1: error:
• Couldn't match type ‘Bool’ with ‘BOOL’
arising from a use of ‘GHC.Prim.coerce’
• In the expression:
GHC.Prim.coerce (mkExpr :: Expr Bool) :: Expr BOOL
GHC.Prim.coerce @(Expr Bool) @(Expr BOOL) mkExpr
In an equation for ‘mkExpr’:
mkExpr = GHC.Prim.coerce (mkExpr :: Expr Bool) :: Expr BOOL
mkExpr = GHC.Prim.coerce @(Expr Bool) @(Expr BOOL) mkExpr
When typechecking the code for ‘mkExpr’
in a derived instance for ‘B BOOL’:
To see the code I am typechecking, use -ddump-deriv
......
{-# LANGUAGE ImpredicativeTypes #-}
module T12644 where
data T a = T1 Int
instance Show (T a) where
show (T1 x) = show x
t1 :: T a
t1 = T1 1
f :: String
f = show t1
......@@ -521,3 +521,4 @@ test('T10635', normal, compile, [''])
test('T12170b', normal, compile, [''])
test('T12466', normal, compile, [''])
test('T12466a', normal, compile, [''])
test('T12644', normal, compile, [''])
......@@ -6,6 +6,9 @@
-- Here are a bunch of tests for impredicative polymorphism
-- mainly written by Dimitrios
-- Sept 16: I'm just accepting the bizarre output.
-- None of this is right
module ShouldCompile where
xs :: [forall a. a->a]
......
tc211.hs:73:9: error:
• Couldn't match type ‘forall a2. a2 -> a2’ with ‘a1 -> a1’
tc211.hs:20:8: error:
• Couldn't match expected type ‘forall a. a -> a’
with actual type ‘a1 -> a1’
• In the expression:
(:) ::
(forall a. a -> a) -> [forall a. a -> a] -> [forall a. a -> a]
In the expression:
((:) ::
(forall a. a -> a) -> [forall a. a -> a] -> [forall a. a -> a])
(head foo) foo
In an equation for ‘bar’:
bar
= ((:) ::
(forall a. a -> a) -> [forall a. a -> a] -> [forall a. a -> a])
(head foo) foo
tc211.hs:25:8: error:
• Couldn't match type ‘a3 -> a3’ with ‘forall a. a -> a’
Expected type: [forall a. a -> a]
Actual type: [a3 -> a3]
• In the expression: (head foo) : (tail foo)
In an equation for ‘barr’: barr = (head foo) : (tail foo)
tc211.hs:25:20: error:
• Couldn't match type ‘forall a. a -> a’ with ‘a3 -> a3’
Expected type: [a3 -> a3]
Actual type: [forall a. a -> a]
• In the second argument of ‘(:)’, namely ‘(tail foo)’
In the expression: (head foo) : (tail foo)
In an equation for ‘barr’: barr = (head foo) : (tail foo)
tc211.hs:62:18: error:
• Couldn't match expected type ‘forall a. a -> a’
with actual type ‘a0 -> a0’
• In the expression:
Cons ::
(forall a. a -> a)
-> List (forall a. a -> a) -> List (forall a. a -> a)
In an equation for ‘cons’:
cons
= Cons ::
(forall a. a -> a)
-> List (forall a. a -> a) -> List (forall a. a -> a)
In the expression:
let
cons
= Cons ::
(forall a. a -> a)
-> List (forall a. a -> a) -> List (forall a. a -> a)
in cons (\ x -> x) Nil
tc211.hs:68:8: error:
• Couldn't match expected type ‘forall a. a -> a’
with actual type ‘a2 -> a2’
• In the expression:
Cons ::
(forall a. a -> a)
-> List (forall a. a -> a) -> List (forall a. a -> a)
In the expression:
(Cons ::
(forall a. a -> a)
-> List (forall a. a -> a) -> List (forall a. a -> a))
(\ x -> x) Nil
In an equation for ‘xs2’:
xs2
= (Cons ::
(forall a. a -> a)
-> List (forall a. a -> a) -> List (forall a. a -> a))
(\ x -> x) Nil
tc211.hs:76:9: error:
• Couldn't match type ‘forall a5. a5 -> a5’ with ‘a4 -> a4’
Expected type: List (forall a. a -> a)
-> (forall a. a -> a) -> a1 -> a1
Actual type: List (a1 -> a1) -> (a1 -> a1) -> a1 -> a1
-> (forall a. a -> a) -> a4 -> a4
Actual type: List (a4 -> a4) -> (a4 -> a4) -> a4 -> a4
• In the expression:
foo2 ::
List (forall a. a -> a) -> (forall a. a -> a) -> (forall a. a -> a)
......
......@@ -20,14 +20,9 @@ T10619.hs:9:15: error:
foo :: t -> (b -> b) -> b -> b (bound at T10619.hs:8:1)
T10619.hs:14:15: error:
• Couldn't match type ‘b’ with ‘a’
because type variable ‘a’ would escape its scope
This (rigid, skolem) type variable is bound by
a type expected by the context:
a -> a
at T10619.hs:14:15-65
• Couldn't match type ‘forall a. a -> a’ with ‘b -> b’
Expected type: (b -> b) -> b -> b
Actual type: (forall a. a -> a) -> forall b. b -> b
Actual type: (forall a. a -> a) -> b -> b
• In the expression:
((\ x -> x) :: (forall a. a -> a) -> forall b. b -> b)
In the expression:
......@@ -56,14 +51,9 @@ T10619.hs:16:13: error:
baz :: Bool -> (b -> b) -> b -> b (bound at T10619.hs:16:1)
T10619.hs:20:14: error:
• Couldn't match type ‘b’ with ‘a’
because type variable ‘a’ would escape its scope
This (rigid, skolem) type variable is bound by
a type expected by the context:
a -> a
at T10619.hs:20:14-64
• Couldn't match type ‘forall a. a -> a’ with ‘b -> b’
Expected type: (b -> b) -> b -> b
Actual type: (forall a. a -> a) -> forall b. b -> b
Actual type: (forall a. a -> a) -> b -> b
• In the expression:
(\ x -> x) :: (forall a. a -> a) -> forall b. b -> b
In an equation for ‘quux’:
......
T2846b.hs:5:5: error:
• No instance for (Show (forall a. [Num a => a]))
• No instance for (Show (Num a0 => a0))
arising from a use of ‘show’
(maybe you haven't applied a function to enough arguments?)
• In the expression: show ([1, 2, 3] :: [Num a => a])
In an equation for ‘f’: f = show ([1, 2, 3] :: [Num a => a])
T8428.hs:11:19: error:
• Couldn't match type ‘forall s1. ST s1’ with ‘ST s
• Couldn't match type ‘(forall s. ST s) a’ with ‘forall s. ST s a
Expected type: IdentityT (forall s. ST s) a -> forall s. ST s a
Actual type: IdentityT (forall s. ST s) a -> (forall s. ST s) a
• In the second argument of ‘(.)’, namely ‘runIdentityT’
In the expression: runST . runIdentityT
In an equation for ‘runIdST’: runIdST = runST . runIdentityT
• Relevant bindings include
runIdST :: IdentityT (forall s. ST s) a -> a
(bound at T8428.hs:11:1)
......@@ -147,7 +147,7 @@ test('tcfail160', normal, compile_fail, [''])
test('tcfail161', normal, compile_fail, [''])
test('tcfail162', normal, compile_fail, [''])
test('tcfail164', normal, compile_fail, [''])
test('tcfail165', normal, compile, [''])
test('tcfail165', normal, compile_fail, [''])
test('tcfail166', normal, compile_fail, [''])
test('tcfail167', normal, compile_fail, [''])
test('tcfail168', normal, compile_fail, [''])
......
tcfail016.hs:8:1: error:
• Couldn't match type ‘(t, Expr t)’ with ‘Expr t
• Couldn't match type ‘Expr t’ with ‘(t, Expr t)
Expected type: AnnExpr t -> [[Char]]
Actual type: Expr t -> [[Char]]
• Relevant bindings include
......
......@@ -10,8 +10,10 @@ import Control.Concurrent
-- Actually (Dec 06) it succeeds now
--
-- In GHC 7.0 it fails again! (and rightly so)
--
-- With the Visible Type Application patch, this succeeds again.
--
-- Sept 16: fails again as it should
foo = do var <- newEmptyMVar :: IO (MVar (forall a. Show a => a -> String))
putMVar var (show :: forall b. Show b => b -> String)
tcfail165.hs:19:23: error:
• Couldn't match expected type ‘forall a. Show a => a -> String’
with actual type ‘b0 -> String’
• In the second argument of ‘putMVar’, namely
‘(show :: forall b. Show b => b -> String)’
In a stmt of a 'do' block:
putMVar var (show :: forall b. Show b => b -> String)
In the expression:
do { var <- newEmptyMVar ::
IO (MVar (forall a. Show a => a -> String));
putMVar var (show :: forall b. Show b => b -> String) }
......@@ -8,6 +8,8 @@ data Capture a = Base a
g :: Capture (forall a . a -> a)
g = Base id -- Fails; need a rigid signature on 'id'
-- Actually, succeeds now, with visible type application
-- Disagree: should not succeed becuase it instantiates
-- Base with a forall type
-- This function should definitely be rejected, with or without type signature
......
tcfail174.hs:14:14: error:
tcfail174.hs:9:5: error:
• Couldn't match type ‘a0 -> a0’ with ‘forall a. a -> a’
Expected type: Capture (forall a. a -> a)
Actual type: Capture (a0 -> a0)
• In the expression: Base id
In an equation for ‘g’: g = Base id
tcfail174.hs:16:14: error:
• Couldn't match type ‘a’ with ‘a1’
because type variable ‘a1’ would escape its scope
This (rigid, skolem) type variable is bound by
the type a1 -> a1
at tcfail174.hs:14:1-14
at tcfail174.hs:16:1-14
Expected type: Capture (forall x. x -> a)
Actual type: Capture (forall a. a -> a)
• In the first argument of ‘Capture’, namely ‘g’
In the expression: Capture g
In an equation for ‘h1’: h1 = Capture g
• Relevant bindings include
h1 :: Capture a (bound at tcfail174.hs:14:1)
h1 :: Capture a (bound at tcfail174.hs:16:1)
tcfail174.hs:17:14: error:
tcfail174.hs:19:14: error:
• Couldn't match type ‘a’ with ‘b’
‘a’ is a rigid type variable bound by
the type a -> a at tcfail174.hs:1:1
‘b’ is a rigid type variable bound by
the type signature for:
h2 :: forall b. Capture b
at tcfail174.hs:16:7
at tcfail174.hs:18:7
Expected type: Capture (forall x. x -> b)
Actual type: Capture (forall a. a -> a)
• In the first argument of ‘Capture’, namely ‘g’
In the expression: Capture g
In an equation for ‘h2’: h2 = Capture g
• Relevant bindings include
h2 :: Capture b (bound at tcfail174.hs:17:1)
h2 :: Capture b (bound at tcfail174.hs:19:1)
......@@ -62,7 +62,7 @@ test('tcrun038',
test('tcrun039', normal, compile_and_run, [''])
test('tcrun040', normal, compile_and_run, [''])
test('tcrun041', omit_ways(['ghci']), compile_and_run, [''])
test('tcrun042', normal, compile_and_run, [''])
test('tcrun042', normal, compile_fail, [''])
test('tcrun043', normal, compile_and_run, [''])
test('tcrun044', normal, compile_and_run, [''])
test('tcrun045', normal, compile_fail, [''])
......
tcrun042.hs:5:5: error:
• Couldn't match expected type ‘forall c. c -> c -> c’
with actual type ‘b0 -> b0 -> b0’
• In the expression: (, "Hello" ++ "World",)
In an equation for ‘e’: e = (, "Hello" ++ "World",)
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