diff options
author | Ryan Scott <ryan.gl.scott@gmail.com> | 2020-04-16 13:00:34 -0400 |
---|---|---|
committer | Marge Bot <ben+marge-bot@smart-cactus.org> | 2020-04-17 12:46:02 -0400 |
commit | bfde3b76ac7f5a72eca012fe34ac1340a5ce2011 (patch) | |
tree | 0a68b028e000ab53ad38b5b7f8125d59614fa86d | |
parent | 85fc32f03a6df92ec8d4ec9accca3c11b31a1596 (diff) | |
download | haskell-bfde3b76ac7f5a72eca012fe34ac1340a5ce2011.tar.gz |
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@microsoft.com>
-rw-r--r-- | compiler/GHC/Core/Lint.hs | 12 | ||||
-rw-r--r-- | testsuite/tests/indexed-types/should_compile/T18065.hs | 108 | ||||
-rw-r--r-- | testsuite/tests/indexed-types/should_compile/all.T | 1 |
3 files changed, 115 insertions, 6 deletions
diff --git a/compiler/GHC/Core/Lint.hs b/compiler/GHC/Core/Lint.hs index 8bc9709c5f..fb530cb2c7 100644 --- a/compiler/GHC/Core/Lint.hs +++ b/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") }}} diff --git a/testsuite/tests/indexed-types/should_compile/T18065.hs b/testsuite/tests/indexed-types/should_compile/T18065.hs new file mode 100644 index 0000000000..e63f624ca8 --- /dev/null +++ b/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 diff --git a/testsuite/tests/indexed-types/should_compile/all.T b/testsuite/tests/indexed-types/should_compile/all.T index ccca063fd2..21703374b9 100644 --- a/testsuite/tests/indexed-types/should_compile/all.T +++ b/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']) |