Commit 5479ae0a authored by Simon Peyton Jones's avatar Simon Peyton Jones

Testsuite error message changes

parent 66658eed
......@@ -2,7 +2,7 @@
==================== Tidy Core ====================
Result size of Tidy Core = {terms: 8, types: 19, coercions: 1}
T2431.$WRefl [InlPrag=INLINE] :: forall a. a T2431.:~: a
T2431.$WRefl [InlPrag=INLINE] :: forall a. a :~: a
[GblId[DataConWrapper],
Caf=NoCafRefs,
Str=DmdType,
......@@ -12,12 +12,9 @@ T2431.$WRefl [InlPrag=INLINE] :: forall a. a T2431.:~: a
Tmpl= \ (@ a) -> T2431.Refl @ a @ a @~ <a>_N}]
T2431.$WRefl = \ (@ a) -> T2431.Refl @ a @ a @~ <a>_N
T2431.absurd
:: forall a. GHC.Types.Int T2431.:~: GHC.Types.Bool -> a
absurd :: forall a. Int :~: Bool -> a
[GblId, Arity=1, Caf=NoCafRefs, Str=DmdType <L,U>b]
T2431.absurd =
\ (@ a) (x :: GHC.Types.Int T2431.:~: GHC.Types.Bool) ->
case x of _ [Occ=Dead] { }
absurd = \ (@ a) (x :: Int :~: Bool) -> case x of _ [Occ=Dead] { }
......@@ -2,7 +2,7 @@
[2 of 2] Compiling T9071 ( T9071.hs, T9071.o )
T9071.hs:7:37:
No instance for (Functor K)
No instance for (Functor Mu)
arising from the first field of ‘F’ (type ‘Mu (K a)’)
Possible fix:
use a standalone 'deriving instance' declaration,
......
T9071_2.hs:7:40:
No instance for (Functor Mu)
No instance for (Functor K1)
arising from the first field of ‘F1’ (type ‘Mu (K1 a)’)
Possible fix:
use a standalone 'deriving instance' declaration,
......
T3169.hs:13:22:
Could not deduce (elt ~ Map b elt)
from the context (Key a, Key b)
bound by the instance declaration at T3169.hs:10:10-36
Couldn't match type ‘elt’ with ‘Map b elt’
‘elt’ is a rigid type variable bound by
the type signature for
lookup :: (a, b) -> Map (a, b) elt -> Maybe elt
......
T7293.hs:24:5:
Couldn't match type ‘'False’ with ‘'True’
Couldn't match type ‘'True’ with ‘'False’
Inaccessible code in
a pattern with constructor
Nil :: forall a. Vec a 'Zero,
......
T7294.hs:25:5: Warning:
Couldn't match type ‘'False’ with ‘'True’
Couldn't match type ‘'True’ with ‘'False’
Inaccessible code in
a pattern with constructor
Nil :: forall a. Vec a 'Zero,
......
gadt21.hs:21:60:
Could not deduce (Ord a1) arising from a use of ‘f’
from the context (a ~ Set a1)
bound by a pattern with constructor
TypeSet :: forall a. Type a -> Type (Set a),
in an equation for ‘withOrdDynExpr’
at gadt21.hs:21:35-43
Possible fix:
add (Ord a1) to the context of
the data constructor ‘TypeSet’
or the data constructor ‘DynExpr’
or the type signature for
withOrdDynExpr :: DynExpr
-> (forall a. Ord a => Expr a -> b) -> Maybe b
In the first argument of ‘Just’, namely ‘(f e)’
In the expression: Just (f e)
In an equation for ‘withOrdDynExpr’:
withOrdDynExpr (DynExpr e@(Const (TypeSet _) _)) f = Just (f e)
gadt21.hs:21:60:
Could not deduce (Ord a1) arising from a use of ‘f’
from the context (a ~ Set a1)
bound by a pattern with constructor
TypeSet :: forall a. Type a -> Type (Set a),
in an equation for ‘withOrdDynExpr’
at gadt21.hs:21:35-43
Possible fix:
add (Ord a1) to the context of the data constructor ‘TypeSet’
In the first argument of ‘Just’, namely ‘(f e)’
In the expression: Just (f e)
In an equation for ‘withOrdDynExpr’:
withOrdDynExpr (DynExpr e@(Const (TypeSet _) _)) f = Just (f e)
......@@ -3,14 +3,14 @@ B.hs:4:1: Warning:
Top-level binding with no type signature:
answer_to_live_the_universe_and_everything :: Int
B.hs:5:13: Warning:
B.hs:5:12: Warning:
Defaulting the following constraint(s) to type ‘Integer’
(Num a0) arising from the literal ‘1’ at B.hs:5:13
(Enum a0)
arising from the arithmetic sequence ‘1 .. 23 * 2’ at B.hs:5:12-20
In the expression: 1
(Num a0) arising from the literal ‘1’ at B.hs:5:13
In the first argument of ‘length’, namely ‘[1 .. 23 * 2]’
In the first argument of ‘(-)’, namely ‘length [1 .. 23 * 2]’
In the expression: length [1 .. 23 * 2] - 4
A.hs:7:1: Warning:
Top-level binding with no type signature: main :: IO ()
......@@ -19,14 +19,14 @@ B.hs:4:1: Warning:
Top-level binding with no type signature:
answer_to_live_the_universe_and_everything :: Int
B.hs:5:13: Warning:
B.hs:5:12: Warning:
Defaulting the following constraint(s) to type ‘Integer’
(Num a0) arising from the literal ‘1’ at B.hs:5:13
(Enum a0)
arising from the arithmetic sequence ‘1 .. 23 * 2’ at B.hs:5:12-20
In the expression: 1
(Num a0) arising from the literal ‘1’ at B.hs:5:13
In the first argument of ‘length’, namely ‘[1 .. 23 * 2]’
In the first argument of ‘(-)’, namely ‘length [1 .. 23 * 2]’
In the expression: length [1 .. 23 * 2] - 4
A.hs:7:1: Warning:
Top-level binding with no type signature: main :: IO ()
Stopped at break026.hs:(5,1)-(7,35)
_result :: t = _
Stopped at break026.hs:5:16-22
_result :: Integer = _
c :: Integer = 0
go :: Integer -> [t1] -> Integer = _
xs :: [t1] = _
Stopped at break026.hs:(6,9)-(7,35)
_result :: t = _
f :: t -> t1 -> t = _
Stopped at break026.hs:7:23-35
_result :: Integer = _
c :: Integer = 0
f :: Integer -> Integer -> Integer = _
x :: Integer = 1
xs :: [Integer] = _
Stopped at break026.hs:(6,9)-(7,35)
_result :: t = _
f :: t -> t1 -> t = _
Stopped at break026.hs:7:23-35
_result :: t = _
c :: t = _
f :: t -> Integer -> t = _
x :: Integer = 2
xs :: [Integer] = _
c = 1
Stopped at break026.hs:(5,1)-(7,35)
_result :: t = _
Stopped at break026.hs:5:16-22
_result :: Integer = _
c :: Integer = 0
go :: Integer -> [t1] -> Integer = _
xs :: [t1] = _
Stopped at break026.hs:(6,9)-(7,35)
_result :: t = _
f :: t -> t1 -> t = _
Stopped at break026.hs:7:23-35
_result :: Integer = _
c :: Integer = 0
f :: Integer -> Integer -> Integer = _
x :: Integer = 1
xs :: [Integer] = _
Stopped at break026.hs:(6,9)-(7,35)
_result :: t = _
f :: t -> t1 -> t = _
Stopped at break026.hs:7:23-35
_result :: t = _
c :: t = _
f :: t -> Integer -> t = _
x :: Integer = 2
xs :: [Integer] = _
Stopped at break026.hs:7:27-31
_result :: Integer = _
c :: Integer = 0
f :: Integer -> Integer -> Integer = _
x :: Integer = 1
()
1
Stopped at break026.hs:(5,1)-(7,35)
_result :: t1 = _
Stopped at break026.hs:5:16-22
_result :: Integer = _
c :: Integer = 0
go :: Integer -> [t] -> Integer = _
xs :: [t] = _
Stopped at break026.hs:(6,9)-(7,35)
_result :: t1 = _
f :: t1 -> t -> t1 = _
Stopped at break026.hs:7:23-35
_result :: Integer = _
c :: Integer = 0
f :: Integer -> Integer -> Integer = _
x :: Integer = 1
xs :: [Integer] = _
Stopped at break026.hs:(6,9)-(7,35)
_result :: t1 = _
f :: t1 -> t -> t1 = _
Stopped at break026.hs:7:23-35
_result :: t1 = _
c :: t1 = _
f :: t1 -> Integer -> t1 = _
x :: Integer = 2
xs :: [Integer] = _
c = 1
Stopped at break026.hs:(5,1)-(7,35)
_result :: t1 = _
Stopped at break026.hs:5:16-22
_result :: Integer = _
c :: Integer = 0
go :: Integer -> [t] -> Integer = _
xs :: [t] = _
Stopped at break026.hs:(6,9)-(7,35)
_result :: t1 = _
f :: t1 -> t -> t1 = _
Stopped at break026.hs:7:23-35
_result :: Integer = _
c :: Integer = 0
f :: Integer -> Integer -> Integer = _
x :: Integer = 1
xs :: [Integer] = _
Stopped at break026.hs:(6,9)-(7,35)
_result :: t1 = _
f :: t1 -> t -> t1 = _
Stopped at break026.hs:7:23-35
_result :: t1 = _
c :: t1 = _
f :: t1 -> Integer -> t1 = _
x :: Integer = 2
xs :: [Integer] = _
Stopped at break026.hs:7:27-31
_result :: Integer = _
c :: Integer = 0
f :: Integer -> Integer -> Integer = _
x :: Integer = 1
()
1
......@@ -41,6 +41,14 @@ class Mergeable a b where
type MergerType a b
merger :: a -> b -> MergerType a b
{-
merge ::
forall a b.
(Merger (MergerType a b), Mergeable a b,
UnmergedLeft (MergerType a b) ~ a,
UnmergedRight (MergerType a b) ~ b) =>
a -> b -> Merged (MergerType a b)
-}
merge x y = mkMerge (merger x y) x y
data TakeRight a
......@@ -117,4 +125,4 @@ instance
type Merged (RightHeadFirst h1 t1 h2 t2) = h2 :* Merged (MergerType (h1 :* t1) t2)
type UnmergedLeft (RightHeadFirst h1 t1 h2 t2) = h1 :* t1
type UnmergedRight (RightHeadFirst h1 t1 h2 t2) = h2 :* t2
mkMerge _ (h1 :* t1) (h2 :* t2) = h2 :* mkMerge (merger (h1 :* t1) t2) (h1 :* t1) t2
\ No newline at end of file
mkMerge _ (h1 :* t1) (h2 :* t2) = h2 :* mkMerge (merger (h1 :* t1) t2) (h1 :* t1) t2
......@@ -8,7 +8,7 @@ type family F a
bar y = let foo :: (F Int ~ [a]) => a -> Int
foo x = length [x,y]
in (y,foo y)
in (y,foo y)
-- This example demonstrates why we need to push in
......@@ -20,5 +20,12 @@ bar y = let foo :: (F Int ~ [a]) => a -> Int
-- Given/Solved, it will be discarded when we meet the given (F Int ~ [a]) and
-- we will not be able to solve the implication constraint.
-- Oct 14: actually this example is _really_ strange, and doesn't illustrate
-- the real issue in Trac #4935, for which there is a separate test
--
-- The example here requires us to infer a type
-- bar :: F Int ~ [a] => ...
-- which is a strange type to quantify over; better to complain about
-- having no instance for F Int.
PushedInAsGivens.hs:10:31:
Couldn't match expected type ‘a1’ with actual type ‘a’
because type variable ‘a1’ would escape its scope
This (rigid, skolem) type variable is bound by
the type signature for foo :: (F Int ~ [a1]) => a1 -> Int
at PushedInAsGivens.hs:9:20-44
Relevant bindings include
x :: a1 (bound at PushedInAsGivens.hs:10:17)
foo :: a1 -> Int (bound at PushedInAsGivens.hs:10:13)
y :: a (bound at PushedInAsGivens.hs:9:5)
bar :: a -> (a, Int) (bound at PushedInAsGivens.hs:9:1)
In the expression: y
In the first argument of ‘length’, namely ‘[x, y]’
PushedInAsGivens.hs:11:15:
Couldn't match expected type ‘[a]’ with actual type ‘F Int’
Relevant bindings include
y :: a (bound at PushedInAsGivens.hs:9:5)
bar :: a -> (a, Int) (bound at PushedInAsGivens.hs:9:1)
In the expression: foo y
In the expression: (y, foo y)
In the expression:
let
foo :: (F Int ~ [a]) => a -> Int
foo x = length [...]
in (y, foo y)
......@@ -16,3 +16,33 @@ mkf p = undefined
foo :: a ~ [F a] => a -> a
foo p = same p (mkf p)
{- p :: a
[G] g : a ~ [F a]
[W] w : a ~ [F a]
--->
g' = g;[x] g'=aq4
[G] g' : a ~ [fsk] g=aqW
[W] x : F a ~ fsk x=aq3
[W] w : a ~ [F a]
--> subst a
x = F g' ; x2
[W] x2 : F fsk ~ fsk x2=aq5
--> (subst a)
w = g' ; w2
[W] w2 : [fsk] ~ [F a]
--> decompose
w2 = [w3]
[W] w3 : fsk ~ F a
cycle is
aq3 = Sym (F aq4) ; aq5 x = Sym (F g') ; x2
aq4 = apw ; aq3 g' =
-}
......@@ -8,7 +8,7 @@ type family F a
-- works if one of the duplicates is removed.
type instance F () = ()
type instance F () = ()
-- type instance F () = ()
foo :: F () -> ()
foo x = x
......
TYPE SIGNATURES
emptyL :: forall a. ListColl a
test2 ::
forall c t t1. (Coll c, Num t1, Num t, Elem c ~ (t, t1)) => c -> c
forall c t t1. (Num t, Num t1, Coll c, Elem c ~ (t, t1)) => c -> c
TYPE CONSTRUCTORS
class Coll c where
type family Elem c :: * open
......
T3208b.hs:15:10:
Could not deduce (STerm o0 ~ STerm a)
Could not deduce (STerm o0 ~ OTerm o0)
from the context (OTerm a ~ STerm a, OBJECT a, SUBST a)
bound by the type signature for
fce' :: (OTerm a ~ STerm a, OBJECT a, SUBST a) => a -> c
at T3208b.hs:14:9-56
NB: ‘STerm’ is a type function, and may not be injective
The type variable ‘o0’ is ambiguous
Expected type: STerm o0
Actual type: OTerm o0
Relevant bindings include
f :: a (bound at T3208b.hs:15:6)
fce' :: a -> c (bound at T3208b.hs:15:1)
In the expression: fce (apply f)
In an equation for ‘fce'’: fce' f = fce (apply f)
T3208b.hs:15:15:
Could not deduce (OTerm o0 ~ STerm a)
Could not deduce (OTerm o0 ~ OTerm a)
from the context (OTerm a ~ STerm a, OBJECT a, SUBST a)
bound by the type signature for
fce' :: (OTerm a ~ STerm a, OBJECT a, SUBST a) => a -> c
at T3208b.hs:14:9-56
NB: ‘OTerm’ is a type function, and may not be injective
The type variable ‘o0’ is ambiguous
Expected type: STerm a
Actual type: OTerm o0
Relevant bindings include
f :: a (bound at T3208b.hs:15:6)
fce' :: a -> c (bound at T3208b.hs:15:1)
......
......@@ -6,10 +6,56 @@ class C a where
type E a
c :: E a -> a -> a
data T a = T a
data T a = MkT a
-- MkT :: a -> T a
instance C (T a) where
type E (T a) = a
c x (T _) = T x
instance C (T b) where
type E (T b) = b
c x (MkT _) = MkT x
f t@(MkT x) = c x t
{- c :: E alpha -> alpha -> alpha
t :: T beta
x :: beta
f :: T beta -> gamma
[W] C alpha
[W] E alpha ~ beta
[W] alpha ~ T beta
[W] gamma ~ alpha
---> beta = t_aqf alpha = t_aqg
alpha := T beta
gamma := alpha
[W] E (T beta) ~ beta
-->
[W] ufsk ~ beta
[W] E (T beta) ~ ufsk
--> (swap and subst)
beta := ufsk
[W] x : E (T ufsk) ~ ufsk (do not rewrite RHS)
take a step ax: E (T beta) ~ beta
-->
[W] ufsk
--------------------------
But what about this?
--------------------------
axiom F [a] = F [a]
x : F [a] ~ fsk
step
ax : F [a] ~ F [a]
flatten
ax ; x : F [a] ~ fsk
x = ax ; x Oh dear!
-}
f t@(T x) = c x t
......@@ -10,3 +10,23 @@ bar = error "urk"
call :: F Bool -> Int
call x = bar (\_ -> x) (undefined :: H (F Bool))
{-
[W] H (F Bool) ~ H alpha
[W] alpha ~ F Bool
-->
F Bool ~ fuv0
H fuv0 ~ fuv1
H alpha ~ fuv2
fuv1 ~ fuv2
alpha ~ fuv0
flatten
~~~~~~~
fuv0 := alpha
fuv1 := fuv2
alpha := F Bool
-}
......@@ -8,3 +8,15 @@ data Proxy a = P
sDFMap :: (forall a. Proxy f -> Proxy a -> Proxy (F f a)) -> Int
sDFMap _ = 3
{-
flat cache
[G] F f_aqh aqj ~ fsk_aqp
[G] F f_aqg aqj ~ fsk_aqq
[W] aqk : f_aqh[2] ~ f_aqg
[w] aql : fsk_aqp ~ fsk_aqq
[G] F f_agh a_aqj ~ F f_aqg
-}
\ No newline at end of file
......@@ -170,7 +170,7 @@ test('T4981-V2', normal, compile, [''])
test('T4981-V3', normal, compile, [''])
test('T5002', normal, compile, [''])
test('PushedInAsGivens', normal, compile, [''])
test('PushedInAsGivens', normal, compile_fail, [''])
# Superclass equalities
test('T4338', normal, compile, [''])
......
{-# LANGUAGE TypeFamilies, FunctionalDependencies, FlexibleContexts, GADTs, ScopedTypeVariables #-}
module ExtraTcsUntch where
module ExtraTcsUntch where
class C x y | x -> y where
class C x y | x -> y where
op :: x -> y -> ()
instance C [a] [a]
......@@ -13,22 +13,24 @@ type family F a :: *
h :: F Int -> ()
h = undefined
data TEx where
TEx :: a -> TEx
data TEx where
TEx :: a -> TEx
f x =
f x =
let g1 :: forall b. b -> ()
g1 _ = h [x]
g2 z = case z of TEx y -> (h [[undefined]], op x [y])
in (g1 '3', g2 undefined)
{- This example comes from Note [Extra TcS Untouchables] in TcSimplify. It demonstrates
{- This example comes from Note [Extra TcS Untouchables] in TcSimplify. It demonstrates
why when floating equalities out of an implication constraint we must record the free
variables of the equalities as untouchables. With GHC 7.4.1 this program gives a Core
Lint error because of an existential escaping.
Lint error because of an existential escaping.
assuming x:beta
......@@ -39,16 +41,21 @@ f x =
{- Assume x:beta
From g1 we get (forall b. F Int ~ [beta])
From g2 we get (forall c. 0 => F Int ~ [[alpha]] /\ C beta [c])
Floating we get
F Int ~ [beta], F Int ~ [[alpha]], alpha ~ alpha', forall c. C beta [c]
= { alpha := alpha' }
= beta ~ [alpha'], F Int ~ [[alpha']], forall c. C beta [c]
= { beta := [alpha']
F Int ~ [[alpha']], forall c. C [alpha'] [c]
= F Int ~ [[alpha']], forall c. (C [alpha'] [c], alpha' ~ c)
From g1 we get [W] (forall b. F Int ~ [beta])
From g2 we get [W] (forall c. 0 => F Int ~ [[alpha]] /\ C beta [c])
(g2 is not generalised; the forall comes from the TEx pattern)
approximateWC then gives the candidate constraints to quantify
F Int ~ [beta], F Int ~ [[alpha']]
(alpha' is the promoted version of alpha)
Now decide inferred sig for f :: F Int ~ [beta] => beta -> blah
since beta is mentioned in tau-type for f but alpha' is not
Perhaps this is a stupid constraint to generalise over (we don't
generalise over (C Int).
-}
\ No newline at end of file
ExtraTcsUntch.hs:24:53:
Could not deduce (C [t] [a]) arising from a use of ‘op’
from the context (F Int ~ [[t]])
bound by the inferred type of
f :: (F Int ~ [[t]]) => [t] -> ((), ((), ()))
at ExtraTcsUntch.hs:(21,1)-(25,29)
In the expression: op x [y]
ExtraTcsUntch.hs:23:18:
Couldn't match expected type ‘F Int’ with actual type ‘[t]’
Relevant bindings include
x :: t (bound at ExtraTcsUntch.hs:21:3)
f :: t -> ((), ((), ())) (bound at ExtraTcsUntch.hs:21:1)
In the first argument of ‘h’, namely ‘[x]’
In the expression: h [x]
In an equation for ‘g1’: g1 _ = h [x]
ExtraTcsUntch.hs:25:38:
Couldn't match expected type ‘F Int’ with actual type ‘[[t0]]’
The type variable ‘t0’ is ambiguous
In the first argument of ‘h’, namely ‘[[undefined]]’
In the expression: h [[undefined]]
In the expression: (h [[undefined]], op x [y])
In a case alternative: TEx y -> (h [[undefined]], op x [y])
......@@ -5,8 +5,34 @@ module ShouldFail where
type family Const a
type instance Const a = ()
data T a where T :: a -> T (Const a)
data T a where T :: c -> T (Const c)
coerce :: forall a b . a -> b
coerce x = case T x :: T (Const b) of
T y -> y
T y -> y
{-
T :: forall a. forall c. (a ~ Const c) => c -> T a
a ~ gamma -- Instantiate T with a=alpha, c=gamma
alpha ~ Const b -- Result of (T x)
alpha ~ Const gamma -- Constraint from (T x)
y::c
forall c. (Const b ~ Const c) => c ~ b
==>
Const b ~ Const a
------------
case e of
T y -> y
e :: T alpha
Patterns
forall c. (alpha ~ Const c) => c ~ b
alpha ~ Const b
-}
\ No newline at end of file
GADTwrong1.hs:12:19:
Could not deduce (a1 ~ b)
from the context (() ~ Const a1)
bound by a pattern with constructor
T :: forall a. a -> T (Const a),
in a case alternative
at GADTwrong1.hs:12:12-14
‘a1’ is a rigid type variable bound by