Commit 424ecadb authored by Ryan Scott's avatar Ryan Scott
Browse files

Add regression tests for #13601, #13780, #13877

Summary:
Some recent commits happened to fix other issues:

* c2417b87 fixed #13601 and #13780
* 8e15e3d3 fixed the original program in #13877

Let's add regression tests for each of these to ensure they stay fixed.

Test Plan: make test TEST="T13601 T13780a T13780c T13877"

Reviewers: goldfire, bgamari, austin

Reviewed By: bgamari

Subscribers: rwbarton, thomie

GHC Trac Issues: #13601, #13780, #13877

Differential Revision: https://phabricator.haskell.org/D3794
parent b3b564fb
{-# LANGUAGE TypeFamilies, DataKinds, TypeInType #-}
import GHC.Exts
import Prelude (Bool(True,False),Integer,Ordering,undefined)
import qualified Prelude
import Data.Kind
--------------------
-- class hierarchy
type family
Rep (rep :: RuntimeRep) :: RuntimeRep where
-- Rep IntRep = IntRep
-- Rep DoubleRep = IntRep
-- Rep PtrRepUnlifted = IntRep
-- Rep PtrRepLifted = PtrRepLifted
class Boolean (Logic a) => Eq (a :: TYPE rep) where
type Logic (a :: TYPE rep) :: TYPE (Rep rep)
(==) :: a -> a -> Logic a
class Eq a => POrd (a :: TYPE rep) where
inf :: a -> a -> a
class POrd a => MinBound (a :: TYPE rep) where
minBound :: () -> a
class POrd a => Lattice (a :: TYPE rep) where
sup :: a -> a -> a
class (Lattice a, MinBound a) => Bounded (a :: TYPE rep) where
maxBound :: () -> a
class Bounded a => Complemented (a :: TYPE rep) where
not :: a -> a
class Bounded a => Heyting (a :: TYPE rep) where
infixr 3 ==>
(==>) :: a -> a -> a
class (Complemented a, Heyting a) => Boolean a
(||) :: Boolean a => a -> a -> a
(||) = sup
(&&) :: Boolean a => a -> a -> a
(&&) = inf
T13601.hs:18:16: error:
• Expected kind ‘TYPE (Rep 'LiftedRep)’,
but ‘Logic a’ has kind ‘TYPE (Rep rep)’
• In the first argument of ‘Boolean’, namely ‘(Logic a)’
In the class declaration for ‘Eq’
{-# LANGUAGE ExistentialQuantification #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeInType #-}
module T13780a where
data family Sing (a :: k)
data Foo a = a ~ Bool => MkFoo
data instance Sing (z :: Foo a) = (z ~ MkFoo) => SMkFoo
T13780a.hs:9:40: error:
• Expected kind ‘Foo a’, but ‘MkFoo’ has kind ‘Foo Bool’
• In the second argument of ‘(~)’, namely ‘MkFoo’
In the definition of data constructor ‘SMkFoo’
In the data instance declaration for ‘Sing’
{-# LANGUAGE GADTs #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeInType #-}
module T13780b where
data family Sing (a :: k)
data instance Sing (z :: Bool) =
z ~ False => SFalse
| z ~ True => STrue
{-# LANGUAGE GADTs #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeInType #-}
module T13780c where
import Data.Kind
import T13780b
type family ElimBool (p :: Bool -> Type) (b :: Bool) (s :: Sing b)
(pFalse :: p False) (pTrue :: p True) :: p b where
ElimBool _ _ SFalse pFalse _ = pFalse
ElimBool _ _ STrue _ pTrue = pTrue
[1 of 2] Compiling T13780b ( T13780b.hs, T13780b.o )
[2 of 2] Compiling T13780c ( T13780c.hs, T13780c.o )
T13780c.hs:11:16: error:
• Expected kind ‘Sing _’, but ‘SFalse’ has kind ‘Sing 'False’
• In the third argument of ‘ElimBool’, namely ‘SFalse’
In the type family declaration for ‘ElimBool’
T13780c.hs:12:16: error:
• Expected kind ‘Sing _1’, but ‘STrue’ has kind ‘Sing 'True’
• In the third argument of ‘ElimBool’, namely ‘STrue’
In the type family declaration for ‘ElimBool’
......@@ -17,3 +17,7 @@ test('T11471', normal, compile_fail, [''])
test('T12174', normal, compile_fail, [''])
test('T12081', normal, compile_fail, [''])
test('T13135', normal, compile_fail, [''])
test('T13601', normal, compile_fail, [''])
test('T13780a', normal, compile_fail, [''])
test('T13780c', [extra_files(['T13780b.hs'])],
multimod_compile_fail, ['T13780c', ''])
{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE Trustworthy #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeInType #-}
{-# LANGUAGE TypeOperators #-}
module T13877 where
import Data.Kind
data family Sing (a :: k)
data instance Sing (z :: [a]) where
SNil :: Sing '[]
SCons :: Sing x -> Sing xs -> Sing (x:xs)
data TyFun :: * -> * -> *
type a ~> b = TyFun a b -> *
infixr 0 ~>
type family Apply (f :: k1 ~> k2) (x :: k1) :: k2
type a @@ b = Apply a b
infixl 9 @@
data FunArrow = (:->) | (:~>)
class FunType (arr :: FunArrow) where
type Fun (k1 :: Type) arr (k2 :: Type) :: Type
class FunType arr => AppType (arr :: FunArrow) where
type App k1 arr k2 (f :: Fun k1 arr k2) (x :: k1) :: k2
type FunApp arr = (FunType arr, AppType arr)
instance FunType (:->) where
type Fun k1 (:->) k2 = k1 -> k2
instance AppType (:->) where
type App k1 (:->) k2 (f :: k1 -> k2) x = f x
instance FunType (:~>) where
type Fun k1 (:~>) k2 = k1 ~> k2
instance AppType (:~>) where
type App k1 (:~>) k2 (f :: k1 ~> k2) x = f @@ x
infixr 0 -?>
type (-?>) (k1 :: Type) (k2 :: Type) (arr :: FunArrow) = Fun k1 arr k2
listElim :: forall (a :: Type) (p :: [a] -> Type) (l :: [a]).
Sing l
-> p '[]
-> (forall (x :: a) (xs :: [a]). Sing x -> Sing xs -> p xs -> p (x:xs))
-> p l
listElim = listElimPoly @(:->) @a @p @l
listElimTyFun :: forall (a :: Type) (p :: [a] ~> Type) (l :: [a]).
Sing l
-> p @@ '[]
-> (forall (x :: a) (xs :: [a]). Sing x -> Sing xs -> p @@ xs -> p @@ (x:xs))
-> p @@ l
listElimTyFun = listElimPoly @(:->) @a @p @l
listElimPoly :: forall (arr :: FunArrow) (a :: Type) (p :: ([a] -?> Type) arr) (l :: [a]).
FunApp arr
=> Sing l
-> App [a] arr Type p '[]
-> (forall (x :: a) (xs :: [a]). Sing x -> Sing xs -> App [a] arr Type p xs -> App [a] arr Type p (x:xs))
-> App [a] arr Type p l
listElimPoly SNil pNil _ = pNil
listElimPoly (SCons x (xs :: Sing xs)) pNil pCons = pCons x xs (listElimPoly @arr @a @p @xs xs pNil pCons)
T13877.hs:65:17: error:
• Couldn't match type ‘p xs’ with ‘Apply p xs’
Expected type: Sing x
-> Sing xs -> App [a] (':->) * p xs -> App [a] (':->) * p (x : xs)
Actual type: Sing x -> Sing xs -> (p @@ xs) -> p @@ (x : xs)
• In the expression: listElimPoly @(:->) @a @p @l
In an equation for ‘listElimTyFun’:
listElimTyFun = listElimPoly @(:->) @a @p @l
• Relevant bindings include
listElimTyFun :: Sing l
-> (p @@ '[])
-> (forall (x :: a) (xs :: [a]).
Sing x -> Sing xs -> (p @@ xs) -> p @@ (x : xs))
-> p @@ l
(bound at T13877.hs:65:1)
T13877.hs:65:41: error:
• Expecting one more argument to ‘p’
Expected kind ‘(-?>) [a] * (':->)’, but ‘p’ has kind ‘[a] ~> *’
• In the type ‘p’
In the expression: listElimPoly @(:->) @a @p @l
In an equation for ‘listElimTyFun’:
listElimTyFun = listElimPoly @(:->) @a @p @l
• Relevant bindings include
listElimTyFun :: Sing l
-> (p @@ '[])
-> (forall (x :: a) (xs :: [a]).
Sing x -> Sing xs -> (p @@ xs) -> p @@ (x : xs))
-> p @@ l
(bound at T13877.hs:65:1)
......@@ -135,4 +135,5 @@ test('T7102a', normal, ghci_script, ['T7102a.script'])
test('T13271', normal, compile_fail, [''])
test('T13674', normal, compile_fail, [''])
test('T13784', normal, compile_fail, [''])
test('T13877', normal, compile_fail, [''])
test('T14033', 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