Commit 1f49b829 authored by Simon Peyton Jones's avatar Simon Peyton Jones

Test Trac #7224 and #7230

parent 00922ef9
{-# LANGUAGE PolyKinds #-}
module T7224 where
class PMonad' (m :: i -> i -> * -> *) where
ret' :: a -> m i i a
bind' :: m i j a -> (a -> m j k b) -> m i k b
T7224.hs:6:19:
Kind variable `i' used as a type
In the type `a -> m i i a'
In the class declaration for PMonad'
{-# OPTIONS_GHC -fwarn-incomplete-patterns #-}
{-# LANGUAGE DataKinds, PolyKinds, GADTs, TypeFamilies #-}
{-# LANGUAGE TypeOperators, UndecidableInstances #-}
module T7230 where
data Nat = Zero | Succ Nat deriving (Show, Eq, Ord)
data family Sing (x :: k)
data instance Sing (n :: Nat) where
SZero :: Sing Zero
SSucc :: Sing n -> Sing (Succ n)
type SNat (n :: Nat) = Sing n
data instance Sing (b :: Bool) where
STrue :: Sing True
SFalse :: Sing False
type SBool (b :: Bool) = Sing b
data instance Sing (xs :: [k]) where
SNil :: Sing ('[] :: [k])
SCons :: Sing x -> Sing xs -> Sing (x ': xs)
type SList (xs :: [k]) = Sing (xs :: [k])
type family (:<<=) (n :: Nat) (m :: Nat) :: Bool
type instance Zero :<<= n = True
type instance Succ n :<<= Zero = False
type instance Succ n :<<= Succ m = n :<<= m
(%:<<=) :: SNat n -> SNat m -> SBool (n :<<= m)
SZero %:<<= _ = STrue
SSucc _ %:<<= SZero = SFalse
SSucc n %:<<= SSucc m = n %:<<= m
type family (b :: Bool) :&& (b' :: Bool) :: Bool
type instance True :&& b = b
type instance False :&& b = False
type family Increasing (xs :: [Nat]) :: Bool
type instance Increasing '[] = True
type instance Increasing '[n] = True
type instance Increasing (n ': m ': ns) = n :<<= m :&& Increasing (m ': ns)
crash :: (Increasing xs) ~ True => SList xs -> SBool (Increasing xs)
crash (SCons x (SCons y xs)) = x %:<<= y
crash _ = STrue
T7230.hs:48:32:
Could not deduce ((x :<<= x1) ~ 'True)
from the context (Increasing xs ~ 'True)
bound by the type signature for
crash :: Increasing xs ~ 'True =>
SList Nat xs -> SBool (Increasing xs)
at T7230.hs:47:10-68
or from (xs ~ (':) Nat x xs1)
bound by a pattern with constructor
SCons :: forall (k :: BOX) (x :: k) (xs :: [k]).
Sing k x -> Sing [k] xs -> Sing [k] ((':) k x xs),
in an equation for `crash'
at T7230.hs:48:8-27
or from (xs1 ~ (':) Nat x1 xs2)
bound by a pattern with constructor
SCons :: forall (k :: BOX) (x :: k) (xs :: [k]).
Sing k x -> Sing [k] xs -> Sing [k] ((':) k x xs),
in an equation for `crash'
at T7230.hs:48:17-26
Expected type: SBool (Increasing xs)
Actual type: SBool (x :<<= x1)
In the expression: x %:<<= y
In an equation for `crash':
crash (SCons x (SCons y xs)) = x %:<<= y
......@@ -63,6 +63,8 @@ test('T7128', normal, compile,[''])
test('T7151', normal, compile_fail,[''])
test('T7095', normal, compile,[''])
test('T7090', normal, compile,[''])
test('T7176', expect_broken(7176), compile,[''])
test('T7176', normal, compile,[''])
test('T7224', normal, compile_fail,[''])
test('T7230', 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