[Git][ghc/ghc][wip/marge_bot_batch_merge_job] 6 commits: Make 'undefined x' linear in 'x' (#18731)
Marge Bot
gitlab at gitlab.haskell.org
Sun Sep 27 08:53:41 UTC 2020
Marge Bot pushed to branch wip/marge_bot_batch_merge_job at Glasgow Haskell Compiler / GHC
Commits:
bda55fa0 by Krzysztof Gogolewski at 2020-09-26T13:18:22-04:00
Make 'undefined x' linear in 'x' (#18731)
- - - - -
160fba4a by Krzysztof Gogolewski at 2020-09-26T13:19:00-04:00
Disallow linear types in FFI (#18472)
- - - - -
e124f2a7 by Krzysztof Gogolewski at 2020-09-26T13:19:36-04:00
Fix handling of function coercions (#18747)
This was broken when we added multiplicity to the function type.
- - - - -
7ff43382 by Vladislav Zavialov at 2020-09-27T03:01:31+03:00
Comments: change outdated reference to mergeOps
As of 686e06c59c3aa6b66895e8a501c7afb019b09e36,
GHC.Parser.PostProcess.mergeOps no longer exists.
[ci skip]
- - - - -
6c1961cd by Vladislav Zavialov at 2020-09-27T04:53:32-04:00
Don't rearrange (->) in the renamer
The parser produces an AST where the (->)
is already associated correctly:
1. (->) has the least possible precedence
2. (->) is right-associative
Thus we don't need to handle it in mkHsOpTyRn.
- - - - -
340e69a7 by Vladislav Zavialov at 2020-09-27T04:53:32-04:00
Remove outdated comment in rnHsTyKi
This comment dates back to 3df40b7b78044206bbcffe3e2c0a57d901baf5e8
and does not seem relevant anymore.
- - - - -
13 changed files:
- compiler/GHC/Core/Coercion.hs
- compiler/GHC/Hs/Decls.hs
- compiler/GHC/Rename/HsType.hs
- compiler/GHC/Tc/Gen/App.hs
- compiler/GHC/Tc/Gen/Foreign.hs
- + testsuite/tests/linear/should_compile/T18731.hs
- testsuite/tests/linear/should_compile/all.T
- + testsuite/tests/linear/should_fail/LinearFFI.hs
- + testsuite/tests/linear/should_fail/LinearFFI.stderr
- testsuite/tests/linear/should_fail/all.T
- + testsuite/tests/simplCore/should_compile/T18747A.hs
- + testsuite/tests/simplCore/should_compile/T18747B.hs
- testsuite/tests/simplCore/should_compile/all.T
Changes:
=====================================
compiler/GHC/Core/Coercion.hs
=====================================
@@ -1486,7 +1486,7 @@ instCoercion (Pair lty rty) g w
| isFunTy lty && isFunTy rty
-- g :: (t1 -> t2) ~ (t3 -> t4)
-- returns t2 ~ t4
- = Just $ mkNthCo Nominal 3 g -- extract result type, which is the 4th argument to (->)
+ = Just $ mkNthCo Nominal 4 g -- extract result type, which is the 5th argument to (->)
| otherwise -- one forall, one funty...
= Nothing
=====================================
compiler/GHC/Hs/Decls.hs
=====================================
@@ -1566,7 +1566,7 @@ all we are concerned about in the parser is identifying the overall shape of
the argument and result types, which we can accomplish by piggybacking on the
special treatment given to function arrows. In a future where function arrows
aren't given special status in the parser, we will likely have to modify
-GHC.Parser.PostProcess.mergeOps to preserve this trick.
+GHC.Parser.PostProcess.mkHsOpTyPV to preserve this trick.
-----
-- Wrinkle: No nested foralls or contexts
=====================================
compiler/GHC/Rename/HsType.hs
=====================================
@@ -52,14 +52,13 @@ import GHC.Rename.Fixity ( lookupFieldFixityRn, lookupFixityRn
import GHC.Tc.Utils.Monad
import GHC.Types.Name.Reader
import GHC.Builtin.Names
-import GHC.Builtin.Types.Prim ( funTyConName )
import GHC.Types.Name
import GHC.Types.SrcLoc
import GHC.Types.Name.Set
import GHC.Types.FieldLabel
import GHC.Utils.Misc
-import GHC.Types.Basic ( compareFixity, funTyFixity, negateFixity
+import GHC.Types.Basic ( compareFixity, negateFixity
, Fixity(..), FixityDirection(..), LexicalFixity(..)
, TypeOrKind(..) )
import GHC.Utils.Outputable
@@ -600,8 +599,7 @@ rnHsTyKi env ty@(HsOpTy _ ty1 l_op ty2)
; fix <- lookupTyFixityRn l_op'
; (ty1', fvs2) <- rnLHsTyKi env ty1
; (ty2', fvs3) <- rnLHsTyKi env ty2
- ; res_ty <- mkHsOpTyRn (\t1 t2 -> HsOpTy noExtField t1 l_op' t2)
- (unLoc l_op') fix ty1' ty2'
+ ; res_ty <- mkHsOpTyRn l_op' fix ty1' ty2'
; return (res_ty, plusFVs [fvs1, fvs2, fvs3]) }
rnHsTyKi env (HsParTy _ ty)
@@ -627,17 +625,10 @@ rnHsTyKi env ty@(HsRecTy _ flds)
rnHsTyKi env (HsFunTy _ mult ty1 ty2)
= do { (ty1', fvs1) <- rnLHsTyKi env ty1
- -- Might find a for-all as the arg of a function type
; (ty2', fvs2) <- rnLHsTyKi env ty2
- -- Or as the result. This happens when reading Prelude.hi
- -- when we find return :: forall m. Monad m -> forall a. a -> m a
-
- -- Check for fixity rearrangements
; (mult', w_fvs) <- rnHsArrow env mult
- ; res_ty <- mkHsOpTyRn (hs_fun_ty mult') funTyConName funTyFixity ty1' ty2'
- ; return (res_ty, fvs1 `plusFV` fvs2 `plusFV` w_fvs) }
- where
- hs_fun_ty w a b = HsFunTy noExtField w a b
+ ; return (HsFunTy noExtField mult' ty1' ty2'
+ , plusFVs [fvs1, fvs2, w_fvs]) }
rnHsTyKi env listTy@(HsListTy _ ty)
= do { data_kinds <- xoptM LangExt.DataKinds
@@ -1210,46 +1201,41 @@ is always read in as
a `op` (b `op` c)
mkHsOpTyRn rearranges where necessary. The two arguments
-have already been renamed and rearranged. It's made rather tiresome
-by the presence of ->, which is a separate syntactic construct.
+have already been renamed and rearranged.
+
+In the past, mkHsOpTyRn used to handle (->), but this was unnecessary. In the
+syntax tree produced by the parser, the arrow already has the least possible
+precedence and does not require rearrangement.
-}
---------------
-- Building (ty1 `op1` (ty21 `op2` ty22))
-mkHsOpTyRn :: (LHsType GhcRn -> LHsType GhcRn -> HsType GhcRn)
- -> Name -> Fixity -> LHsType GhcRn -> LHsType GhcRn
+mkHsOpTyRn :: Located Name -> Fixity -> LHsType GhcRn -> LHsType GhcRn
-> RnM (HsType GhcRn)
-mkHsOpTyRn mk1 pp_op1 fix1 ty1 (L loc2 (HsOpTy noExtField ty21 op2 ty22))
+mkHsOpTyRn op1 fix1 ty1 (L loc2 (HsOpTy _ ty21 op2 ty22))
= do { fix2 <- lookupTyFixityRn op2
- ; mk_hs_op_ty mk1 pp_op1 fix1 ty1
- (\t1 t2 -> HsOpTy noExtField t1 op2 t2)
- (unLoc op2) fix2 ty21 ty22 loc2 }
-
-mkHsOpTyRn mk1 pp_op1 fix1 ty1 (L loc2 (HsFunTy _ mult ty21 ty22))
- = mk_hs_op_ty mk1 pp_op1 fix1 ty1
- hs_fun_ty funTyConName funTyFixity ty21 ty22 loc2
- where
- hs_fun_ty a b = HsFunTy noExtField mult a b
+ ; mk_hs_op_ty op1 fix1 ty1 op2 fix2 ty21 ty22 loc2 }
-mkHsOpTyRn mk1 _ _ ty1 ty2 -- Default case, no rearrangment
- = return (mk1 ty1 ty2)
+mkHsOpTyRn op1 _ ty1 ty2 -- Default case, no rearrangment
+ = return (HsOpTy noExtField ty1 op1 ty2)
---------------
-mk_hs_op_ty :: (LHsType GhcRn -> LHsType GhcRn -> HsType GhcRn)
- -> Name -> Fixity -> LHsType GhcRn
- -> (LHsType GhcRn -> LHsType GhcRn -> HsType GhcRn)
- -> Name -> Fixity -> LHsType GhcRn -> LHsType GhcRn -> SrcSpan
+mk_hs_op_ty :: Located Name -> Fixity -> LHsType GhcRn
+ -> Located Name -> Fixity -> LHsType GhcRn
+ -> LHsType GhcRn -> SrcSpan
-> RnM (HsType GhcRn)
-mk_hs_op_ty mk1 op1 fix1 ty1
- mk2 op2 fix2 ty21 ty22 loc2
- | nofix_error = do { precParseErr (NormalOp op1,fix1) (NormalOp op2,fix2)
- ; return (mk1 ty1 (L loc2 (mk2 ty21 ty22))) }
- | associate_right = return (mk1 ty1 (L loc2 (mk2 ty21 ty22)))
+mk_hs_op_ty op1 fix1 ty1 op2 fix2 ty21 ty22 loc2
+ | nofix_error = do { precParseErr (NormalOp (unLoc op1),fix1)
+ (NormalOp (unLoc op2),fix2)
+ ; return (ty1 `op1ty` (L loc2 (ty21 `op2ty` ty22))) }
+ | associate_right = return (ty1 `op1ty` (L loc2 (ty21 `op2ty` ty22)))
| otherwise = do { -- Rearrange to ((ty1 `op1` ty21) `op2` ty22)
- new_ty <- mkHsOpTyRn mk1 op1 fix1 ty1 ty21
- ; return (mk2 (noLoc new_ty) ty22) }
+ new_ty <- mkHsOpTyRn op1 fix1 ty1 ty21
+ ; return (noLoc new_ty `op2ty` ty22) }
where
+ lhs `op1ty` rhs = HsOpTy noExtField lhs op1 rhs
+ lhs `op2ty` rhs = HsOpTy noExtField lhs op2 rhs
(nofix_error, associate_right) = compareFixity fix1 fix2
=====================================
compiler/GHC/Tc/Gen/App.hs
=====================================
@@ -19,6 +19,7 @@ module GHC.Tc.Gen.App
import {-# SOURCE #-} GHC.Tc.Gen.Expr( tcCheckPolyExprNC )
+import GHC.Builtin.Types (multiplicityTy)
import GHC.Tc.Gen.Head
import GHC.Hs
import GHC.Tc.Utils.Monad
@@ -499,13 +500,17 @@ tcInstFun do_ql inst_final rn_fun fun_sigma rn_args
-- - We need the freshly allocated unification variables, to extend
-- delta with.
-- It's easier just to do the job directly here.
- do { arg_nus <- replicateM (countLeadingValArgs args) newOpenFlexiTyVar
+ do { let valArgsCount = countLeadingValArgs args
+ ; arg_nus <- replicateM valArgsCount newOpenFlexiTyVar
+ -- We need variables for multiplicity (#18731)
+ -- Otherwise, 'undefined x' wouldn't be linear in x
+ ; mults <- replicateM valArgsCount (newFlexiTyVarTy multiplicityTy)
; res_nu <- newOpenFlexiTyVar
; kind_co <- unifyKind Nothing liftedTypeKind (tyVarKind kappa)
; let delta' = delta `extendVarSetList` (res_nu:arg_nus)
arg_tys = mkTyVarTys arg_nus
res_ty = mkTyVarTy res_nu
- fun_ty' = mkVisFunTysMany arg_tys res_ty
+ fun_ty' = mkVisFunTys (zipWithEqual "tcInstFun" mkScaled mults arg_tys) res_ty
co_wrap = mkWpCastN (mkTcGReflLeftCo Nominal fun_ty' kind_co)
acc' = addArgWrap co_wrap acc
-- Suppose kappa :: kk
=====================================
compiler/GHC/Tc/Gen/Foreign.hs
=====================================
@@ -243,7 +243,7 @@ tcFImport (L dloc fo@(ForeignImport { fd_name = L nloc nm, fd_sig_ty = hs_ty
-- things are LocalIds. However, it does not need zonking,
-- (so GHC.Tc.Utils.Zonk.zonkForeignExports ignores it).
- ; imp_decl' <- tcCheckFIType (map scaledThing arg_tys) res_ty imp_decl
+ ; imp_decl' <- tcCheckFIType arg_tys res_ty imp_decl
-- Can't use sig_ty here because sig_ty :: Type and
-- we need HsType Id hence the undefined
; let fi_decl = ForeignImport { fd_name = L nloc id
@@ -255,14 +255,14 @@ tcFImport d = pprPanic "tcFImport" (ppr d)
-- ------------ Checking types for foreign import ----------------------
-tcCheckFIType :: [Type] -> Type -> ForeignImport -> TcM ForeignImport
+tcCheckFIType :: [Scaled Type] -> Type -> ForeignImport -> TcM ForeignImport
tcCheckFIType arg_tys res_ty (CImport (L lc cconv) safety mh l@(CLabel _) src)
-- Foreign import label
= do checkCg checkCOrAsmOrLlvmOrInterp
-- NB check res_ty not sig_ty!
-- In case sig_ty is (forall a. ForeignPtr a)
- check (isFFILabelTy (mkVisFunTysMany arg_tys res_ty)) (illegalForeignTyErr Outputable.empty)
+ check (isFFILabelTy (mkVisFunTys arg_tys res_ty)) (illegalForeignTyErr Outputable.empty)
cconv' <- checkCConv cconv
return (CImport (L lc cconv') safety mh l src)
@@ -274,7 +274,9 @@ tcCheckFIType arg_tys res_ty (CImport (L lc cconv) safety mh CWrapper src) = do
checkCg checkCOrAsmOrLlvmOrInterp
cconv' <- checkCConv cconv
case arg_tys of
- [arg1_ty] -> do checkForeignArgs isFFIExternalTy (map scaledThing arg1_tys)
+ [Scaled arg1_mult arg1_ty] -> do
+ checkNoLinearFFI arg1_mult
+ checkForeignArgs isFFIExternalTy arg1_tys
checkForeignRes nonIOok checkSafe isFFIExportResultTy res1_ty
checkForeignRes mustBeIO checkSafe (isFFIDynTy arg1_ty) res_ty
where
@@ -290,9 +292,10 @@ tcCheckFIType arg_tys res_ty idecl@(CImport (L lc cconv) (L ls safety) mh
case arg_tys of -- The first arg must be Ptr or FunPtr
[] ->
addErrTc (illegalForeignTyErr Outputable.empty (text "At least one argument expected"))
- (arg1_ty:arg_tys) -> do
+ (Scaled arg1_mult arg1_ty:arg_tys) -> do
dflags <- getDynFlags
- let curried_res_ty = mkVisFunTysMany arg_tys res_ty
+ let curried_res_ty = mkVisFunTys arg_tys res_ty
+ checkNoLinearFFI arg1_mult
check (isFFIDynTy curried_res_ty arg1_ty)
(illegalForeignTyErr argument)
checkForeignArgs (isFFIArgumentTy dflags safety) arg_tys
@@ -317,7 +320,7 @@ tcCheckFIType arg_tys res_ty idecl@(CImport (L lc cconv) (L ls safety) mh
dflags <- getDynFlags
checkForeignArgs (isFFIArgumentTy dflags safety) arg_tys
checkForeignRes nonIOok checkSafe (isFFIImportResultTy dflags) res_ty
- checkMissingAmpersand dflags arg_tys res_ty
+ checkMissingAmpersand dflags (map scaledThing arg_tys) res_ty
case target of
StaticTarget _ _ _ False
| not (null arg_tys) ->
@@ -405,7 +408,7 @@ tcCheckFEType sig_ty (CExport (L l (CExportStatic esrc str cconv)) src) = do
checkCg checkCOrAsmOrLlvm
checkTc (isCLabelString str) (badCName str)
cconv' <- checkCConv cconv
- checkForeignArgs isFFIExternalTy (map scaledThing arg_tys)
+ checkForeignArgs isFFIExternalTy arg_tys
checkForeignRes nonIOok noCheckSafe isFFIExportResultTy res_ty
return (CExport (L l (CExportStatic esrc str cconv')) src)
where
@@ -422,10 +425,16 @@ tcCheckFEType sig_ty (CExport (L l (CExportStatic esrc str cconv)) src) = do
-}
------------ Checking argument types for foreign import ----------------------
-checkForeignArgs :: (Type -> Validity) -> [Type] -> TcM ()
+checkForeignArgs :: (Type -> Validity) -> [Scaled Type] -> TcM ()
checkForeignArgs pred tys = mapM_ go tys
where
- go ty = check (pred ty) (illegalForeignTyErr argument)
+ go (Scaled mult ty) = checkNoLinearFFI mult >>
+ check (pred ty) (illegalForeignTyErr argument)
+
+checkNoLinearFFI :: Mult -> TcM () -- No linear types in FFI (#18472)
+checkNoLinearFFI Many = return ()
+checkNoLinearFFI _ = addErrTc $ illegalForeignTyErr argument
+ (text "Linear types are not supported in FFI declarations, see #18472")
------------ Checking result types for foreign calls ----------------------
-- | Check that the type has the form
=====================================
testsuite/tests/linear/should_compile/T18731.hs
=====================================
@@ -0,0 +1,5 @@
+{-# LANGUAGE LinearTypes #-}
+module T18731 where
+
+f :: a #-> b
+f x = undefined x
=====================================
testsuite/tests/linear/should_compile/all.T
=====================================
@@ -36,3 +36,4 @@ test('LinearLetRec', expect_broken(405), compile, ['-O -dlinear-core-lint'])
test('LinearTH1', normal, compile, [''])
test('LinearTH2', expect_broken(broken_multiplicity_syntax), compile, [''])
test('LinearHole', normal, compile, [''])
+test('T18731', normal, compile, [''])
=====================================
testsuite/tests/linear/should_fail/LinearFFI.hs
=====================================
@@ -0,0 +1,8 @@
+{-# LANGUAGE LinearTypes #-}
+module LinearFFI where -- #18472
+
+import Foreign.Ptr
+
+foreign import ccall "exp" c_exp :: Double #-> Double
+foreign import stdcall "dynamic" d8 :: FunPtr (IO Int) #-> IO Int
+foreign import ccall "wrapper" mkF :: IO () #-> IO (FunPtr (IO ()))
=====================================
testsuite/tests/linear/should_fail/LinearFFI.stderr
=====================================
@@ -0,0 +1,20 @@
+
+LinearFFI.hs:6:1: error:
+ • Unacceptable argument type in foreign declaration:
+ Linear types are not supported in FFI declarations, see #18472
+ • When checking declaration:
+ foreign import ccall safe "exp" c_exp :: Double #-> Double
+
+LinearFFI.hs:7:1: error:
+ • Unacceptable argument type in foreign declaration:
+ Linear types are not supported in FFI declarations, see #18472
+ • When checking declaration:
+ foreign import stdcall safe "dynamic" d8
+ :: FunPtr (IO Int) #-> IO Int
+
+LinearFFI.hs:8:1: error:
+ • Unacceptable argument type in foreign declaration:
+ Linear types are not supported in FFI declarations, see #18472
+ • When checking declaration:
+ foreign import ccall safe "wrapper" mkF
+ :: IO () #-> IO (FunPtr (IO ()))
=====================================
testsuite/tests/linear/should_fail/all.T
=====================================
@@ -28,3 +28,4 @@ test('LinearBottomMult', normal, compile_fail, [''])
test('LinearSequenceExpr', normal, compile_fail, [''])
test('LinearIf', normal, compile_fail, [''])
test('LinearPatternGuardWildcard', normal, compile_fail, [''])
+test('LinearFFI', normal, compile_fail, [''])
=====================================
testsuite/tests/simplCore/should_compile/T18747A.hs
=====================================
@@ -0,0 +1,82 @@
+{-# LANGUAGE AllowAmbiguousTypes #-}
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE TypeOperators #-}
+module T18747A where
+
+import Data.Kind
+import Data.Type.Equality
+
+type family Sing :: k -> Type
+data SomeSing :: Type -> Type where
+ SomeSing :: Sing (a :: k) -> SomeSing k
+
+data SList :: forall a. [a] -> Type where
+ SNil :: SList '[]
+ SCons :: Sing x -> Sing xs -> SList (x:xs)
+type instance Sing = SList
+
+data Univ = U1 | K1 Type | Sum Univ Univ | Product Univ Univ
+
+data SUniv :: Univ -> Type where
+ SU1 :: SUniv U1
+ SK1 :: Sing c -> SUniv (K1 c)
+ SSum :: Sing a -> Sing b -> SUniv (Sum a b)
+ SProduct :: Sing a -> Sing b -> SUniv (Product a b)
+type instance Sing = SUniv
+
+data In :: Univ -> Type where
+ MkU1 :: In U1
+ MkK1 :: c -> In (K1 c)
+ L1 :: In a -> In (Sum a b)
+ R1 :: In b -> In (Sum a b)
+ MkProduct :: In a -> In b -> In (Product a b)
+
+data SIn :: forall u. In u -> Type where
+ SMkU1 :: SIn MkU1
+ SMkK1 :: Sing c -> SIn (MkK1 c)
+ SL1 :: Sing a -> SIn (L1 a)
+ SR1 :: Sing b -> SIn (R1 b)
+ SMkProduct :: Sing a -> Sing b -> SIn (MkProduct a b)
+type instance Sing = SIn
+
+class Generic (a :: Type) where
+ type Rep a :: Univ
+ from :: a -> In (Rep a)
+ to :: In (Rep a) -> a
+
+class PGeneric (a :: Type) where
+ type PFrom (x :: a) :: In (Rep a)
+ type PTo (x :: In (Rep a)) :: a
+
+class SGeneric k where
+ sFrom :: forall (a :: k). Sing a -> Sing (PFrom a)
+ sTo :: forall (a :: In (Rep k)). Sing a -> Sing (PTo a :: k)
+ sTof :: forall (a :: k). Sing a -> PTo (PFrom a) :~: a
+ sFot :: forall (a :: In (Rep k)). Sing a -> PFrom (PTo a :: k) :~: a
+
+instance Generic [a] where
+ type Rep [a] = Sum U1 (Product (K1 a) (K1 [a]))
+ from [] = L1 MkU1
+ from (x:xs) = R1 (MkProduct (MkK1 x) (MkK1 xs))
+ to (L1 MkU1) = []
+ to (R1 (MkProduct (MkK1 x) (MkK1 xs))) = x:xs
+
+instance PGeneric [a] where
+ type PFrom '[] = L1 MkU1
+ type PFrom (x:xs) = R1 (MkProduct (MkK1 x) (MkK1 xs))
+ type PTo (L1 MkU1) = '[]
+ type PTo (R1 (MkProduct (MkK1 x) (MkK1 xs))) = x:xs
+
+instance SGeneric [a] where
+ sFrom SNil = SL1 SMkU1
+ sFrom (SCons x xs) = SR1 (SMkProduct (SMkK1 x) (SMkK1 xs))
+ sTo (SL1 SMkU1) = SNil
+ sTo (SR1 (SMkProduct (SMkK1 x) (SMkK1 xs))) = SCons x xs
+ sTof SNil = Refl
+ sTof SCons{} = Refl
+ sFot (SL1 SMkU1) = Refl
+ sFot (SR1 (SMkProduct SMkK1{} SMkK1{})) = Refl
=====================================
testsuite/tests/simplCore/should_compile/T18747B.hs
=====================================
@@ -0,0 +1,50 @@
+{-# LANGUAGE ConstraintKinds #-}
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE UndecidableInstances #-}
+module T18747B where
+
+import Data.Kind
+import Data.Type.Equality
+
+type family Sing :: k -> Type
+
+data SomeSing (k :: Type) where
+ SomeSing :: Sing (a :: k) -> SomeSing k
+
+type family Promote (k :: Type) :: Type
+type family PromoteX (a :: k) :: Promote k
+
+type family Demote (k :: Type) :: Type
+type family DemoteX (a :: k) :: Demote k
+
+type SingKindX (a :: k) = (PromoteX (DemoteX a) ~~ a)
+
+class SingKindX k => SingKind k where
+ toSing :: Demote k -> SomeSing k
+
+type instance Demote Type = Type
+type instance Promote Type = Type
+type instance DemoteX (a :: Type) = Demote a
+type instance PromoteX (a :: Type) = Promote a
+
+type instance Demote Bool = Bool
+type instance Promote Bool = Bool
+
+data Foo (a :: Type) where MkFoo :: Foo Bool
+
+data SFoo :: forall a. Foo a -> Type where
+ SMkFoo :: SFoo MkFoo
+type instance Sing = SFoo
+
+type instance Demote (Foo a) = Foo (DemoteX a)
+type instance Promote (Foo a) = Foo (PromoteX a)
+
+instance SingKindX a => SingKind (Foo a) where
+ toSing MkFoo = SomeSing SMkFoo
+
=====================================
testsuite/tests/simplCore/should_compile/all.T
=====================================
@@ -338,3 +338,5 @@ test('T18603', normal, compile, ['-dcore-lint -O'])
# T18649 should /not/ generate a specialisation rule
test('T18649', normal, compile, ['-O -ddump-rules -Wno-simplifiable-class-constraints'])
+test('T18747A', normal, compile, [''])
+test('T18747B', normal, compile, [''])
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/compare/4149828c2935eed35dfdd27c128836adcaf89fae...340e69a751dd1d329ae16a9f50c58b9183535edc
--
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/compare/4149828c2935eed35dfdd27c128836adcaf89fae...340e69a751dd1d329ae16a9f50c58b9183535edc
You're receiving this email because of your account on gitlab.haskell.org.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/ghc-commits/attachments/20200927/74dbd133/attachment-0001.html>
More information about the ghc-commits
mailing list