Commit 8846a7fd authored by Ryan Scott's avatar Ryan Scott

Fix #14369 by making injectivity warnings finer-grained

Summary:
Previously, GHC would always raise the possibility that a
type family might not be injective in certain error messages, even if
that type family actually //was// injective. Fix this by actually
checking for a type family's lack of injectivity before emitting
such an error message.

Test Plan: ./validate

Reviewers: goldfire, austin, bgamari, simonpj

Reviewed By: simonpj

Subscribers: simonpj, rwbarton, thomie

GHC Trac Issues: #14369

Differential Revision: https://phabricator.haskell.org/D4106
parent 101a8c77
......@@ -1830,8 +1830,9 @@ mkEqInfoMsg ct ty1 ty2
tyfun_msg | Just tc1 <- mb_fun1
, Just tc2 <- mb_fun2
, tc1 == tc2
, not (isInjectiveTyCon tc1 Nominal)
= text "NB:" <+> quotes (ppr tc1)
<+> text "is a type function, and may not be injective"
<+> text "is a non-injective type family"
| otherwise = empty
isUserSkolem :: ReportErrCtxt -> TcTyVar -> Bool
......
......@@ -3,9 +3,8 @@ NoMatchErr.hs:19:7: error:
• Couldn't match type ‘Memo d0’ with ‘Memo d’
Expected type: Memo d a -> Memo d a
Actual type: Memo d0 a -> Memo d0 a
NB: ‘Memo’ is a type function, and may not be injective
NB: ‘Memo’ is a non-injective type family
The type variable ‘d0’ is ambiguous
• In the ambiguity check for ‘f’
To defer the ambiguity check to use sites, enable AllowAmbiguousTypes
In the type signature:
f :: (Fun d) => Memo d a -> Memo d a
In the type signature: f :: (Fun d) => Memo d a -> Memo d a
{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilyDependencies #-}
{-# LANGUAGE TypeInType #-}
{-# LANGUAGE TypeOperators #-}
module T14369 where
data family Sing (a :: k)
data instance Sing (z :: Maybe a) where
SNothing :: Sing Nothing
SJust :: Sing x -> Sing (Just x)
class SingKind k where
type Demote k = r | r -> k
fromSing :: Sing (a :: k) -> Demote k
instance SingKind a => SingKind (Maybe a) where
type Demote (Maybe a) = Maybe (Demote a)
fromSing SNothing = Nothing
fromSing (SJust x) = Just (fromSing x)
f :: forall (x :: forall a. Maybe a) a. SingKind a => Sing x -> Maybe (Demote a)
f = fromSing
T14369.hs:27:5: error:
• Couldn't match type ‘Demote a’ with ‘Demote a1’
Expected type: Sing (x a) -> Maybe (Demote a1)
Actual type: Sing (x a) -> Demote (Maybe a)
• In the expression: fromSing
In an equation for ‘f’: f = fromSing
• Relevant bindings include
f :: Sing (x a) -> Maybe (Demote a1) (bound at T14369.hs:27:1)
......@@ -3,7 +3,7 @@ T1897b.hs:16:1: error:
• Couldn't match type ‘Depend a’ with ‘Depend a0’
Expected type: t (Depend a) -> Bool
Actual type: t (Depend a0) -> Bool
NB: ‘Depend’ is a type function, and may not be injective
NB: ‘Depend’ is a non-injective type family
The type variable ‘a0’ is ambiguous
• In the ambiguity check for the inferred type for ‘isValid’
To defer the ambiguity check to use sites, enable AllowAmbiguousTypes
......
......@@ -3,7 +3,7 @@ T1900.hs:7:3: error:
• Couldn't match type ‘Depend s0’ with ‘Depend s’
Expected type: Depend s -> Depend s
Actual type: Depend s0 -> Depend s0
NB: ‘Depend’ is a type function, and may not be injective
NB: ‘Depend’ is a non-injective type family
The type variable ‘s0’ is ambiguous
• In the ambiguity check for ‘trans’
To defer the ambiguity check to use sites, enable AllowAmbiguousTypes
......
......@@ -3,7 +3,7 @@ T2544.hs:17:12: error:
• Couldn't match type ‘IxMap r’ with ‘IxMap i1’
Expected type: IxMap (l :|: r) [Int]
Actual type: BiApp (IxMap l) (IxMap i1) [Int]
NB: ‘IxMap’ is a type function, and may not be injective
NB: ‘IxMap’ is a non-injective type family
The type variable ‘i1’ is ambiguous
• In the expression: BiApp empty empty
In an equation for ‘empty’: empty = BiApp empty empty
......@@ -15,7 +15,7 @@ T2544.hs:17:18: error:
• Couldn't match type ‘IxMap i0’ with ‘IxMap l’
Expected type: IxMap l [Int]
Actual type: IxMap i0 [Int]
NB: ‘IxMap’ is a type function, and may not be injective
NB: ‘IxMap’ is a non-injective type family
The type variable ‘i0’ is ambiguous
• In the first argument of ‘BiApp’, namely ‘empty’
In the expression: BiApp empty empty
......
......@@ -9,7 +9,7 @@ T2664.hs:31:9: error:
at T2664.hs:23:5-12
Expected type: IO (PChan (a :*: b), PChan c)
Actual type: IO (PChan (a :*: b), PChan (Dual b :+: Dual a))
NB: ‘Dual’ is a type function, and may not be injective
NB: ‘Dual’ is a non-injective type family
• In a stmt of a 'do' block:
return
(O $ takeMVar v,
......
T4099.hs:11:30: error:
• Couldn't match expected type ‘T a0’ with actual type ‘T b’
NB: ‘T’ is a type function, and may not be injective
NB: ‘T’ is a non-injective type family
The type variable ‘a0’ is ambiguous
• In the second argument of ‘foo’, namely ‘x’
In the expression: foo (error "urk") x
......
......@@ -7,7 +7,7 @@ T4179.hs:26:16: error:
Actual type: x (A2 (FCon x) -> A3 (FCon x))
-> A2 (x (A2 (FCon x) -> A3 (FCon x)))
-> A3 (x (A2 (FCon x) -> A3 (FCon x)))
NB: ‘A2’ is a type function, and may not be injective
NB: ‘A2’ is a non-injective type family
• In the first argument of ‘foldDoC’, namely ‘op’
In the expression: foldDoC op
In an equation for ‘fCon’: fCon = foldDoC op
......
......@@ -3,7 +3,7 @@ T9036.hs:17:17: error:
• Couldn't match type ‘Curried t0 [t0]’ with ‘Curried t [t]’
Expected type: Maybe (GetMonad t after) -> Curried t [t]
Actual type: Maybe (GetMonad t0 after) -> Curried t0 [t0]
NB: ‘Curried’ is a type function, and may not be injective
NB: ‘Curried’ is a non-injective type family
The type variable ‘t0’ is ambiguous
• In the ambiguity check for ‘simpleLogger’
To defer the ambiguity check to use sites, enable AllowAmbiguousTypes
......
......@@ -2,7 +2,7 @@
T9171.hs:10:20: error:
• Couldn't match expected type ‘GetParam Base (GetParam Base Int)’
with actual type ‘GetParam Base (GetParam Base Int)’
NB: ‘GetParam’ is a type function, and may not be injective
NB: ‘GetParam’ is a non-injective type family
The type variable ‘k20’ is ambiguous
Use -fprint-explicit-kinds to see the kind arguments
• In the ambiguity check for an expression type signature
......
......@@ -140,3 +140,4 @@ test('T13972', normal, compile_fail, [''])
test('T14033', normal, compile_fail, [''])
test('T14045a', normal, compile_fail, [''])
test('T14175', normal, compile_fail, [''])
test('T14369', normal, compile_fail, [''])
......@@ -2,18 +2,12 @@
T5853.hs:15:46: error:
• Could not deduce: Subst (Subst fa a) b ~ Subst fa b
arising from a use of ‘<$>’
from the context: (F fa,
Elem fa ~ Elem fa,
Elem (Subst fa b) ~ b,
Subst fa b ~ Subst fa b,
Subst (Subst fa b) (Elem fa) ~ fa,
F (Subst fa a),
Elem (Subst fa a) ~ a,
Elem fa ~ Elem fa,
Subst (Subst fa a) (Elem fa) ~ fa,
Subst fa a ~ Subst fa a)
from the context: (F fa, Elem fa ~ Elem fa, Elem (Subst fa b) ~ b,
Subst fa b ~ Subst fa b, Subst (Subst fa b) (Elem fa) ~ fa,
F (Subst fa a), Elem (Subst fa a) ~ a, Elem fa ~ Elem fa,
Subst (Subst fa a) (Elem fa) ~ fa, Subst fa a ~ Subst fa a)
bound by the RULE "map/map" at T5853.hs:15:2-57
NB: ‘Subst’ is a type function, and may not be injective
NB: ‘Subst’ is a non-injective type family
• In the expression: (f . g) <$> xs
When checking the transformation rule "map/map"
• Relevant bindings include
......
T8030.hs:9:3: error:
• Couldn't match expected type ‘Pr a’ with actual type ‘Pr a0’
NB: ‘Pr’ is a type function, and may not be injective
NB: ‘Pr’ is a non-injective type family
The type variable ‘a0’ is ambiguous
• In the ambiguity check for ‘op1’
To defer the ambiguity check to use sites, enable AllowAmbiguousTypes
......@@ -13,7 +13,7 @@ T8030.hs:10:3: error:
• Couldn't match type ‘Pr a0’ with ‘Pr a’
Expected type: Pr a -> Pr a -> Pr a
Actual type: Pr a0 -> Pr a0 -> Pr a0
NB: ‘Pr’ is a type function, and may not be injective
NB: ‘Pr’ is a non-injective type family
The type variable ‘a0’ is ambiguous
• In the ambiguity check for ‘op2’
To defer the ambiguity check to use sites, enable AllowAmbiguousTypes
......
......@@ -3,7 +3,7 @@ T8034.hs:6:3: error:
• Couldn't match type ‘F a0’ with ‘F a’
Expected type: F a -> F a
Actual type: F a0 -> F a0
NB: ‘F’ is a type function, and may not be injective
NB: ‘F’ is a non-injective type family
The type variable ‘a0’ is ambiguous
• In the ambiguity check for ‘foo’
To defer the ambiguity check to use sites, enable AllowAmbiguousTypes
......
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