Commit 1235ca95 authored by Simon Peyton Jones's avatar Simon Peyton Jones

Test Trac #15943

This test seems to work in HEAD
parent e08d34bb
{-# Language RankNTypes #-}
{-# Language DataKinds #-}
{-# Language KindSignatures #-}
{-# Language PolyKinds #-}
{-# Language TypeFamilyDependencies #-}
{-# Language GADTs #-}
{-# Language TypeSynonymInstances #-}
{-# Language FlexibleInstances #-}
{-# Language QuantifiedConstraints #-}
module T15943 where
import Data.Type.Equality
import Data.Coerce
import Data.Type.Coercion
import Data.Kind
newtype WrapFalse a b = WrapFalse (Hom False a b)
newtype WrapTrue a b = WrapTrue (Hom True a b)
class
(forall (x :: ob) (y :: ob). Coercible (WrapFalse x y) (WrapTrue y x))
=>
Ríki ob where
type Hom (or::Bool) = (res :: ob -> ob -> Type) | res -> or
instance Ríki Type where
type Hom False = (->)
type Hom True = Op
newtype Op :: Type -> Type -> Type where
Op :: (b -> a) -> Op a b
......@@ -294,6 +294,7 @@ test('T15322a', normal, compile_fail, [''])
test('T15142', normal, compile, [''])
test('T15352', normal, compile, [''])
test('T15664', normal, compile, [''])
test('T15943', normal, compile, [''])
test('T15704', normal, compile, [''])
test('T15711', normal, compile, ['-ddump-types'])
test('T15852', normal, compile, ['-ddump-types'])
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