diff options
Diffstat (limited to 'testsuite/tests')
15 files changed, 100 insertions, 56 deletions
diff --git a/testsuite/tests/deriving/should_fail/T7148.stderr b/testsuite/tests/deriving/should_fail/T7148.stderr index f8e5055b12..ee42cc91f1 100644 --- a/testsuite/tests/deriving/should_fail/T7148.stderr +++ b/testsuite/tests/deriving/should_fail/T7148.stderr @@ -1,18 +1,14 @@ T7148.hs:27:40: error: - • Couldn't match type ‘b’ with ‘Tagged a b’ + • Occurs check: cannot construct the infinite type: b ~ Tagged a b arising from the coercion of the method ‘iso2’ from type ‘forall b1. SameType b1 () -> SameType b1 b’ to type ‘forall b1. SameType b1 () -> SameType b1 (Tagged a b)’ - ‘b’ is a rigid type variable bound by - the deriving clause for ‘IsoUnit (Tagged a b)’ at T7148.hs:27:40-46 • When deriving the instance for (IsoUnit (Tagged a b)) T7148.hs:27:40: error: - • Couldn't match type ‘b’ with ‘Tagged a b’ + • Occurs check: cannot construct the infinite type: b ~ Tagged a b arising from the coercion of the method ‘iso1’ from type ‘forall b1. SameType () b1 -> SameType b b1’ to type ‘forall b1. SameType () b1 -> SameType (Tagged a b) b1’ - ‘b’ is a rigid type variable bound by - the deriving clause for ‘IsoUnit (Tagged a b)’ at T7148.hs:27:40-46 • When deriving the instance for (IsoUnit (Tagged a b)) diff --git a/testsuite/tests/gadt/T3169.stderr b/testsuite/tests/gadt/T3169.stderr index 4bc39a731b..d0f650b9ab 100644 --- a/testsuite/tests/gadt/T3169.stderr +++ b/testsuite/tests/gadt/T3169.stderr @@ -1,10 +1,6 @@ T3169.hs:13:22: error: - • Couldn't match type ‘elt’ with ‘Map b elt’ - ‘elt’ is a rigid type variable bound by - the type signature for: - lookup :: forall elt. (a, b) -> Map (a, b) elt -> Maybe elt - at T3169.hs:12:3-8 + • Occurs check: cannot construct the infinite type: elt ~ Map b elt Expected type: Map a (Map b elt) Actual type: Map (a, b) elt • In the second argument of ‘lookup’, namely ‘m’ diff --git a/testsuite/tests/gadt/T7558.stderr b/testsuite/tests/gadt/T7558.stderr index ff90037ff6..568f64fcee 100644 --- a/testsuite/tests/gadt/T7558.stderr +++ b/testsuite/tests/gadt/T7558.stderr @@ -1,10 +1,6 @@ T7558.hs:8:4: error: - • Couldn't match type ‘a’ with ‘Maybe a’ - ‘a’ is a rigid type variable bound by - the type signature for: - f :: forall a. T a a -> Bool - at T7558.hs:7:1-18 + • Occurs check: cannot construct the infinite type: a ~ Maybe a Inaccessible code in a pattern with constructor: MkT :: forall a b. a ~ Maybe b => a -> Maybe b -> T a b, diff --git a/testsuite/tests/indexed-types/should_fail/T13674.hs b/testsuite/tests/indexed-types/should_fail/T13674.hs new file mode 100644 index 0000000000..4d9a81d8a5 --- /dev/null +++ b/testsuite/tests/indexed-types/should_fail/T13674.hs @@ -0,0 +1,56 @@ +{-# LANGUAGE ConstraintKinds #-} +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE PolyKinds #-} +{-# LANGUAGE RankNTypes #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE TypeApplications #-} +{-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE TypeOperators #-} + +module T13674 where + +import Data.Proxy +import GHC.Exts (Constraint) +import GHC.TypeLits +import Unsafe.Coerce (unsafeCoerce) + +data Dict :: Constraint -> * where + Dict :: a => Dict a + +infixr 9 :- +newtype a :- b = Sub (a => Dict b) + +-- | Given that @a :- b@, derive something that needs a context @b@, using the context @a@ +(\\) :: a => (b => r) -> (a :- b) -> r +r \\ Sub Dict = r + +newtype Magic n = Magic (KnownNat n => Dict (KnownNat n)) + +magic :: forall n m o. (Integer -> Integer -> Integer) -> (KnownNat n, KnownNat m) :- KnownNat o +magic f = Sub $ unsafeCoerce (Magic Dict) (natVal (Proxy :: Proxy n) `f` natVal (Proxy :: Proxy m)) + +type family Lcm :: Nat -> Nat -> Nat where + +axiom :: forall a b. Dict (a ~ b) +axiom = unsafeCoerce (Dict :: Dict (a ~ a)) + +lcmNat :: forall n m. (KnownNat n, KnownNat m) :- KnownNat (Lcm n m) +lcmNat = magic lcm + +lcmIsIdempotent :: forall n. Dict (n ~ Lcm n n) +lcmIsIdempotent = axiom + +newtype GF (n :: Nat) = GF Integer + +x :: GF 5 +x = GF 3 + +y :: GF 5 +y = GF 4 + +foo :: (KnownNat m, KnownNat n) => GF m -> GF n -> GF (Lcm m n) +foo m@(GF x) n@(GF y) = GF $ (x*y) `mod` (lcm (natVal m) (natVal n)) + +bar :: (KnownNat m) => GF m -> GF m -> GF m +bar (x :: GF m) y = foo x y - foo y x \\ lcmNat @m @m \\ Sub @() (lcmIsIdempotent @m) diff --git a/testsuite/tests/indexed-types/should_fail/T13674.stderr b/testsuite/tests/indexed-types/should_fail/T13674.stderr new file mode 100644 index 0000000000..53a7cb705c --- /dev/null +++ b/testsuite/tests/indexed-types/should_fail/T13674.stderr @@ -0,0 +1,28 @@ + +T13674.hs:56:21: error: + • Occurs check: cannot construct the infinite type: m ~ Lcm m m + Expected type: GF m + Actual type: GF (Lcm m m) + • In the first argument of ‘(-)’, namely ‘foo x y’ + In the expression: + foo x y - foo y x \\ lcmNat @m @m \\ Sub @() (lcmIsIdempotent @m) + In an equation for ‘bar’: + bar (x :: GF m) y + = foo x y - foo y x \\ lcmNat @m @m \\ Sub @() (lcmIsIdempotent @m) + • Relevant bindings include + y :: GF m (bound at T13674.hs:56:17) + x :: GF m (bound at T13674.hs:56:6) + bar :: GF m -> GF m -> GF m (bound at T13674.hs:56:1) + +T13674.hs:56:31: error: + • Occurs check: cannot construct the infinite type: m ~ Lcm m m + Expected type: GF m + Actual type: GF (Lcm m m) + • In the first argument of ‘(\\)’, namely ‘foo y x’ + In the first argument of ‘(\\)’, namely ‘foo y x \\ lcmNat @m @m’ + In the second argument of ‘(-)’, namely + ‘foo y x \\ lcmNat @m @m \\ Sub @() (lcmIsIdempotent @m)’ + • Relevant bindings include + y :: GF m (bound at T13674.hs:56:17) + x :: GF m (bound at T13674.hs:56:6) + bar :: GF m -> GF m -> GF m (bound at T13674.hs:56:1) diff --git a/testsuite/tests/indexed-types/should_fail/T4272.stderr b/testsuite/tests/indexed-types/should_fail/T4272.stderr index f60711a758..f0c5ab57f0 100644 --- a/testsuite/tests/indexed-types/should_fail/T4272.stderr +++ b/testsuite/tests/indexed-types/should_fail/T4272.stderr @@ -1,10 +1,7 @@ T4272.hs:15:26: error: - • Couldn't match type ‘a’ with ‘TermFamily a a’ - ‘a’ is a rigid type variable bound by - the type signature for: - laws :: forall a b. TermLike a => TermFamily a a -> b - at T4272.hs:14:1-53 + • Occurs check: cannot construct the infinite type: + a ~ TermFamily a a Expected type: TermFamily a (TermFamily a a) Actual type: TermFamily a a • In the first argument of ‘terms’, namely diff --git a/testsuite/tests/indexed-types/should_fail/T9662.stderr b/testsuite/tests/indexed-types/should_fail/T9662.stderr index 3cdc60a18c..54b05665a3 100644 --- a/testsuite/tests/indexed-types/should_fail/T9662.stderr +++ b/testsuite/tests/indexed-types/should_fail/T9662.stderr @@ -1,7 +1,7 @@ T9662.hs:47:8: error: - • Couldn't match type ‘m’ with ‘Int’ - ‘m’ is a rigid type variable bound by + • Couldn't match type ‘k’ with ‘Int’ + ‘k’ is a rigid type variable bound by the type signature for: test :: forall sh k m n. Shape (((sh :. k) :. m) :. n) -> Shape (((sh :. m) :. n) :. k) diff --git a/testsuite/tests/indexed-types/should_fail/all.T b/testsuite/tests/indexed-types/should_fail/all.T index 9cad8e1734..24abd30cf0 100644 --- a/testsuite/tests/indexed-types/should_fail/all.T +++ b/testsuite/tests/indexed-types/should_fail/all.T @@ -133,3 +133,4 @@ test('T12867', normal, compile_fail, ['']) test('T7102', [ expect_broken(7102) ], ghci_script, ['T7102.script']) test('T7102a', normal, ghci_script, ['T7102a.script']) test('T13271', normal, compile_fail, ['']) +test('T13674', normal, compile_fail, ['']) diff --git a/testsuite/tests/typecheck/should_compile/FD3.stderr b/testsuite/tests/typecheck/should_compile/FD3.stderr index d7ac728b6c..85728da0a6 100644 --- a/testsuite/tests/typecheck/should_compile/FD3.stderr +++ b/testsuite/tests/typecheck/should_compile/FD3.stderr @@ -1,13 +1,9 @@ FD3.hs:15:15: error: - • Couldn't match type ‘a’ with ‘(String, a)’ + • Occurs check: cannot construct the infinite type: a ~ (String, a) arising from a functional dependency between: constraint ‘MkA (String, a) a’ arising from a use of ‘mkA’ instance ‘MkA a1 a1’ at FD3.hs:12:10-16 - ‘a’ is a rigid type variable bound by - the type signature for: - translate :: forall a. (String, a) -> A a - at FD3.hs:14:1-31 • In the expression: mkA a In an equation for ‘translate’: translate a = mkA a • Relevant bindings include diff --git a/testsuite/tests/typecheck/should_compile/T9834.stderr b/testsuite/tests/typecheck/should_compile/T9834.stderr index 303b1defe6..01b003fa3a 100644 --- a/testsuite/tests/typecheck/should_compile/T9834.stderr +++ b/testsuite/tests/typecheck/should_compile/T9834.stderr @@ -1,8 +1,6 @@ T9834.hs:23:10: warning: [-Wdeferred-type-errors (in -Wdefault)] - • Couldn't match type ‘p’ with ‘(->) (p a0)’ - ‘p’ is a rigid type variable bound by - the class declaration for ‘ApplicativeFix’ at T9834.hs:21:39 + • Occurs check: cannot construct the infinite type: p ~ (->) (p a0) Expected type: (forall (q :: * -> *). Applicative q => Comp p q a -> Comp p q a) diff --git a/testsuite/tests/typecheck/should_fail/mc19.stderr b/testsuite/tests/typecheck/should_fail/mc19.stderr index cffb7f61c5..1b9682e6c8 100644 --- a/testsuite/tests/typecheck/should_fail/mc19.stderr +++ b/testsuite/tests/typecheck/should_fail/mc19.stderr @@ -1,10 +1,6 @@ mc19.hs:10:31: error: - • Couldn't match type ‘a’ with ‘[a]’ - ‘a’ is a rigid type variable bound by - a type expected by the context: - forall a. [a] -> [a] - at mc19.hs:10:10-35 + • Occurs check: cannot construct the infinite type: a ~ [a] Expected type: [a] -> [a] Actual type: [a] -> [[a]] • In the expression: inits diff --git a/testsuite/tests/typecheck/should_fail/mc21.stderr b/testsuite/tests/typecheck/should_fail/mc21.stderr index 9cffcfb492..014628f94a 100644 --- a/testsuite/tests/typecheck/should_fail/mc21.stderr +++ b/testsuite/tests/typecheck/should_fail/mc21.stderr @@ -1,10 +1,6 @@ mc21.hs:12:26: error: - • Couldn't match type ‘a’ with ‘[a]’ - ‘a’ is a rigid type variable bound by - a type expected by the context: - forall a. [a] -> [[a]] - at mc21.hs:(11,9)-(12,31) + • Occurs check: cannot construct the infinite type: a ~ [a] Expected type: [a] -> [[a]] Actual type: [[a]] -> [[a]] • In the expression: take 5 diff --git a/testsuite/tests/typecheck/should_fail/mc22.stderr b/testsuite/tests/typecheck/should_fail/mc22.stderr index ec82baf620..40a754a9c5 100644 --- a/testsuite/tests/typecheck/should_fail/mc22.stderr +++ b/testsuite/tests/typecheck/should_fail/mc22.stderr @@ -1,10 +1,6 @@ mc22.hs:10:26: error: - • Couldn't match type ‘a’ with ‘t a’ - ‘a’ is a rigid type variable bound by - a type expected by the context: - forall a. [a] -> [t a] - at mc22.hs:(9,9)-(10,31) + • Occurs check: cannot construct the infinite type: a ~ t a Expected type: [a] -> [t a] Actual type: [t a] -> [t a] • In the expression: take 5 diff --git a/testsuite/tests/typecheck/should_fail/tcfail191.stderr b/testsuite/tests/typecheck/should_fail/tcfail191.stderr index 8eb11f9c62..125c2d8393 100644 --- a/testsuite/tests/typecheck/should_fail/tcfail191.stderr +++ b/testsuite/tests/typecheck/should_fail/tcfail191.stderr @@ -1,10 +1,6 @@ tcfail191.hs:11:26: error: - • Couldn't match type ‘a’ with ‘[a]’ - ‘a’ is a rigid type variable bound by - a type expected by the context: - forall a. [a] -> [[a]] - at tcfail191.hs:(10,9)-(11,31) + • Occurs check: cannot construct the infinite type: a ~ [a] Expected type: [a] -> [[a]] Actual type: [[a]] -> [[a]] • In the expression: take 5 diff --git a/testsuite/tests/typecheck/should_fail/tcfail193.stderr b/testsuite/tests/typecheck/should_fail/tcfail193.stderr index 6259dfc2a2..028e2f0232 100644 --- a/testsuite/tests/typecheck/should_fail/tcfail193.stderr +++ b/testsuite/tests/typecheck/should_fail/tcfail193.stderr @@ -1,10 +1,6 @@ tcfail193.hs:10:31: error: - • Couldn't match type ‘a’ with ‘[a]’ - ‘a’ is a rigid type variable bound by - a type expected by the context: - forall a. [a] -> [a] - at tcfail193.hs:10:10-35 + • Occurs check: cannot construct the infinite type: a ~ [a] Expected type: [a] -> [a] Actual type: [a] -> [[a]] • In the expression: inits |