Commit b612da66 authored by Simon Peyton Jones's avatar Simon Peyton Jones
Browse files

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 al...
parent 3012c431
......@@ -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
......@@ -597,14 +597,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@(FunTy arg _)
......
......@@ -2274,6 +2274,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 ) }
......
......@@ -576,7 +576,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 {})
......@@ -2213,31 +2213,30 @@ coercing from. So from, say,
newtype T x = MkT <rep-ty>
instance C a <rep-ty> => C a (T x) where
op = (coerce
(op :: a -> [<rep-ty>] -> Int)
) :: a -> [T x] -> Int
op = coerce @ (a -> [<rep-ty>] -> Int)
@ (a -> [T x] -> Int)
op
Notice that we give the 'coerce' call two type signatures: one to
fix the type 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.
Here's a wrinkle. Supppose 'op' is locally overloaded:
coerce :: Coeercible a b => a -> b
class C2 b where
op2 :: forall a. Eq a => a -> [b] -> Int
By giving it explicit type arguments we deal with the case where
'op' has a higher rank type, and so we must instantiae 'coerce' with
a polytype. E.g.
class C a where op :: forall b. a -> b -> b
newtype T x = MkT <rep-ty>
instance C <rep-ty> => C (T x) where
op = coerce @ (forall b. <rep-ty> -> b -> b)
@ (forall b. T x -> b -> b)
op
Then we could do exactly as above, but it's a bit redundant to
instantiate op, then re-generalise with the inner signature.
(The inner sig is only there to fix the type at which 'op' is
called.) So we just instantiate the signature, and add
The type checker checks this code, and it currently requires
-XImpredicativeTypes to permit that polymorphic type instantiation,
so ew have to switch that flag on locally in TcDeriv.genInst.
instance C2 <rep-ty> => C2 (T x) where
op2 = (coerce
(op2 :: a -> [<rep-ty>] -> Int)
) :: forall a. Eq a => a -> [T x] -> Int
See #8503 for more discussion.
-}
gen_Newtype_binds :: SrcSpan
......@@ -2260,19 +2259,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
......
......@@ -721,27 +721,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 (FunTy act_arg act_res) (FunTy exp_arg exp_res)
| not (isPredTy act_arg)
......@@ -1320,7 +1306,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)
{-# 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('T12245', 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 #-}
-- Sept 16: this compiles again now, because I've weakened
-- ImpredicativeTypes a lot
module T11319 where
f :: Monad m => m (Maybe a)
......
{-# 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
......@@ -504,7 +504,7 @@ test('T11462',
test('T11480', normal, compile, [''])
test('RebindHR', normal, compile, [''])
test('RebindNegate', normal, compile, [''])
test('T11319', expect_broken(11319), compile, [''])
test('T11319', normal, compile, [''])
test('T11397', normal, compile, [''])
test('T11458', normal, compile, [''])
test('T11524', normal, compile, [''])
......@@ -541,3 +541,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 ‘(a, Expr a)’ with ‘Expr a’
• Couldn't match type ‘Expr a’ with ‘(a, Expr a)
Expected type: AnnExpr a -> [[Char]]
Actual type: Expr a -> [[Char]]
• Relevant bindings include
......
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