[Git][ghc/ghc][wip/T18065] Fix #18065 by fixing an InstCo oversight in Core Lint
Ryan Scott
gitlab at gitlab.haskell.org
Thu Apr 16 17:12:38 UTC 2020
Ryan Scott pushed to branch wip/T18065 at Glasgow Haskell Compiler / GHC
Commits:
cde7683b by Ryan Scott at 2020-04-16T13:10:29-04:00
Fix #18065 by fixing an InstCo oversight in Core Lint
There was a small thinko in Core Lint's treatment of `InstCo`
coercions that ultimately led to #18065. The fix: add an apostrophe.
That's it!
Fixes #18065.
Co-authored-by: Simon Peyton Jones <simonpj at microsoft.com>
- - - - -
3 changed files:
- compiler/GHC/Core/Lint.hs
- + testsuite/tests/indexed-types/should_compile/T18065.hs
- testsuite/tests/indexed-types/should_compile/all.T
Changes:
=====================================
compiler/GHC/Core/Lint.hs
=====================================
@@ -2030,21 +2030,21 @@ lintCoercion the_co@(LRCo lr co)
lintCoercion (InstCo co arg)
= do { co' <- lintCoercion co
; arg' <- lintCoercion arg
- ; let Pair t1' t2' = coercionKind co'
- Pair s1 s2 = coercionKind arg
+ ; let Pair t1 t2 = coercionKind co'
+ Pair s1 s2 = coercionKind arg'
; lintRole arg Nominal (coercionRole arg')
- ; case (splitForAllTy_ty_maybe t1', splitForAllTy_ty_maybe t2') of
+ ; case (splitForAllTy_ty_maybe t1, splitForAllTy_ty_maybe t2) of
-- forall over tvar
{ (Just (tv1,_), Just (tv2,_))
| typeKind s1 `eqType` tyVarKind tv1
, typeKind s2 `eqType` tyVarKind tv2
-> return (InstCo co' arg')
| otherwise
- -> failWithL (text "Kind mis-match in inst coercion")
+ -> failWithL (text "Kind mis-match in inst coercion1" <+> ppr co)
- ; _ -> case (splitForAllTy_co_maybe t1', splitForAllTy_co_maybe t2') of
+ ; _ -> case (splitForAllTy_co_maybe t1, splitForAllTy_co_maybe t2) of
-- forall over covar
{ (Just (cv1, _), Just (cv2, _))
| typeKind s1 `eqType` varType cv1
@@ -2053,7 +2053,7 @@ lintCoercion (InstCo co arg)
, CoercionTy _ <- s2
-> return (InstCo co' arg')
| otherwise
- -> failWithL (text "Kind mis-match in inst coercion")
+ -> failWithL (text "Kind mis-match in inst coercion2" <+> ppr co)
; _ -> failWithL (text "Bad argument of inst") }}}
=====================================
testsuite/tests/indexed-types/should_compile/T18065.hs
=====================================
@@ -0,0 +1,108 @@
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TypeApplications #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE UndecidableInstances #-}
+module T18065 where
+
+import Data.Kind
+import Data.List.NonEmpty (NonEmpty(..))
+
+type family Sing :: k -> Type
+data TyFun :: Type -> Type -> Type
+type a ~> b = TyFun a b -> Type
+infixr 0 ~>
+type family Apply (f :: a ~> b) (x :: a) :: b
+
+type SingFunction1 f = forall t. Sing t -> Sing (f `Apply` t)
+singFun1 :: forall f. SingFunction1 f -> Sing f
+singFun1 f = SLambda f
+
+type SingFunction2 f = forall t1 t2. Sing t1 -> Sing t2 -> Sing (f `Apply` t1 `Apply` t2)
+singFun2 :: forall f. SingFunction2 f -> Sing f
+singFun2 f = SLambda (\x -> singFun1 (f x))
+
+newtype SLambda (f :: a ~> b) =
+ SLambda { applySing :: forall t. Sing t -> Sing (f `Apply` t) }
+type instance Sing = SLambda
+
+data SList :: forall a. [a] -> Type where
+ SNil :: SList '[]
+ SCons :: Sing x -> Sing xs -> SList (x:xs)
+type instance Sing = SList
+
+data SNonEmpty :: forall a. NonEmpty a -> Type where
+ (:%|) :: Sing x -> Sing xs -> SNonEmpty (x:|xs)
+type instance Sing = SNonEmpty
+
+type family Id (x :: a) :: a where
+ Id x = x
+data IdSym0 :: a ~> a
+type instance Apply IdSym0 x = Id x
+sId :: forall a (x :: a). Sing x -> Sing (Id x)
+sId sx = sx
+
+type family (.) (f :: b ~> c) (g :: a ~> b) (x :: a) :: c where
+ (f . g) x = f `Apply` (g `Apply` x)
+data (.@#@$) :: (b ~> c) ~> (a ~> b) ~> a ~> c
+data (.@#@$$) :: (b ~> c) -> (a ~> b) ~> a ~> c
+data (.@#@$$$) :: (b ~> c) -> (a ~> b) -> a ~> c
+type instance Apply (.@#@$) f = (.@#@$$) f
+type instance Apply ((.@#@$$) f) g = (.@#@$$$) f g
+type instance Apply ((.@#@$$$) f g) x = (f . g) x
+(%.) :: forall b c a (f :: b ~> c) (g :: a ~> b) (x :: a).
+ Sing f -> Sing g -> Sing x -> Sing ((f . g) x)
+(%.) sf sg sx = sf `applySing` (sg `applySing` sx)
+
+type family Go (k :: a ~> b ~> b) (z :: b) (l :: [a]) :: b where
+ Go _ z '[] = z
+ Go k z (y:ys) = k `Apply` y `Apply` Go k z ys
+data GoSym :: (a ~> b ~> b) -> b -> [a] ~> b
+type instance Apply (GoSym k z) l = Go k z l
+type family Listfoldr (k :: a ~> b ~> b) (z :: b) (l :: [a]) :: b where
+ Listfoldr k z l = Go k z l
+sListfoldr :: forall a b (k :: a ~> b ~> b) (z :: b) (l :: [a]).
+ Sing k -> Sing z -> Sing l -> Sing (Listfoldr k z l)
+sListfoldr sk sz = sGo
+ where
+ sGo :: forall l'. Sing l' -> Sing (GoSym k z `Apply` l')
+ sGo SNil = sz
+ sGo (sy `SCons` sys) = sk `applySing` sy `applySing` sGo sys
+
+class PMonoid a where
+ type Mempty :: a
+ type Mappend (x :: a) (y :: a) :: a
+data MappendSym0 :: a ~> a ~> a
+data MappendSym1 :: a -> a ~> a
+type instance Apply MappendSym0 x = MappendSym1 x
+type instance Apply (MappendSym1 x) y = Mappend x y
+class SMonoid a where
+ sMempty :: Sing (Mempty :: a)
+ sMappend :: forall (x :: a) (y :: a). Sing x -> Sing y -> Sing (Mappend x y)
+
+class PFoldable t where
+ type Foldr (f :: a ~> b ~> b) (z :: b) (l :: t a) :: b
+instance PFoldable [] where
+ type Foldr f z l = Listfoldr f z l
+class SFoldable t where
+ sFoldr :: forall a b (f :: a ~> b ~> b) (z :: b) (l :: t a).
+ Sing f -> Sing z -> Sing l -> Sing (Foldr f z l)
+instance SFoldable [] where
+ sFoldr = sListfoldr
+
+type family FoldMap (f :: a ~> m) (l :: t a) :: m where
+ FoldMap f l = Foldr (MappendSym0 .@#@$$$ f) Mempty l
+sFoldMap :: forall t a m (f :: a ~> m) (l :: t a).
+ (SFoldable t, SMonoid m)
+ => Sing f -> Sing l -> Sing (FoldMap f l)
+sFoldMap sf = sFoldr (singFun2 @((.@#@$$) MappendSym0) (singFun2 @MappendSym0 sMappend %.) `applySing` sf) sMempty
+
+type family NEFold (l :: NonEmpty m) :: m where
+ NEFold (a :| as) = a `Mappend` FoldMap IdSym0 as
+sNEFold :: forall m (l :: NonEmpty m). SMonoid m
+ => Sing l -> Sing (NEFold l)
+sNEFold (sa :%| sas) = sa `sMappend` sFoldMap (singFun1 @IdSym0 sId) sas
=====================================
testsuite/tests/indexed-types/should_compile/all.T
=====================================
@@ -295,3 +295,4 @@ test('T17008b', normal, compile, [''])
test('T17056', normal, compile, [''])
test('T17405', normal, multimod_compile, ['T17405c', '-v0'])
test('T17923', normal, compile, [''])
+test('T18065', normal, compile, ['-O'])
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/cde7683be2c71f6142aa5f39ff18f0ab9a170f75
--
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/cde7683be2c71f6142aa5f39ff18f0ab9a170f75
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/20200416/427bfc94/attachment-0001.html>
More information about the ghc-commits
mailing list