Commit b460d6c9 authored by Richard Eisenberg's avatar Richard Eisenberg Committed by Ben Gamari

Fix #13233 by checking for lev-poly primops

The implementation plan is all in Note [Detecting forced eta expansion]
in DsExpr.

Test Plan: ./validate, codeGen/should_fail/T13233

Reviewers: simonpj, austin, bgamari

Subscribers: rwbarton, thomie

GHC Trac Issues: #13233

Differential Revision: https://phabricator.haskell.org/D3490
parent b1aede61
......@@ -1350,8 +1350,8 @@ lintArrow :: SDoc -> LintedKind -> LintedKind -> LintM LintedKind
-- See Note [GHC Formalism]
lintArrow what k1 k2 -- Eg lintArrow "type or kind `blah'" k1 k2
-- or lintarrow "coercion `blah'" k1 k2
= do { unless (okArrowArgKind k1) (addErrL (msg (text "argument") k1))
; unless (okArrowResultKind k2) (addErrL (msg (text "result") k2))
= do { unless (classifiesTypeWithValues k1) (addErrL (msg (text "argument") k1))
; unless (classifiesTypeWithValues k2) (addErrL (msg (text "result") k2))
; return liftedTypeKind }
where
msg ar k
......
......@@ -457,7 +457,8 @@ See #case_invariants#
Note [Levity polymorphism invariants]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
The levity-polymorphism invariants are these:
The levity-polymorphism invariants are these (as per "Levity Polymorphism",
PLDI '17):
* The type of a term-binder must not be levity-polymorphic,
unless it is a let(rec)-bound join point
......
......@@ -580,7 +580,7 @@ translatePat fam_insts pat = case pat of
| otherwise -> do
ps <- translatePat fam_insts p
(xp,xe) <- mkPmId2Forms ty
let g = mkGuard ps (HsWrap wrapper (unLoc xe))
let g = mkGuard ps (mkHsWrap wrapper (unLoc xe))
return [xp,g]
-- (n + k) ===> x (True <- x >= k) (n <- x-k)
......
......@@ -575,8 +575,8 @@ dsCmd ids local_vars stack_ty res_ty
let
left_id = HsConLikeOut (RealDataCon left_con)
right_id = HsConLikeOut (RealDataCon right_con)
left_expr ty1 ty2 e = noLoc $ HsApp (noLoc $ HsWrap (mkWpTyApps [ty1, ty2]) left_id ) e
right_expr ty1 ty2 e = noLoc $ HsApp (noLoc $ HsWrap (mkWpTyApps [ty1, ty2]) right_id) e
left_expr ty1 ty2 e = noLoc $ HsApp (noLoc $ mkHsWrap (mkWpTyApps [ty1, ty2]) left_id ) e
right_expr ty1 ty2 e = noLoc $ HsApp (noLoc $ mkHsWrap (mkWpTyApps [ty1, ty2]) right_id) e
-- Prefix each tuple with a distinct series of Left's and Right's,
-- in a balanced way, keeping track of the types.
......
This diff is collapsed.
......@@ -289,8 +289,7 @@ it easier to read debugging output.
Note [Levity polymorphism checking]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
According to the Levity Polymorphism paper
<http://cs.brynmawr.edu/~rae/papers/2017/levity/levity.pdf>, levity
According to the "Levity Polymorphism" paper (PLDI '17), levity
polymorphism is forbidden in precisely two places: in the type of a bound
term-level argument and in the type of an argument to a function. The paper
explains it more fully, but briefly: expressions in these contexts need to be
......
......@@ -689,6 +689,9 @@ data HsExpr id
---------------------------------------
-- Finally, HsWrap appears only in typechecker output
-- The contained Expr is *NOT* itself an HsWrap.
-- See Note [Detecting forced eta expansion] in DsExpr. This invariant
-- is maintained by HsUtils.mkHsWrap.
| HsWrap HsWrapper -- TRANSLATION
(HsExpr id)
......
......@@ -196,7 +196,7 @@ mkHsCaseAlt pat expr
= mkSimpleMatch CaseAlt [pat] expr
nlHsTyApp :: name -> [Type] -> LHsExpr name
nlHsTyApp fun_id tys = noLoc (HsWrap (mkWpTyApps tys) (HsVar (noLoc fun_id)))
nlHsTyApp fun_id tys = noLoc (mkHsWrap (mkWpTyApps tys) (HsVar (noLoc fun_id)))
nlHsTyApps :: name -> [Type] -> [LHsExpr name] -> LHsExpr name
nlHsTyApps fun_id tys xs = foldl nlHsApp (nlHsTyApp fun_id tys) xs
......@@ -654,9 +654,12 @@ typeToLHsType ty
mkLHsWrap :: HsWrapper -> LHsExpr id -> LHsExpr id
mkLHsWrap co_fn (L loc e) = L loc (mkHsWrap co_fn e)
-- Avoid (HsWrap co (HsWrap co' _)).
-- See Note [Detecting forced eta expansion] in DsExpr
mkHsWrap :: HsWrapper -> HsExpr id -> HsExpr id
mkHsWrap co_fn e | isIdHsWrapper co_fn = e
| otherwise = HsWrap co_fn e
mkHsWrap co_fn (HsWrap co_fn' e) = mkHsWrap (co_fn <.> co_fn') e
mkHsWrap co_fn e = HsWrap co_fn e
mkHsWrapCo :: TcCoercionN -- A Nominal coercion a ~N b
-> HsExpr id -> HsExpr id
......
......@@ -371,7 +371,7 @@ tcLocalBinds (HsIPBinds (IPBinds ip_binds _)) thing_inside
-- Coerces a `t` into a dictionry for `IP "x" t`.
-- co : t -> IP "x" t
toDict ipClass x ty = HsWrap $ mkWpCastR $
toDict ipClass x ty = mkHsWrap $ mkWpCastR $
wrapIP $ mkClassPred ipClass [x,ty]
{- Note [Implicit parameter untouchables]
......
......@@ -211,7 +211,7 @@ tcExpr e@(HsIPVar x) res_ty
ip_ty res_ty }
where
-- Coerces a dictionary for `IP "x" t` into `t`.
fromDict ipClass x ty = HsWrap $ mkWpCastR $
fromDict ipClass x ty = mkHsWrap $ mkWpCastR $
unwrapIP $ mkClassPred ipClass [x,ty]
origin = IPOccOrigin x
......@@ -230,7 +230,7 @@ tcExpr e@(HsOverLabel mb_fromLabel l) res_ty
where
-- Coerces a dictionary for `IsLabel "x" t` into `t`,
-- or `HasField "x" r a into `r -> a`.
fromDict pred = HsWrap $ mkWpCastR $ unwrapIP pred
fromDict pred = mkHsWrap $ mkWpCastR $ unwrapIP pred
origin = OverLabelOrigin l
lbl = mkStrLitTy l
......@@ -354,8 +354,8 @@ tcExpr expr@(OpApp arg1 op fix arg2) res_ty
tc_poly_expr_nc arg2 arg2_exp_ty
; arg2_ty <- readExpType arg2_exp_ty
; op_id <- tcLookupId op_name
; let op' = L loc (HsWrap (mkWpTyApps [arg1_ty, arg2_ty])
(HsVar (L lv op_id)))
; let op' = L loc (mkHsWrap (mkWpTyApps [arg1_ty, arg2_ty])
(HsVar (L lv op_id)))
; return $ OpApp arg1' op' fix arg2' }
| (L loc (HsVar (L lv op_name))) <- op
......@@ -392,10 +392,10 @@ tcExpr expr@(OpApp arg1 op fix arg2) res_ty
; op_id <- tcLookupId op_name
; res_ty <- readExpType res_ty
; let op' = L loc (HsWrap (mkWpTyApps [ getRuntimeRep "tcExpr ($)" res_ty
, arg2_sigma
, res_ty])
(HsVar (L lv op_id)))
; let op' = L loc (mkHsWrap (mkWpTyApps [ getRuntimeRep "tcExpr ($)" res_ty
, arg2_sigma
, res_ty])
(HsVar (L lv op_id)))
-- arg1' :: arg1_ty
-- wrap_arg1 :: arg1_ty "->" (arg2_sigma -> op_res_ty)
-- wrap_res :: op_res_ty "->" res_ty
......@@ -1793,7 +1793,7 @@ tcSeq loc fun_name args res_ty
; arg1' <- tcMonoExpr arg1 (mkCheckExpType arg1_ty)
; arg2' <- tcMonoExpr arg2 arg2_exp_ty
; res_ty <- readExpType res_ty -- by now, it's surely filled in
; let fun' = L loc (HsWrap ty_args (HsVar (L loc fun)))
; let fun' = L loc (mkHsWrap ty_args (HsVar (L loc fun)))
ty_args = WpTyApp res_ty <.> WpTyApp arg1_ty
; return (idHsWrapper, fun', [Left arg1', Left arg2']) }
......@@ -1835,7 +1835,7 @@ tcTagToEnum loc fun_name args res_ty
(mk_error ty' doc2)
; arg' <- tcMonoExpr arg (mkCheckExpType intPrimTy)
; let fun' = L loc (HsWrap (WpTyApp rep_ty) (HsVar (L loc fun)))
; let fun' = L loc (mkHsWrap (WpTyApp rep_ty) (HsVar (L loc fun)))
rep_ty = mkTyConApp rep_tc rep_args
; return (mkWpCastR (mkTcSymCo coi), fun', [Left arg']) }
......
......@@ -507,7 +507,7 @@ tcLcStmt m_tc ctxt (TransStmt { trS_form = form, trS_stmts = stmts
poly_arg_ty `mkFunTy` poly_res_ty
; using' <- tcPolyExpr using using_poly_ty
; let final_using = fmap (HsWrap (WpTyApp tup_ty)) using'
; let final_using = fmap (mkHsWrap (WpTyApp tup_ty)) using'
-- 'stmts' returns a result of type (m1_ty tuple_ty),
-- typically something like [(Int,Bool,Int)]
......@@ -689,7 +689,7 @@ tcMcStmt ctxt (TransStmt { trS_stmts = stmts, trS_bndrs = bindersMap
-- using :: ((a,b,c)->t) -> m1 (a,b,c) -> m2 (n (a,b,c))
; using' <- tcPolyExpr using using_poly_ty
; let final_using = fmap (HsWrap (WpTyApp tup_ty)) using'
; let final_using = fmap (mkHsWrap (WpTyApp tup_ty)) using'
--------------- Bulding the bindersMap ----------------
; let mk_n_bndr :: Name -> TcId -> TcId
......
......@@ -574,8 +574,8 @@ runAnnotation target expr = do
-- and hence ensures the appropriate dictionary is bound by const_binds
; wrapper <- instCall AnnOrigin [expr_ty] [mkClassPred data_class [expr_ty]]
; let specialised_to_annotation_wrapper_expr
= L loc (HsWrap wrapper
(HsVar (L loc to_annotation_wrapper_id)))
= L loc (mkHsWrap wrapper
(HsVar (L loc to_annotation_wrapper_id)))
; return (L loc (HsApp specialised_to_annotation_wrapper_expr expr')) }
-- Run the appropriately wrapped expression to get the value of
......
......@@ -11,7 +11,6 @@ module Kind (
isTYPEApp,
returnsTyCon, returnsConstraintKind,
isConstraintKindCon,
okArrowArgKind, okArrowResultKind,
classifiesTypeWithValues,
isStarKind, isStarKindSynonymTyCon,
......@@ -116,17 +115,6 @@ isKindLevPoly k = ASSERT2( isStarKind k || _is_type, ppr k )
= False
--------------------------------------------
-- Kinding for arrow (->)
-- Says when a kind is acceptable on lhs or rhs of an arrow
-- arg -> res
--
-- See Note [Levity polymorphism]
okArrowArgKind, okArrowResultKind :: Kind -> Bool
okArrowArgKind = classifiesTypeWithValues
okArrowResultKind = classifiesTypeWithValues
-----------------------------------------
-- Subkinding
-- The tc variants are used during type-checking, where ConstraintKind
......@@ -162,31 +150,3 @@ isStarKind _ = False
-- | Is the tycon @Constraint@?
isStarKindSynonymTyCon :: TyCon -> Bool
isStarKindSynonymTyCon tc = tc `hasKey` constraintKindTyConKey
{- Note [Levity polymorphism]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Is this type legal?
(a :: TYPE rep) -> Int
where 'rep :: RuntimeRep'
You might think not, because no lambda can have a
runtime-rep-polymorphic binder. So no lambda has the
above type. BUT here's a way it can be useful (taken from
Trac #12708):
data T rep (a :: TYPE rep)
= MkT (a -> Int)
x1 :: T LiftedRep Int
x1 = MkT LiftedRep Int (\x::Int -> 3)
x2 :: T IntRep Int#
x2 = MkT IntRep Int# (\x:Int# -> 3)
Note that the lambdas are just fine!
Hence, okArrowArgKind and okArrowResultKind both just
check that the type is of the form (TYPE r) for some
representation type r.
-}
......@@ -35,4 +35,3 @@ test('T10667', [ when((arch('powerpc64') or arch('powerpc64le')),
compile, ['-g'])
test('T12115', normal, compile, [''])
test('T12355', normal, compile, [''])
test('T13233', expect_broken(13233), compile, [''])
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeInType #-}
{-# LANGUAGE UnboxedTuples #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE MagicHash #-}
module Bug where
import GHC.Exts (TYPE)
import GHC.Exts (TYPE, RuntimeRep, Weak#, State#, RealWorld, mkWeak# )
class Foo (a :: TYPE rep) where
bar :: forall (b :: TYPE rep2). (a -> a -> b) -> a -> a -> b
baz :: forall (a :: TYPE rep). Foo a => a -> a -> (# a, a #)
baz = bar (#,#)
obscure :: (forall (rep1 :: RuntimeRep) (rep2 :: RuntimeRep)
(a :: TYPE rep1) (b :: TYPE rep2).
a -> b -> (# a, b #)) -> ()
obscure _ = ()
quux :: ()
quux = obscure (#,#)
primop :: forall (rep :: RuntimeRep) (a :: TYPE rep) b c.
a -> b -> (State# RealWorld -> (# State# RealWorld, c #))
-> State# RealWorld -> (# State# RealWorld, Weak# b #)
primop = mkWeak#
T13233.hs:14:11: error:
Cannot use primitive with levity-polymorphic arguments:
GHC.Prim.(#,#) :: a -> a -> (# a, a #)
Levity polymorphic arguments:
a :: TYPE rep
a :: TYPE rep
T13233.hs:22:16: error:
Cannot use primitive with levity-polymorphic arguments:
GHC.Prim.(#,#) :: forall (a :: TYPE rep1) (b :: TYPE rep2).
a -> b -> (# a, b #)
Levity polymorphic arguments:
a :: TYPE rep1
b :: TYPE rep2
T13233.hs:27:10: error:
Cannot use primitive with levity-polymorphic arguments:
mkWeak# :: a
-> b
-> (State# RealWorld -> (# State# RealWorld, c #))
-> State# RealWorld
-> (# State# RealWorld, Weak# b #)
Levity polymorphic arguments: a :: TYPE rep
......@@ -3,3 +3,4 @@
# Only the LLVM code generator consistently forces the alignment of
# memcpy operations
test('T8131', [cmm_src, only_ways(llvm_ways)], compile_fail, [''])
test('T13233', normal, compile_fail, [''])
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