Commit 55ca1085 authored by Richard Eisenberg's avatar Richard Eisenberg Committed by Marge Bot

Fix #17405 by not checking imported equations

Previously, we checked all imported type family equations
for injectivity. This is very silly. Now, we check only
for conflicts.

Before I could even imagine doing the fix, I needed to untangle
several functions that were (in my opinion) overly complicated.
It's still not quite as perfect as I'd like, but it's good enough
for now.

Test case: typecheck/should_compile/T17405
parent fa25c8c4
......@@ -10,7 +10,7 @@ module FamInst (
newFamInst,
-- * Injectivity
makeInjectivityErrors
reportInjectivityErrors, reportConflictingInjectivityErrs
) where
import GhcPrelude
......@@ -44,6 +44,7 @@ import VarSet
import FV
import Bag( Bag, unionBags, unitBag )
import Control.Monad
import Data.List.NonEmpty ( NonEmpty(..) )
import qualified GHC.LanguageExtensions as LangExt
......@@ -682,10 +683,13 @@ addLocalFamInst (home_fie, my_fis) fam_inst
home_fie' = extendFamInstEnv home_fie fam_inst
-- Check for conflicting instance decls and injectivity violations
; no_conflict <- checkForConflicts inst_envs fam_inst
; injectivity_ok <- checkForInjectivityConflicts inst_envs fam_inst
; ((), no_errs) <- askNoErrs $
do { checkForConflicts inst_envs fam_inst
; checkForInjectivityConflicts inst_envs fam_inst
; checkInjectiveEquation fam_inst
}
; if no_conflict && injectivity_ok then
; if no_errs then
return (home_fie', fam_inst : my_fis)
else
return (home_fie, my_fis) }
......@@ -701,7 +705,8 @@ Check whether a single family instance conflicts with those in two instance
environments (one for the EPS and one for the HPT).
-}
checkForConflicts :: FamInstEnvs -> FamInst -> TcM Bool
-- | Checks to make sure no two family instances overlap.
checkForConflicts :: FamInstEnvs -> FamInst -> TcM ()
checkForConflicts inst_envs fam_inst
= do { let conflicts = lookupFamInstEnvConflicts inst_envs fam_inst
; traceTc "checkForConflicts" $
......@@ -709,64 +714,70 @@ checkForConflicts inst_envs fam_inst
, ppr fam_inst
-- , ppr inst_envs
]
; reportConflictInstErr fam_inst conflicts
; return (null conflicts) }
; reportConflictInstErr fam_inst conflicts }
checkForInjectivityConflicts :: FamInstEnvs -> FamInst -> TcM ()
-- see Note [Verifying injectivity annotation] in FamInstEnv, check 1B1.
checkForInjectivityConflicts instEnvs famInst
| isTypeFamilyTyCon tycon -- as opposed to data family tycon
, Injective inj <- tyConInjectivityInfo tycon
= let conflicts = lookupFamInstEnvInjectivityConflicts inj instEnvs famInst in
reportConflictingInjectivityErrs tycon conflicts (coAxiomSingleBranch (fi_axiom famInst))
| otherwise
= return ()
where tycon = famInstTyCon famInst
-- | Check whether a new open type family equation can be added without
-- violating injectivity annotation supplied by the user. Returns True when
-- this is possible and False if adding this equation would violate injectivity
-- annotation.
checkForInjectivityConflicts :: FamInstEnvs -> FamInst -> TcM Bool
-- annotation. This looks only at the one equation; it does not look for
-- interaction between equations. Use checkForInjectivityConflicts for that.
-- Does checks (2)-(4) of Note [Verifying injectivity annotation] in FamInstEnv.
checkInjectiveEquation :: FamInst -> TcM ()
checkInjectiveEquation famInst
| isTypeFamilyTyCon tycon
-- type family is injective in at least one argument
, Injective inj <- tyConInjectivityInfo tycon = do
{ dflags <- getDynFlags
; let axiom = coAxiomSingleBranch fi_ax
; let axiom = coAxiomSingleBranch fi_ax
-- see Note [Verifying injectivity annotation] in FamInstEnv
-- see Note [Verifying injectivity annotation] in FamInstEnv
errs = makeInjectivityErrors dflags fi_ax axiom inj conflicts
; mapM_ (\(err, span) -> setSrcSpan span $ addErr err) errs
; reportInjectivityErrors dflags fi_ax axiom inj
}
-- if there was no injectivity annotation or tycon does not represent a
-- type family we report no conflicts
-- type family we report no conflicts
| otherwise
= return ()
where tycon = famInstTyCon famInst
fi_ax = fi_axiom famInst
-- | Build a list of injectivity errors together with their source locations.
-- | Report a list of injectivity errors together with their source locations.
-- Looks only at one equation; does not look for conflicts *among* equations.
reportInjectivityErrors
:: DynFlags
-> CoAxiom br -- ^ Type family for which we generate errors
-> CoAxBranch -- ^ Currently checked equation (represented by axiom)
-> [Bool] -- ^ Injectivity annotation
-> [Bool] -- ^ Injectivity annotation
-> [CoAxBranch] -- ^ List of injectivity conflicts
-> [(SDoc, SrcSpan)]
-> TcM ()
reportInjectivityErrors dflags fi_ax axiom inj
= ASSERT2( any id inj, text "No injective type variables" )
= ASSERT2( any id inj, text "No injective type variables" )
let lhs = coAxBranchLHS axiom
rhs = coAxBranchRHS axiom
fam_tc = coAxiomTyCon fi_ax
are_conflicts = not $ null conflicts
(unused_inj_tvs, unused_vis, undec_inst_flag)
= unusedInjTvsInRHS dflags fam_tc lhs rhs
inj_tvs_unused = not $ isEmptyVarSet unused_inj_tvs
tf_headed = isTFHeaded rhs
bare_variables = bareTvInRHSViolated lhs rhs
wrong_bare_rhs = not $ null bare_variables
err_builder herald eqns
= ( hang herald
2 (vcat (map (pprCoAxBranchUser fam_tc) eqns))
, coAxBranchSpan (head eqns) )
errorIf p f = if p then [f err_builder axiom] else []
in errorIf are_conflicts (conflictInjInstErr conflicts )
++ errorIf inj_tvs_unused (unusedInjectiveVarsErr unused_inj_tvs
unused_vis undec_inst_flag)
++ errorIf tf_headed tfHeadedErr
do let lhs = coAxBranchLHS axiom
rhs = coAxBranchRHS axiom
fam_tc = coAxiomTyCon fi_ax
(unused_inj_tvs, unused_vis, undec_inst_flag)
= unusedInjTvsInRHS dflags fam_tc lhs rhs
inj_tvs_unused = not $ isEmptyVarSet unused_inj_tvs
tf_headed = isTFHeaded rhs
bare_variables = bareTvInRHSViolated lhs rhs
wrong_bare_rhs = not $ null bare_variables
when inj_tvs_unused $ reportUnusedInjectiveVarsErr fam_tc unused_inj_tvs
unused_vis undec_inst_flag axiom
when tf_headed $ reportTfHeadedErr fam_tc axiom
when wrong_bare_rhs $ reportBareVariableInRHSErr fam_tc bare_variables axiom
-- | Is type headed by a type family application?
isTFHeaded :: Type -> Bool
......@@ -906,8 +917,8 @@ unusedInjTvsInRHS :: DynFlags
-> [Type] -- LHS arguments
-> Type -- the RHS
-> ( TyVarSet
, Bool -- True <=> one or more variable is used invisibly
, Bool) -- True <=> suggest -XUndecidableInstances
, Bool -- True <=> one or more variable is used invisibly
, Bool ) -- True <=> suggest -XUndecidableInstances
-- See Note [Verifying injectivity annotation] in FamInstEnv.
-- This function implements check (4) described there, further
-- described in Note [Coverage condition for injective type families].
......@@ -945,51 +956,42 @@ unusedInjTvsInRHS _ _ _ _ = (emptyVarSet, False, False)
-- Producing injectivity error messages
---------------------------------------
-- | Type of functions that use error message and a list of axioms to build full
-- error message (with a source location) for injective type families.
type InjErrorBuilder = SDoc -> [CoAxBranch] -> (SDoc, SrcSpan)
-- | Build injecivity error herald common to all injectivity errors.
injectivityErrorHerald :: Bool -> SDoc
injectivityErrorHerald isSingular =
text "Type family equation" <> s isSingular <+> text "violate" <>
s (not isSingular) <+> text "injectivity annotation" <>
if isSingular then dot else colon
-- Above is an ugly hack. We want this: "sentence. herald:" (note the dot and
-- colon). But if herald is empty we want "sentence:" (note the colon). We
-- can't test herald for emptiness so we rely on the fact that herald is empty
-- only when isSingular is False. If herald is non empty it must end with a
-- colon.
where
s False = text "s"
s True = empty
-- | Build error message for a pair of equations violating an injectivity
-- annotation.
conflictInjInstErr :: [CoAxBranch] -> InjErrorBuilder -> CoAxBranch
-> (SDoc, SrcSpan)
conflictInjInstErr conflictingEqns errorBuilder tyfamEqn
| confEqn : _ <- conflictingEqns
= errorBuilder (injectivityErrorHerald False) [confEqn, tyfamEqn]
| otherwise
= panic "conflictInjInstErr"
-- | Report error message for a pair of equations violating an injectivity
-- annotation. No error message if there are no branches.
reportConflictingInjectivityErrs :: TyCon -> [CoAxBranch] -> CoAxBranch -> TcM ()
reportConflictingInjectivityErrs _ [] _ = return ()
reportConflictingInjectivityErrs fam_tc (confEqn1:_) tyfamEqn
= addErrs [buildInjectivityError fam_tc herald (confEqn1 :| [tyfamEqn])]
where
herald = text "Type family equation right-hand sides overlap; this violates" $$
text "the family's injectivity annotation:"
-- | Injectivity error herald common to all injectivity errors.
injectivityErrorHerald :: SDoc
injectivityErrorHerald =
text "Type family equation violates the family's injectivity annotation."
-- | Build error message for equation with injective type variables unused in
-- | Report error message for equation with injective type variables unused in
-- the RHS. Note [Coverage condition for injective type families], step 6
unusedInjectiveVarsErr :: TyVarSet
-> Bool -- True <=> print invisible arguments
-> Bool -- True <=> suggest -XUndecidableInstances
-> InjErrorBuilder -> CoAxBranch
-> (SDoc, SrcSpan)
unusedInjectiveVarsErr tvs has_kinds undec_inst errorBuilder tyfamEqn
= let (doc, loc) = errorBuilder (injectivityErrorHerald True $$ msg)
[tyfamEqn]
in (pprWithExplicitKindsWhen has_kinds doc, loc)
reportUnusedInjectiveVarsErr :: TyCon
-> TyVarSet
-> Bool -- True <=> print invisible arguments
-> Bool -- True <=> suggest -XUndecidableInstances
-> CoAxBranch
-> TcM ()
reportUnusedInjectiveVarsErr fam_tc tvs has_kinds undec_inst tyfamEqn
= let (loc, doc) = buildInjectivityError fam_tc
(injectivityErrorHerald $$
herald $$
text "In the type family equation:")
(tyfamEqn :| [])
in addErrAt loc (pprWithExplicitKindsWhen has_kinds doc)
where
doc = sep [ what <+> text "variable" <>
herald = sep [ what <+> text "variable" <>
pluralVarSet tvs <+> pprVarSet tvs (pprQuotedList . scopedSort)
, text "cannot be inferred from the right-hand side." ]
$$ extra
$$ extra
what | has_kinds = text "Type/kind"
| otherwise = text "Type"
......@@ -997,28 +999,33 @@ unusedInjectiveVarsErr tvs has_kinds undec_inst errorBuilder tyfamEqn
extra | undec_inst = text "Using UndecidableInstances might help"
| otherwise = empty
msg = doc $$ text "In the type family equation:"
-- | Build error message for equation that has a type family call at the top
-- | Report error message for equation that has a type family call at the top
-- level of RHS
tfHeadedErr :: InjErrorBuilder -> CoAxBranch
-> (SDoc, SrcSpan)
tfHeadedErr errorBuilder famInst
= errorBuilder (injectivityErrorHerald True $$
text "RHS of injective type family equation cannot" <+>
text "be a type family:") [famInst]
-- | Build error message for equation that has a bare type variable in the RHS
reportTfHeadedErr :: TyCon -> CoAxBranch -> TcM ()
reportTfHeadedErr fam_tc branch
= addErrs [buildInjectivityError fam_tc
(injectivityErrorHerald $$
text "RHS of injective type family equation cannot" <+>
text "be a type family:")
(branch :| [])]
-- | Report error message for equation that has a bare type variable in the RHS
-- but LHS pattern is not a bare type variable.
bareVariableInRHSErr :: [Type] -> InjErrorBuilder -> CoAxBranch
-> (SDoc, SrcSpan)
bareVariableInRHSErr tys errorBuilder famInst
= errorBuilder (injectivityErrorHerald True $$
reportBareVariableInRHSErr :: TyCon -> [Type] -> CoAxBranch -> TcM ()
reportBareVariableInRHSErr fam_tc tys branch
= addErrs [buildInjectivityError fam_tc
(injectivityErrorHerald $$
text "RHS of injective type family equation is a bare" <+>
text "type variable" $$
text "but these LHS type and kind patterns are not bare" <+>
text "variables:" <+> pprQuotedList tys) [famInst]
text "variables:" <+> pprQuotedList tys)
(branch :| [])]
buildInjectivityError :: TyCon -> SDoc -> NonEmpty CoAxBranch -> (SrcSpan, SDoc)
buildInjectivityError fam_tc herald (eqn1 :| rest_eqns)
= ( coAxBranchSpan eqn1
, hang herald
2 (vcat (map (pprCoAxBranchUser fam_tc) (eqn1 : rest_eqns))) )
reportConflictInstErr :: FamInst -> [FamInstMatch] -> TcRn ()
reportConflictInstErr _ []
......
......@@ -50,7 +50,7 @@ import TcEnv ( tcInitTidyEnv, tcInitOpenTidyEnv )
import FunDeps
import FamInstEnv ( isDominatedBy, injectiveBranches,
InjectivityCheckResult(..) )
import FamInst ( makeInjectivityErrors )
import FamInst
import Name
import VarEnv
import VarSet
......@@ -2031,8 +2031,8 @@ checkValidCoAxiom ax@(CoAxiom { co_ax_tc = fam_tc, co_ax_branches = branches })
; let conflicts =
fst $ foldl' (gather_conflicts inj prev_branches cur_branch)
([], 0) prev_branches
; mapM_ (\(err, span) -> setSrcSpan span $ addErr err)
(makeInjectivityErrors dflags ax cur_branch inj conflicts) }
; reportConflictingInjectivityErrs fam_tc conflicts cur_branch
; reportInjectivityErrors dflags ax cur_branch inj }
| otherwise
= return ()
......
......@@ -202,7 +202,7 @@ pprCoAxiom ax@(CoAxiom { co_ax_tc = tc, co_ax_branches = branches })
2 (vcat (map (pprCoAxBranchUser tc) (fromBranches branches)))
pprCoAxBranchUser :: TyCon -> CoAxBranch -> SDoc
-- Used when printing injectivity errors (FamInst.makeInjectivityErrors)
-- Used when printing injectivity errors (FamInst.reportInjectivityErrors)
-- and inaccessible branches (TcValidity.inaccessibleCoAxBranch)
-- This happens in error messages: don't print the RHS of a data
-- family axiom, which is meaningless to a user
......
......@@ -895,6 +895,13 @@ conditions hold:
There are subtleties here. See Note [Coverage condition for injective type families]
in FamInst.
Check (1) must be done for all family instances (transitively) imported. Other
checks (2-4) should be done just for locally written equations, as they are checks
involving just a single equation, not about interactions. Doing the other checks for
imported equations led to #17405, as the behavior of check (4) depends on
-XUndecidableInstances (see Note [Coverage condition for injective type families] in
FamInst), which may vary between modules.
See also Note [Injective type families] in TyCon
-}
......
......@@ -49,6 +49,8 @@ module Util (
changeLast,
whenNonEmpty,
-- * Tuples
fstOf3, sndOf3, thdOf3,
firstM, first3M, secondM,
......@@ -137,6 +139,7 @@ import Data.Data
import Data.IORef ( IORef, newIORef, atomicModifyIORef' )
import System.IO.Unsafe ( unsafePerformIO )
import Data.List hiding (group)
import Data.List.NonEmpty ( NonEmpty(..) )
import GHC.Exts
import GHC.Stack (HasCallStack)
......@@ -610,6 +613,10 @@ changeLast [] _ = panic "changeLast"
changeLast [_] x = [x]
changeLast (x:xs) x' = x : changeLast xs x'
whenNonEmpty :: Applicative m => [a] -> (NonEmpty a -> m ()) -> m ()
whenNonEmpty [] _ = pure ()
whenNonEmpty (x:xs) f = f (x :| xs)
{-
************************************************************************
* *
......
......@@ -7,11 +7,12 @@ T8165_fail1.hs:17:12: error:
• In the newtype declaration for ‘MyInt’
T8165_fail1.hs:25:8: error:
Type family equations violate injectivity annotation:
Type family equation right-hand sides overlap; this violates
the family's injectivity annotation:
S Int = Char -- Defined at T8165_fail1.hs:25:8
S WrappedInt = S Int -- Defined at T8165_fail1.hs:28:12
T8165_fail1.hs:28:12: error:
Type family equation violates injectivity annotation.
Type family equation violates the family's injectivity annotation.
RHS of injective type family equation cannot be a type family:
S WrappedInt = S Int -- Defined at T8165_fail1.hs:28:12
<interactive>:10:15: error:
Type family equations violate injectivity annotation:
Type family equation right-hand sides overlap; this violates
the family's injectivity annotation:
F Char Bool Int = Int -- Defined at <interactive>:10:15
F Bool Int Char = Int -- Defined at <interactive>:11:15
<interactive>:16:15: error:
Type family equations violate injectivity annotation:
Type family equation right-hand sides overlap; this violates
the family's injectivity annotation:
I Int Char Bool = Bool -- Defined at <interactive>:16:15
I Int Int Int = Bool -- Defined at <interactive>:17:15
<interactive>:26:15: error:
Type family equation violates injectivity annotation.
Type family equation violates the family's injectivity annotation.
RHS of injective type family equation cannot be a type family:
IdProxy a = Id a -- Defined at <interactive>:26:15
<interactive>:34:15: error:
Type family equation violates injectivity annotation.
Type family equation violates the family's injectivity annotation.
RHS of injective type family equation is a bare type variable
but these LHS type and kind patterns are not bare variables: ‘'Z’
P 'Z m = m -- Defined at <interactive>:34:15
<interactive>:40:15: error:
Type family equation violates injectivity annotation.
Type family equation violates the family's injectivity annotation.
Type variable ‘b’ cannot be inferred from the right-hand side.
In the type family equation:
J Int b c = Char -- Defined at <interactive>:40:15
<interactive>:44:15: error:
Type family equation violates injectivity annotation.
Type family equation violates the family's injectivity annotation.
Type variable ‘n’ cannot be inferred from the right-hand side.
In the type family equation:
K ('S n) m = 'S m -- Defined at <interactive>:44:15
<interactive>:49:15: error:
Type family equation violates injectivity annotation.
Type family equation violates the family's injectivity annotation.
RHS of injective type family equation cannot be a type family:
L a = MaybeSyn a -- Defined at <interactive>:49:15
<interactive>:55:41: error:
Type family equation violates injectivity annotation.
Type family equation violates the family's injectivity annotation.
Type/kind variable ‘k1’
cannot be inferred from the right-hand side.
In the type family equation:
......@@ -46,7 +48,7 @@
-- Defined at <interactive>:55:41
<interactive>:60:15: error:
Type family equation violates injectivity annotation.
Type family equation violates the family's injectivity annotation.
Type/kind variable ‘k1’
cannot be inferred from the right-hand side.
In the type family equation:
......@@ -54,14 +56,14 @@
-- Defined at <interactive>:60:15
<interactive>:64:15: error:
Type family equation violates injectivity annotation.
Type family equation violates the family's injectivity annotation.
Type/kind variable ‘k’ cannot be inferred from the right-hand side.
In the type family equation:
forall k (a :: k) (b :: k).
Fc @k a b = Int -- Defined at <interactive>:64:15
<interactive>:68:15: error:
Type family equation violates injectivity annotation.
Type family equation violates the family's injectivity annotation.
Type/kind variables ‘k’, ‘a’, ‘b’
cannot be inferred from the right-hand side.
In the type family equation:
......@@ -69,49 +71,54 @@
Gc @k a b = Int -- Defined at <interactive>:68:15
<interactive>:81:15: error:
Type family equations violate injectivity annotation:
Type family equation right-hand sides overlap; this violates
the family's injectivity annotation:
F1 [a] = Maybe (GF1 a) -- Defined at <interactive>:81:15
F1 (Maybe a) = Maybe (GF2 a) -- Defined at <interactive>:82:15
<interactive>:85:15: error:
Type family equation violates injectivity annotation.
Type family equation violates the family's injectivity annotation.
RHS of injective type family equation is a bare type variable
but these LHS type and kind patterns are not bare variables: ‘[a]’
W1 [a] = a -- Defined at <interactive>:85:15
<interactive>:88:15: error:
Type family equation violates injectivity annotation.
Type family equation violates the family's injectivity annotation.
RHS of injective type family equation cannot be a type family:
W2 [a] = W2 a -- Defined at <interactive>:88:15
<interactive>:92:15: error:
Type family equations violate injectivity annotation:
Type family equation right-hand sides overlap; this violates
the family's injectivity annotation:
Z1 [a] = (a, a) -- Defined at <interactive>:92:15
Z1 (Maybe b) = (b, [b]) -- Defined at <interactive>:93:15
<interactive>:96:15: error:
Type family equations violate injectivity annotation:
Type family equation right-hand sides overlap; this violates
the family's injectivity annotation:
G1 [a] = [a] -- Defined at <interactive>:96:15
G1 (Maybe b) = [(b, b)] -- Defined at <interactive>:97:15
<interactive>:100:15: error:
Type family equations violate injectivity annotation:
Type family equation right-hand sides overlap; this violates
the family's injectivity annotation:
G3 a Int = (a, Int) -- Defined at <interactive>:100:15
G3 a Bool = (Bool, a) -- Defined at <interactive>:101:15
<interactive>:104:15: error:
Type family equation violates injectivity annotation.
Type family equation violates the family's injectivity annotation.
Type variable ‘b’ cannot be inferred from the right-hand side.
In the type family equation:
G4 a b = [a] -- Defined at <interactive>:104:15
<interactive>:107:15: error:
Type family equations violate injectivity annotation:
Type family equation right-hand sides overlap; this violates
the family's injectivity annotation:
G5 [a] = [GF1 a] -- Defined at <interactive>:107:15
G5 Int = [Bool] -- Defined at <interactive>:108:15
<interactive>:111:15: error:
Type family equation violates injectivity annotation.
Type family equation violates the family's injectivity annotation.
Type variable ‘a’ cannot be inferred from the right-hand side.
In the type family equation:
G6 [a] = [HF1 a] -- Defined at <interactive>:111:15
{-# LANGUAGE TypeFamilyDependencies, UndecidableInstances #-}
module T17405a where
data D a
type family F a = r | r -> a
type instance F (D a) = D (F a)
{-# LANGUAGE TypeFamilyDependencies #-}
module T17405b where
type family F2 a
type instance F2 Int = Bool
module T17405c where
import T17405a
import T17405b
......@@ -293,3 +293,4 @@ test('T16632', normal, compile, ['-Wunused-type-patterns -fdiagnostics-show-care
test('T16828', normal, compile, [''])
test('T17008b', normal, compile, [''])
test('T17056', normal, compile, [''])
test('T17405', normal, multimod_compile, ['T17405c', '-v0'])
T6018th.hs:98:4: error:
Type family equations violate injectivity annotation:
Type family equation right-hand sides overlap; this violates
the family's injectivity annotation:
H Int Int Int = Bool -- Defined at T6018th.hs:98:4
H Int Char Bool = Bool -- Defined at T6018th.hs:98:4
T10836.hs:5:5: error:
Type family equations violate injectivity annotation:
Foo Int = Int -- Defined at T10836.hs:5:5
Foo Bool = Int -- Defined at T10836.hs:6:5
In the equations for closed type family ‘Foo’
In the type family declaration for ‘Foo’
• Type family equation right-hand sides overlap; this violates
the family's injectivity annotation:
Foo Int = Int -- Defined at T10836.hs:5:5
Foo Bool = Int -- Defined at T10836.hs:6:5
• In the equations for closed type family ‘Foo’
In the type family declaration for ‘Foo’
T10836.hs:9:5: error:
Type family equations violate injectivity annotation:
Bar Int = Int -- Defined at T10836.hs:9:5
Bar Bool = Int -- Defined at T10836.hs:10:5
In the equations for closed type family ‘Bar’
In the type family declaration for ‘Bar’
• Type family equation right-hand sides overlap; this violates
the family's injectivity annotation:
Bar Int = Int -- Defined at T10836.hs:9:5
Bar Bool = Int -- Defined at T10836.hs:10:5
• In the equations for closed type family ‘Bar’
In the type family declaration for ‘Bar’
T12430.hs:6:3: error:
• Type family equation violates injectivity annotation.
• Type family equation violates the family's injectivity annotation.
Type variable ‘x’ cannot be inferred from the right-hand side.
In the type family equation:
F x = C x -- Defined at T12430.hs:6:3
......
T16512b.hs:6:3: error:
• Type family equation violates injectivity annotation.
• Type family equation violates the family's injectivity annotation.
Type variable ‘a’ cannot be inferred from the right-hand side.
Using UndecidableInstances might help
In the type family equation:
......
......@@ -5,60 +5,65 @@
[5 of 5] Compiling T6018fail ( T6018fail.hs, T6018fail.o )
T6018Afail.hs:9:15: error:
Type family equations violate injectivity annotation:
Type family equation right-hand sides overlap; this violates
the family's injectivity annotation:
G Char Bool Int = Int -- Defined at T6018Afail.hs:9:15
G Bool Int Char = Int -- Defined at T6018fail.hs:17:15
T6018Cfail.hs:8:15: error:
Type family equations violate injectivity annotation:
Type family equation right-hand sides overlap; this violates
the family's injectivity annotation:
T6018Bfail.H Char Bool Int = Int -- Defined at T6018Cfail.hs:8:15
T6018Bfail.H Bool Int Char = Int -- Defined at T6018Dfail.hs:7:15
T6018fail.hs:15:15: error:
Type family equations violate injectivity annotation:
Type family equation right-hand sides overlap; this violates
the family's injectivity annotation:
F Bool Int Char = Int -- Defined at T6018fail.hs:15:15
F Char Bool Int = Int -- Defined at T6018fail.hs:14:15
T6018fail.hs:21:15: error:
Type family equations violate injectivity annotation:
Type family equation right-hand sides overlap; this violates
the family's injectivity annotation:
I Int Int Int = Bool -- Defined at T6018fail.hs:21:15
I Int Char Bool = Bool -- Defined at T6018fail.hs:20:15
T6018fail.hs:30:15: error:
Type family equation violates injectivity annotation.
Type family equation violates the family's injectivity annotation.
RHS of injective type family equation cannot be a type family:
IdProxy a = Id a -- Defined at T6018fail.hs:30:15
T6018fail.hs:38:15: error:
Type family equation violates injectivity annotation.