Implement a coverage checker for injectivity
authorRichard Eisenberg <rae@cs.brynmawr.edu>
Wed, 4 Sep 2019 01:10:59 +0000 (21:10 -0400)
committerMarge Bot <ben+marge-bot@smart-cactus.org>
Wed, 23 Oct 2019 09:58:46 +0000 (05:58 -0400)
This fixes #16512.

There are lots of parts of this patch:

* The main payload is in FamInst. See
Note [Coverage condition for injective type families] there
for the overview. But it doesn't fix the bug.

* We now bump the reduction depth every time we discharge
a CFunEqCan. See Note [Flatten when discharging CFunEqCan]
in TcInteract.

* Exploration of this revealed a new, easy to maintain invariant
for CTyEqCans. See Note [Almost function-free] in TcRnTypes.

* We also realized that type inference for injectivity was a
bit incomplete. This means we exchanged lookupFlattenTyVar for
rewriteTyVar. See Note [rewriteTyVar] in TcFlatten. The new
function is monadic while the previous one was pure, necessitating
some faff in TcInteract. Nothing too bad.

* zonkCt did not maintain invariants on CTyEqCan. It's not worth
the bother doing so, so we just transmute CTyEqCans to
CNonCanonicals.

* The pure unifier was finding the fixpoint of the returned
substitution, even when doing one-way matching (in tcUnifyTysWithTFs).
Fixed now.

Test cases: typecheck/should_fail/T16512{a,b}

38 files changed:
compiler/typecheck/Constraint.hs
compiler/typecheck/FamInst.hs
compiler/typecheck/FunDeps.hs
compiler/typecheck/TcCanonical.hs
compiler/typecheck/TcFlatten.hs
compiler/typecheck/TcInteract.hs
compiler/typecheck/TcMType.hs
compiler/typecheck/TcSMonad.hs
compiler/typecheck/TcType.hs
compiler/typecheck/TcValidity.hs
compiler/types/FamInstEnv.hs
compiler/types/TyCoFVs.hs
compiler/types/TyCoPpr.hs
compiler/types/Type.hs
compiler/types/Type.hs-boot
compiler/types/Unify.hs
compiler/utils/Util.hs
docs/users_guide/glasgow_exts.rst
testsuite/tests/ghci/scripts/T6018ghcifail.stderr
testsuite/tests/indexed-types/should_compile/T12522.hs
testsuite/tests/indexed-types/should_compile/T12522b.hs
testsuite/tests/indexed-types/should_compile/T13705.hs
testsuite/tests/indexed-types/should_fail/T12522a.hs
testsuite/tests/indexed-types/should_fail/T12522a.stderr
testsuite/tests/indexed-types/should_fail/T14369.hs
testsuite/tests/indexed-types/should_fail/T14369.stderr
testsuite/tests/indexed-types/should_fail/T7788.stderr
testsuite/tests/indexed-types/should_fail/T9554.stderr
testsuite/tests/th/T14060.stdout
testsuite/tests/typecheck/should_compile/T13822.hs
testsuite/tests/typecheck/should_compile/T6018.hs
testsuite/tests/typecheck/should_fail/T16512a.hs [new file with mode: 0644]
testsuite/tests/typecheck/should_fail/T16512a.stderr [new file with mode: 0644]
testsuite/tests/typecheck/should_fail/T16512b.hs [new file with mode: 0644]
testsuite/tests/typecheck/should_fail/T16512b.stderr [new file with mode: 0644]
testsuite/tests/typecheck/should_fail/T6018fail.stderr
testsuite/tests/typecheck/should_fail/T6018failclosed.stderr
testsuite/tests/typecheck/should_fail/all.T

index acc3352..b518acf 100644 (file)
@@ -160,16 +160,14 @@ data Ct
 
   | CTyEqCan {  -- tv ~ rhs
        -- Invariants:
-       --   * See Note [Applying the inert substitution] in TcFlatten
+       --   * See Note [inert_eqs: the inert equalities] in TcSMonad
        --   * tv not in tvs(rhs)   (occurs check)
        --   * If tv is a TauTv, then rhs has no foralls
        --       (this avoids substituting a forall for the tyvar in other types)
        --   * tcTypeKind ty `tcEqKind` tcTypeKind tv; Note [Ct kind invariant]
        --   * rhs may have at most one top-level cast
-       --   * rhs (perhaps under the one cast) is not necessarily function-free,
-       --       but it has no top-level function.
-       --     E.g. a ~ [F b]  is fine
-       --     but  a ~ F b    is not
+       --   * rhs (perhaps under the one cast) is *almost function-free*,
+       --       See Note [Almost function-free]
        --   * If the equality is representational, rhs has no top-level newtype
        --     See Note [No top-level newtypes on RHS of representational
        --     equalities] in TcCanonical
@@ -289,6 +287,55 @@ of the rhs. This is necessary because both constraints are used for substitution
 during solving. If the kinds differed, then the substitution would take a well-kinded
 type to an ill-kinded one.
 
+Note [Almost function-free]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~
+A type is *almost function-free* if it has no type functions (something that
+responds True to isTypeFamilyTyCon), except (possibly)
+ * under a forall, or
+ * in a coercion (either in a CastTy or a CercionTy)
+
+The RHS of a CTyEqCan must be almost function-free. This is for two reasons:
+
+1. There cannot be a top-level function. If there were, the equality should
+   really be a CFunEqCan, not a CTyEqCan.
+
+2. Nested functions aren't too bad, on the other hand. However, consider this
+   scenario:
+
+     type family F a = r | r -> a
+
+     [D] F ty1 ~ fsk1
+     [D] F ty2 ~ fsk2
+     [D] fsk1 ~ [G Int]
+     [D] fsk2 ~ [G Bool]
+
+     type instance G Int = Char
+     type instance G Bool = Char
+
+   If it was the case that fsk1 = fsk2, then we could unifty ty1 and ty2 --
+   good! They don't look equal -- but if we aggressively reduce that G Int and
+   G Bool they would become equal. The "almost function free" makes sure that
+   these redexes are exposed.
+
+   Note that this equality does *not* depend on casts or coercions, and so
+   skipping these forms is OK. In addition, the result of a type family cannot
+   be a polytype, so skipping foralls is OK, too. We skip foralls because we
+   want the output of the flattener to be almost function-free. See Note
+   [Flattening under a forall] in TcFlatten.
+
+   As I (Richard E) write this, it is unclear if the scenario pictured above
+   can happen -- I would expect the G Int and G Bool to be reduced. But
+   perhaps it can arise somehow, and maintaining almost function-free is cheap.
+
+Historical note: CTyEqCans used to require only condition (1) above: that no
+type family was at the top of an RHS. But work on #16512 suggested that the
+injectivity checks were not complete, and adding the requirement that functions
+do not appear even in a nested fashion was easy (it was already true, but
+unenforced).
+
+The almost-function-free property is checked by isAlmostFunctionFree in TcType.
+The flattener (in TcFlatten) produces types that are almost function-free.
+
 -}
 
 mkNonCanonical :: CtEvidence -> Ct
@@ -1637,8 +1684,7 @@ equality simplification, and type family reduction. (Why combine these? Because
 it's actually quite easy to mistake one for another, in sufficiently involved
 scenarios, like ConstraintKinds.)
 
-The flag -fcontext-stack=n (not very well named!) fixes the maximium
-level.
+The flag -freduction-depth=n fixes the maximium level.
 
 * The counter includes the depth of type class instance declarations.  Example:
      [W] d{7} : Eq [Int]
index a339dd7..67178d6 100644 (file)
@@ -1,6 +1,6 @@
 -- The @FamInst@ type: family instance heads
 
-{-# LANGUAGE CPP, GADTs #-}
+{-# LANGUAGE CPP, GADTs, ViewPatterns #-}
 
 module FamInst (
         FamInstEnvs, tcGetFamInstEnvs,
@@ -10,7 +10,7 @@ module FamInst (
         newFamInst,
 
         -- * Injectivity
-        makeInjectivityErrors, injTyVarsOfType, injTyVarsOfTypes
+        makeInjectivityErrors
     ) where
 
 import GhcPrelude
@@ -36,14 +36,17 @@ import DataCon ( dataConName )
 import Maybes
 import Type
 import TyCoRep
+import TyCoFVs
 import TcMType
 import Name
-import Pair
 import Panic
 import VarSet
+import FV
 import Bag( Bag, unionBags, unitBag )
 import Control.Monad
 
+import qualified GHC.LanguageExtensions  as LangExt
+
 #include "HsVersions.h"
 
 {- Note [The type family instance consistency story]
@@ -719,10 +722,11 @@ checkForInjectivityConflicts instEnvs famInst
     | isTypeFamilyTyCon tycon
     -- type family is injective in at least one argument
     , Injective inj <- tyConInjectivityInfo tycon = do
-    { let axiom = coAxiomSingleBranch fi_ax
+    { dflags <- getDynFlags
+    ; let axiom = coAxiomSingleBranch fi_ax
           conflicts = lookupFamInstEnvInjectivityConflicts inj instEnvs famInst
           -- see Note [Verifying injectivity annotation] in FamInstEnv
-          errs = makeInjectivityErrors fi_ax axiom inj conflicts
+          errs = makeInjectivityErrors dflags fi_ax axiom inj conflicts
     ; mapM_ (\(err, span) -> setSrcSpan span $ addErr err) errs
     ; return (null errs)
     }
@@ -735,19 +739,21 @@ checkForInjectivityConflicts instEnvs famInst
 
 -- | Build a list of injectivity errors together with their source locations.
 makeInjectivityErrors
-   :: CoAxiom br   -- ^ Type family for which we generate errors
+   :: DynFlags
+   -> CoAxiom br   -- ^ Type family for which we generate errors
    -> CoAxBranch   -- ^ Currently checked equation (represented by axiom)
    -> [Bool]       -- ^ Injectivity annotation
    -> [CoAxBranch] -- ^ List of injectivity conflicts
    -> [(SDoc, SrcSpan)]
-makeInjectivityErrors fi_ax axiom inj conflicts
+makeInjectivityErrors dflags fi_ax axiom inj conflicts
   = 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  = unusedInjTvsInRHS fam_tc inj lhs rhs
-        inj_tvs_unused  = not $ and (isEmptyVarSet <$> unused_inj_tvs)
+        (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
@@ -758,81 +764,11 @@ makeInjectivityErrors fi_ax axiom inj conflicts
                           , 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)
+        ++ errorIf inj_tvs_unused (unusedInjectiveVarsErr unused_inj_tvs
+                                     unused_vis undec_inst_flag)
         ++ errorIf tf_headed       tfHeadedErr
         ++ errorIf wrong_bare_rhs (bareVariableInRHSErr   bare_variables)
 
-
--- | Return a list of type variables that the function is injective in and that
--- do not appear on injective positions in the RHS of a family instance
--- declaration. The returned Pair includes invisible vars followed by visible ones
-unusedInjTvsInRHS :: TyCon -> [Bool] -> [Type] -> Type -> Pair TyVarSet
--- INVARIANT: [Bool] list contains at least one True value
--- See Note [Verifying injectivity annotation] in FamInstEnv.
--- This function implements check (4) described there.
--- In theory, instead of implementing this whole check in this way, we could
--- attempt to unify equation with itself.  We would reject exactly the same
--- equations but this method gives us more precise error messages by returning
--- precise names of variables that are not mentioned in the RHS.
-unusedInjTvsInRHS tycon injList lhs rhs =
-  (`minusVarSet` injRhsVars) <$> injLhsVars
-    where
-      inj_pairs :: [(Type, ArgFlag)]
-      -- All the injective arguments, paired with their visibility
-      inj_pairs = ASSERT2( injList `equalLength` lhs
-                         , ppr tycon $$ ppr injList $$ ppr lhs )
-                  filterByList injList (lhs `zip` tyConArgFlags tycon lhs)
-
-      -- set of type and kind variables in which type family is injective
-      invis_lhs, vis_lhs :: [Type]
-      (invis_lhs, vis_lhs) = partitionInvisibles inj_pairs
-
-      invis_vars = tyCoVarsOfTypes invis_lhs
-      Pair invis_vars' vis_vars = splitVisVarsOfTypes vis_lhs
-      injLhsVars
-        = Pair (invis_vars `minusVarSet` vis_vars `unionVarSet` invis_vars')
-               vis_vars
-
-      -- set of type variables appearing in the RHS on an injective position.
-      -- For all returned variables we assume their associated kind variables
-      -- also appear in the RHS.
-      injRhsVars = injTyVarsOfType rhs
-
-injTyVarsOfType :: TcTauType -> TcTyVarSet
--- Collect all type variables that are either arguments to a type
---   constructor or to /injective/ type families.
--- Determining the overall type determines thes variables
---
--- E.g.   Suppose F is injective in its second arg, but not its first
---        then injVarOfType (Either a (F [b] (a,c))) = {a,c}
---        Determining the overall type determines a,c but not b.
-injTyVarsOfType ty
-  | Just ty' <- coreView ty -- #12430
-  = injTyVarsOfType ty'
-injTyVarsOfType (TyVarTy v)
-  = unitVarSet v `unionVarSet` injTyVarsOfType (tyVarKind v)
-injTyVarsOfType (TyConApp tc tys)
-  | isTypeFamilyTyCon tc
-  = case tyConInjectivityInfo tc of
-        NotInjective  -> emptyVarSet
-        Injective inj -> injTyVarsOfTypes (filterByList inj tys)
-  | otherwise
-  = injTyVarsOfTypes tys
-injTyVarsOfType (LitTy {})
-  = emptyVarSet
-injTyVarsOfType (FunTy _ arg res)
-  = injTyVarsOfType arg `unionVarSet` injTyVarsOfType res
-injTyVarsOfType (AppTy fun arg)
-  = injTyVarsOfType fun `unionVarSet` injTyVarsOfType arg
--- No forall types in the RHS of a type family
-injTyVarsOfType (CastTy ty _)   = injTyVarsOfType ty
-injTyVarsOfType (CoercionTy {}) = emptyVarSet
-injTyVarsOfType (ForAllTy {})    =
-    panic "unusedInjTvsInRHS.injTyVarsOfType"
-
-injTyVarsOfTypes :: [Type] -> VarSet
-injTyVarsOfTypes tys = mapUnionVarSet injTyVarsOfType tys
-
 -- | Is type headed by a type family application?
 isTFHeaded :: Type -> Bool
 -- See Note [Verifying injectivity annotation], case 3.
@@ -852,6 +788,163 @@ bareTvInRHSViolated pats rhs | isTyVarTy rhs
    = filter (not . isTyVarTy) pats
 bareTvInRHSViolated _ _ = []
 
+------------------------------------------------------------------
+-- Checking for the coverage condition for injective type families
+------------------------------------------------------------------
+
+{-
+Note [Coverage condition for injective type families]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+The Injective Type Families paper describes how we can tell whether
+or not a type family equation upholds the injectivity condition.
+Briefly, consider the following:
+
+  type family F a b = r | r -> a      -- NB: b is not injective
+
+  type instance F ty1 ty2 = ty3
+
+We need to make sure that all variables mentioned in ty1 are mentioned in ty3
+-- that's how we know that knowing ty3 determines ty1. But they can't be
+mentioned just anywhere in ty3: they must be in *injective* positions in ty3.
+For example:
+
+  type instance F a Int = Maybe (G a)
+
+This is no good, if G is not injective. However, if G is indeed injective,
+then this would appear to meet our needs. There is a trap here, though: while
+knowing G a does indeed determine a, trying to compute a from G a might not
+terminate. This is precisely the same problem that we have with functional
+dependencies and their liberal coverage condition. Here is the test case:
+
+  type family G a = r | r -> a
+  type instance G [a] = [G a]
+  [W] G alpha ~ [alpha]
+
+We see that the equation given applies, because G alpha equals a list. So we
+learn that alpha must be [beta] for some beta. We then have
+
+  [W] G [beta] ~ [[beta]]
+
+This can reduce to
+
+  [W] [G beta] ~ [[beta]]
+
+which then decomposes to
+
+  [W] G beta ~ [beta]
+
+right where we started. The equation G [a] = [G a] thus is dangerous: while
+it does not violate the injectivity assumption, it might throw us into a loop,
+with a particularly dastardly Wanted.
+
+We thus do what functional dependencies do: require -XUndecidableInstances to
+accept this.
+
+Checking the coverage condition is not terribly hard, but we also want to produce
+a nice error message. A nice error message has at least two properties:
+
+1. If any of the variables involved are invisible or are used in an invisible context,
+we want to print invisible arguments (as -fprint-explicit-kinds does).
+
+2. If we fail to accept the equation because we're worried about non-termination,
+we want to suggest UndecidableInstances.
+
+To gather the right information, we can talk about the *usage* of a variable. Every
+variable is used either visibly or invisibly, and it is either not used at all,
+in a context where acceptance requires UndecidableInstances, or in a context that
+does not require UndecidableInstances. If a variable is used both visibly and
+invisibly, then we want to remember the fact that it was used invisibly: printing
+out invisibles will be helpful for the user to understand what is going on.
+If a variable is used where we need -XUndecidableInstances and where we don't,
+we can similarly just remember the latter.
+
+We thus define Visibility and NeedsUndecInstFlag below. These enumerations are
+*ordered*, and we used their Ord instances. We then define VarUsage, which is just a pair
+of a Visibility and a NeedsUndecInstFlag. (The visibility is irrelevant when a
+variable is NotPresent, but this extra slack in the representation causes no
+harm.) We finally define VarUsages as a mapping from variables to VarUsage.
+Its Monoid instance combines two maps, using the Semigroup instance of VarUsage
+to combine elements that are represented in both maps. In this way, we can
+compositionally analyze types (and portions thereof).
+
+To do the injectivity check:
+
+1. We build VarUsages that represent the LHS (rather, the portion of the LHS
+that is flagged as injective); each usage on the LHS is NotPresent, because we
+hvae not yet looked at the RHS.
+
+2. We also build a VarUsage for the RHS, done by injTyVarUsages.
+
+3. We then combine these maps. Now, every variable in the injective components of the LHS
+will be mapped to its correct usage (either NotPresent or perhaps needing
+-XUndecidableInstances in order to be seen as injective).
+
+4. We look up each var used in an injective argument on the LHS in
+the map, making a list of tvs that should be determined by the RHS
+but aren't.
+
+5. We then return the set of bad variables, whether any of the bad
+ones were used invisibly, and whether any bad ones need -XUndecidableInstances.
+If -XUndecidableInstances is enabled, than a var that needs the flag
+won't be bad, so it won't appear in this list.
+
+6. We use all this information to produce a nice error message, (a) switching
+on -fprint-explicit-kinds if appropriate and (b) telling the user about
+-XUndecidableInstances if appropriate.
+
+-}
+
+-- | Return the set of type variables that a type family equation is
+-- expected to be injective in but is not. Suppose we have @type family
+-- F a b = r | r -> a@. Then any variables that appear free in the first
+-- argument to F in an equation must be fixed by that equation's RHS.
+-- This function returns all such variables that are not indeed fixed.
+-- It also returns whether any of these variables appear invisibly
+-- and whether -XUndecidableInstances would help.
+-- See Note [Coverage condition for injective type families].
+unusedInjTvsInRHS :: DynFlags
+                  -> TyCon  -- type family
+                  -> [Type] -- LHS arguments
+                  -> Type   -- the RHS
+                  -> ( TyVarSet
+                     , 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].
+-- In theory (and modulo the -XUndecidableInstances wrinkle),
+-- instead of implementing this whole check in this way, we could
+-- attempt to unify equation with itself.  We would reject exactly the same
+-- equations but this method gives us more precise error messages by returning
+-- precise names of variables that are not mentioned in the RHS.
+unusedInjTvsInRHS dflags tycon@(tyConInjectivityInfo -> Injective inj_list) lhs rhs =
+  -- Note [Coverage condition for injective type families], step 5
+  (bad_vars, any_invisible, suggest_undec)
+    where
+      undec_inst = xopt LangExt.UndecidableInstances dflags
+
+      inj_lhs = filterByList inj_list lhs
+      lhs_vars = tyCoVarsOfTypes inj_lhs
+
+      rhs_inj_vars = fvVarSet $ injectiveVarsOfType undec_inst rhs
+
+      bad_vars = lhs_vars `minusVarSet` rhs_inj_vars
+
+      any_bad = not $ isEmptyVarSet bad_vars
+
+      invis_vars = fvVarSet $ invisibleVarsOfTypes [mkTyConApp tycon lhs, rhs]
+
+      any_invisible = any_bad && (bad_vars `intersectsVarSet` invis_vars)
+      suggest_undec = any_bad &&
+                      not undec_inst &&
+                      (lhs_vars `subVarSet` fvVarSet (injectiveVarsOfType True rhs))
+
+-- When the type family is not injective in any arguments
+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.
@@ -883,26 +976,28 @@ conflictInjInstErr conflictingEqns errorBuilder tyfamEqn
   = panic "conflictInjInstErr"
 
 -- | Build error message for equation with injective type variables unused in
--- the RHS.
-unusedInjectiveVarsErr :: Pair TyVarSet -> InjErrorBuilder -> CoAxBranch
+-- 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 (Pair invis_vars vis_vars) errorBuilder tyfamEqn
+unusedInjectiveVarsErr tvs has_kinds undec_inst errorBuilder tyfamEqn
   = let (doc, loc) = errorBuilder (injectivityErrorHerald True $$ msg)
                                   [tyfamEqn]
     in (pprWithExplicitKindsWhen has_kinds doc, loc)
     where
-      tvs = invis_vars `unionVarSet` vis_vars
-      has_types = not $ isEmptyVarSet vis_vars
-      has_kinds = not $ isEmptyVarSet invis_vars
-
       doc = sep [ what <+> text "variable" <>
                   pluralVarSet tvs <+> pprVarSet tvs (pprQuotedList . scopedSort)
                 , text "cannot be inferred from the right-hand side." ]
-      what = case (has_types, has_kinds) of
-               (True, True)   -> text "Type and kind"
-               (True, False)  -> text "Type"
-               (False, True)  -> text "Kind"
-               (False, False) -> pprPanic "mkUnusedInjectiveVarsErr" $ ppr tvs
+            $$ extra
+
+      what | has_kinds = text "Type/kind"
+           | otherwise = text "Type"
+
+      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
index f8c4124..809e428 100644 (file)
@@ -29,10 +29,11 @@ import Type
 import TcType( transSuperClasses )
 import CoAxiom( TypeEqn )
 import Unify
-import FamInst( injTyVarsOfTypes )
 import InstEnv
 import VarSet
 import VarEnv
+import TyCoFVs
+import FV
 import Outputable
 import ErrUtils( Validity(..), allValid )
 import SrcLoc
@@ -550,7 +551,7 @@ oclose preds fixed_tvs
             -- closeOverKinds: see Note [Closing over kinds in coverage]
 
     tv_fds  :: [(TyCoVarSet,TyCoVarSet)]
-    tv_fds  = [ (tyCoVarsOfTypes ls, injTyVarsOfTypes rs)
+    tv_fds  = [ (tyCoVarsOfTypes ls, fvVarSet $ injectiveVarsOfTypes True rs)
                   -- See Note [Care with type functions]
               | pred <- preds
               , pred' <- pred : transSuperClasses pred
index 30ea3a9..2079020 100644 (file)
@@ -1302,10 +1302,10 @@ can_eq_app :: CtEvidence       -- :: s1 t1 ~N s2 t2
 -- to an irreducible constraint; see typecheck/should_compile/T10494
 -- See Note [Decomposing equality], note {4}
 can_eq_app ev s1 t1 s2 t2
-  | CtDerived { ctev_loc = loc } <- ev
+  | CtDerived {} <- ev
   = do { unifyDeriveds loc [Nominal, Nominal] [s1, t1] [s2, t2]
        ; stopWith ev "Decomposed [D] AppTy" }
-  | CtWanted { ctev_dest = dest, ctev_loc = loc } <- ev
+  | CtWanted { ctev_dest = dest } <- ev
   = do { co_s <- unifyWanted loc Nominal s1 s2
        ; let arg_loc
                | isNextArgVisible s1 = loc
@@ -1323,7 +1323,7 @@ can_eq_app ev s1 t1 s2 t2
   | s1k `mismatches` s2k
   = canEqHardFailure ev (s1 `mkAppTy` t1) (s2 `mkAppTy` t2)
 
-  | CtGiven { ctev_evar = evar, ctev_loc = loc } <- ev
+  | CtGiven { ctev_evar = evar } <- ev
   = do { let co   = mkTcCoVarCo evar
              co_s = mkTcLRCo CLeft  co
              co_t = mkTcLRCo CRight co
@@ -1335,6 +1335,8 @@ can_eq_app ev s1 t1 s2 t2
        ; canEqNC evar_s NomEq s1 s2 }
 
   where
+    loc = ctEvLoc ev
+
     s1k = tcTypeKind s1
     s2k = tcTypeKind s2
 
@@ -1585,6 +1587,7 @@ constraints: see Note [Instance and Given overlap] in TcInteract.
 Conclusion:
   * Decompose [W] N s ~R N t  iff there no given constraint that could
     later solve it.
+
 -}
 
 canDecomposableTyConAppOK :: CtEvidence -> EqRel
@@ -1848,9 +1851,9 @@ canEqTyVar :: CtEvidence          -- ev :: lhs ~ rhs
            -> TcType                -- lhs: pretty lhs, already flat
            -> TcType -> TcType      -- rhs: already flat
            -> TcS (StopOrContinue Ct)
-canEqTyVar ev eq_rel swapped tv1 ps_ty1 xi2 ps_xi2
+canEqTyVar ev eq_rel swapped tv1 ps_xi1 xi2 ps_xi2
   | k1 `tcEqType` k2
-  = canEqTyVarHomo ev eq_rel swapped tv1 ps_ty1 xi2 ps_xi2
+  = canEqTyVarHomo ev eq_rel swapped tv1 ps_xi1 xi2 ps_xi2
 
   -- So the LHS and RHS don't have equal kinds
   -- Note [Flattening] in TcFlatten gives us (F2), which says that
@@ -1889,7 +1892,7 @@ canEqTyVar ev eq_rel swapped tv1 ps_ty1 xi2 ps_xi2
                                                (mkTcReflCo role xi1) rhs_co
                        -- NB: rewriteEqEvidence executes a swap, if any, so we're
                        -- NotSwapped now.
-                 ; canEqTyVarHomo new_ev eq_rel NotSwapped tv1 ps_ty1 new_rhs ps_rhs }
+                 ; canEqTyVarHomo new_ev eq_rel NotSwapped tv1 ps_xi1 new_rhs ps_rhs }
          else
     do { let sym_k1_co = mkTcSymCo k1_co  -- :: kind(xi1) ~N flat_k1
              sym_k2_co = mkTcSymCo k2_co  -- :: kind(xi2) ~N flat_k2
@@ -1905,7 +1908,7 @@ canEqTyVar ev eq_rel swapped tv1 ps_ty1 xi2 ps_xi2
 
        ; new_ev <- rewriteEqEvidence ev swapped new_lhs new_rhs lhs_co rhs_co
          -- no longer swapped, due to rewriteEqEvidence
-       ; canEqTyVarHetero new_ev eq_rel tv1 sym_k1_co flat_k1 ps_ty1
+       ; canEqTyVarHetero new_ev eq_rel tv1 sym_k1_co flat_k1 ps_xi1
                                         new_rhs flat_k2 ps_rhs } }
   where
     xi1 = mkTyVarTy tv1
@@ -1969,16 +1972,16 @@ canEqTyVarHetero ev eq_rel tv1 co1 ki1 ps_tv1 xi2 ki2 ps_xi2
 canEqTyVarHomo :: CtEvidence
                -> EqRel -> SwapFlag
                -> TcTyVar                -- lhs: tv1
-               -> TcType                 -- pretty lhs
-               -> TcType -> TcType       -- rhs (might not be flat)
+               -> TcType                 -- pretty lhs, flat
+               -> TcType -> TcType       -- rhs, flat
                -> TcS (StopOrContinue Ct)
-canEqTyVarHomo ev eq_rel swapped tv1 ps_ty1 ty2 _
-  | Just (tv2, _) <- tcGetCastedTyVar_maybe ty2
+canEqTyVarHomo ev eq_rel swapped tv1 ps_xi1 xi2 _
+  | Just (tv2, _) <- tcGetCastedTyVar_maybe xi2
   , tv1 == tv2
   = canEqReflexive ev eq_rel (mkTyVarTy tv1)
     -- we don't need to check co because it must be reflexive
 
-  | Just (tv2, co2) <- tcGetCastedTyVar_maybe ty2
+  | Just (tv2, co2) <- tcGetCastedTyVar_maybe xi2
   , swapOverTyVars tv1 tv2
   = do { traceTcS "canEqTyVar swapOver" (ppr tv1 $$ ppr tv2 $$ ppr swapped)
          -- FM_Avoid commented out: see Note [Lazy flattening] in TcFlatten
@@ -1998,11 +2001,11 @@ canEqTyVarHomo ev eq_rel swapped tv1 ps_ty1 ty2 _
        ; new_ev <- rewriteEqEvidence ev swapped new_lhs new_rhs lhs_co rhs_co
 
        ; dflags <- getDynFlags
-       ; canEqTyVar2 dflags new_ev eq_rel IsSwapped tv2 (ps_ty1 `mkCastTy` sym_co2) }
+       ; canEqTyVar2 dflags new_ev eq_rel IsSwapped tv2 (ps_xi1 `mkCastTy` sym_co2) }
 
-canEqTyVarHomo ev eq_rel swapped tv1 _ _ ps_ty2
+canEqTyVarHomo ev eq_rel swapped tv1 _ _ ps_xi2
   = do { dflags <- getDynFlags
-       ; canEqTyVar2 dflags ev eq_rel swapped tv1 ps_ty2 }
+       ; canEqTyVar2 dflags ev eq_rel swapped tv1 ps_xi2 }
 
 -- The RHS here is either not a casted tyvar, or it's a tyvar but we want
 -- to rewrite the LHS to the RHS (as per swapOverTyVars)
@@ -2011,7 +2014,7 @@ canEqTyVar2 :: DynFlags
             -> EqRel
             -> SwapFlag
             -> TcTyVar                  -- lhs = tv, flat
-            -> TcType                   -- rhs
+            -> TcType                   -- rhs, flat
             -> TcS (StopOrContinue Ct)
 -- LHS is an inert type variable,
 -- and RHS is fully rewritten, but with type synonyms
@@ -2186,7 +2189,7 @@ However, if we encounter an equality constraint with a type synonym
 application on one side and a variable on the other side, we should
 NOT (necessarily) expand the type synonym, since for the purpose of
 good error messages we want to leave type synonyms unexpanded as much
-as possible.  Hence the ps_ty1, ps_ty2 argument passed to canEqTyVar.
+as possible.  Hence the ps_xi1, ps_xi2 argument passed to canEqTyVar.
 
 -}
 
index 69ced0b..5cc2f89 100644 (file)
@@ -3,6 +3,7 @@
 module TcFlatten(
    FlattenMode(..),
    flatten, flattenKind, flattenArgsNom,
+   rewriteTyVar,
 
    unflattenWanteds
  ) where
@@ -456,7 +457,8 @@ type FlatWorkListRef = TcRef [Ct]  -- See Note [The flattening work list]
 
 data FlattenEnv
   = FE { fe_mode    :: !FlattenMode
-       , fe_loc     :: !CtLoc             -- See Note [Flattener CtLoc]
+       , fe_loc     :: CtLoc              -- See Note [Flattener CtLoc]
+                      -- unbanged because it's bogus in rewriteTyVar
        , fe_flavour :: !CtFlavour
        , fe_eq_rel  :: !EqRel             -- See Note [Flattener EqRels]
        , fe_work    :: !FlatWorkListRef } -- See Note [The flattening work list]
@@ -520,7 +522,8 @@ runFlatten :: FlattenMode -> CtLoc -> CtFlavour -> EqRel -> FlatM a -> TcS a
 runFlatten mode loc flav eq_rel thing_inside
   = do { flat_ref <- newTcRef []
        ; let fmode = FE { fe_mode = mode
-                        , fe_loc  = loc
+                        , fe_loc  = bumpCtLocDepth loc
+                            -- See Note [Flatten when discharging CFunEqCan]
                         , fe_flavour = flav
                         , fe_eq_rel = eq_rel
                         , fe_work = flat_ref }
@@ -743,8 +746,27 @@ changes the flavour from Derived just for this purpose.
 *  They are all wrapped in runFlatten, so their                        *
 *  flattening work gets put into the work list                         *
 *                                                                      *
-********************************************************************* -}
+*********************************************************************
+
+Note [rewriteTyVar]
+~~~~~~~~~~~~~~~~~~~~~~
+Suppose we have an injective function F and
+  inert_funeqs:   F t1 ~ fsk1
+                  F t2 ~ fsk2
+  inert_eqs:      fsk1 ~ [a]
+                  a ~ Int
+                  fsk2 ~ [Int]
+
+We never rewrite the RHS (cc_fsk) of a CFunEqCan. But we /do/ want to get the
+[D] t1 ~ t2 from the injectiveness of F. So we flatten cc_fsk of CFunEqCans
+when trying to find derived equalities arising from injectivity.
+-}
 
+-- | See Note [Flattening].
+-- If (xi, co) <- flatten mode ev ty, then co :: xi ~r ty
+-- where r is the role in @ev@. If @mode@ is 'FM_FlattenAll',
+-- then 'xi' is almost function-free (Note [Almost function-free]
+-- in TcRnTypes).
 flatten :: FlattenMode -> CtEvidence -> TcType
         -> TcS (Xi, TcCoercion)
 flatten mode ev ty
@@ -753,8 +775,27 @@ flatten mode ev ty
        ; traceTcS "flatten }" (ppr ty')
        ; return (ty', co) }
 
+-- Apply the inert set as an *inert generalised substitution* to
+-- a variable, zonking along the way.
+-- See Note [inert_eqs: the inert equalities] in TcSMonad.
+-- Equivalently, this flattens the variable with respect to NomEq
+-- in a Derived constraint. (Why Derived? Because Derived allows the
+-- most about of rewriting.) Returns no coercion, because we're
+-- using Derived constraints.
+-- See Note [rewriteTyVar]
+rewriteTyVar :: TcTyVar -> TcS TcType
+rewriteTyVar tv
+  = do { traceTcS "rewriteTyVar {" (ppr tv)
+       ; (ty, _) <- runFlatten FM_SubstOnly fake_loc Derived NomEq $
+                    flattenTyVar tv
+       ; traceTcS "rewriteTyVar }" (ppr ty)
+       ; return ty }
+  where
+    fake_loc = pprPanic "rewriteTyVar used a CtLoc" (ppr tv)
+
 -- specialized to flattening kinds: never Derived, always Nominal
 -- See Note [No derived kind equalities]
+-- See Note [Flattening]
 flattenKind :: CtLoc -> CtFlavour -> TcType -> TcS (Xi, TcCoercionN)
 flattenKind loc flav ty
   = do { traceTcS "flattenKind {" (ppr flav <+> ppr ty)
@@ -765,6 +806,7 @@ flattenKind loc flav ty
        ; traceTcS "flattenKind }" (ppr ty' $$ ppr co) -- co is never a panic
        ; return (ty', co) }
 
+-- See Note [Flattening]
 flattenArgsNom :: CtEvidence -> TyCon -> [TcType] -> TcS ([Xi], [TcCoercion], TcCoercionN)
 -- Externally-callable, hence runFlatten
 -- Flatten a vector of types all at once; in fact they are
@@ -811,6 +853,9 @@ Flattening also:
   * zonks, removing any metavariables, and
   * applies the substitution embodied in the inert set
 
+The result of flattening is *almost function-free*. See
+Note [Almost function-free] in TcRnTypes.
+
 Because flattening zonks and the returned coercion ("co" above) is also
 zonked, it's possible that (co :: xi ~ ty) isn't quite true. So, instead,
 we can rely on this fact:
@@ -1575,7 +1620,7 @@ flatten_tyvar2 tv fr@(_, eq_rel)
                         , cc_rhs = rhs_ty, cc_eq_rel = ct_eq_rel } <- ct
              , let ct_fr = (ctEvFlavour ctev, ct_eq_rel)
              , ct_fr `eqCanRewriteFR` fr  -- This is THE key call of eqCanRewriteFR
-             ->  do { traceFlat "Following inert tyvar"
+             -> do { traceFlat "Following inert tyvar"
                         (ppr mode <+>
                          ppr tv <+>
                          equals <+>
index dbc564a..6b69928 100644 (file)
@@ -1343,59 +1343,61 @@ improveLocalFunEqs work_ev inerts fam_tc args fsk
     || not (isImprovable work_ev)
   = return ()
 
-  | not (null improvement_eqns)
-  = do { traceTcS "interactFunEq improvements: " $
-         vcat [ text "Eqns:" <+> ppr improvement_eqns
-              , text "Candidates:" <+> ppr funeqs_for_tc
-              , text "Inert eqs:" <+> ppr ieqs ]
-       ; emitFunDepDeriveds improvement_eqns }
-
   | otherwise
-  = return ()
+  = do { eqns <- improvement_eqns
+       ; if not (null eqns)
+         then do { traceTcS "interactFunEq improvements: " $
+                   vcat [ text "Eqns:" <+> ppr eqns
+                        , text "Candidates:" <+> ppr funeqs_for_tc
+                        , text "Inert eqs:" <+> ppr (inert_eqs inerts) ]
+                 ; emitFunDepDeriveds eqns }
+         else return () }
 
   where
-    ieqs          = inert_eqs inerts
     funeqs        = inert_funeqs inerts
     funeqs_for_tc = findFunEqsByTyCon funeqs fam_tc
-    rhs           = lookupFlattenTyVar ieqs fsk
     work_loc      = ctEvLoc work_ev
     work_pred     = ctEvPred work_ev
     fam_inj_info  = tyConInjectivityInfo fam_tc
 
     --------------------
-    improvement_eqns :: [FunDepEqn CtLoc]
+    improvement_eqns :: TcS [FunDepEqn CtLoc]
     improvement_eqns
       | Just ops <- isBuiltInSynFamTyCon_maybe fam_tc
       =    -- Try built-in families, notably for arithmethic
-         concatMap (do_one_built_in ops) funeqs_for_tc
+        do { rhs <- rewriteTyVar fsk
+           ; concatMapM (do_one_built_in ops rhs) funeqs_for_tc }
 
       | Injective injective_args <- fam_inj_info
       =    -- Try improvement from type families with injectivity annotations
-        concatMap (do_one_injective injective_args) funeqs_for_tc
+        do { rhs <- rewriteTyVar fsk
+           ; concatMapM (do_one_injective injective_args rhs) funeqs_for_tc }
 
       | otherwise
-      = []
+      = return []
 
     --------------------
-    do_one_built_in ops (CFunEqCan { cc_tyargs = iargs, cc_fsk = ifsk, cc_ev = inert_ev })
-      = mk_fd_eqns inert_ev (sfInteractInert ops args rhs iargs
-                                             (lookupFlattenTyVar ieqs ifsk))
+    do_one_built_in ops rhs (CFunEqCan { cc_tyargs = iargs, cc_fsk = ifsk, cc_ev = inert_ev })
+      = do { inert_rhs <- rewriteTyVar ifsk
+           ; return $ mk_fd_eqns inert_ev (sfInteractInert ops args rhs iargs inert_rhs) }
 
-    do_one_built_in _ _ = pprPanic "interactFunEq 1" (ppr fam_tc)
+    do_one_built_in _ _ = pprPanic "interactFunEq 1" (ppr fam_tc)
 
     --------------------
     -- See Note [Type inference for type families with injectivity]
-    do_one_injective inj_args (CFunEqCan { cc_tyargs = inert_args
-                                         , cc_fsk = ifsk, cc_ev = inert_ev })
+    do_one_injective inj_args rhs (CFunEqCan { cc_tyargs = inert_args
+                                             , cc_fsk = ifsk, cc_ev = inert_ev })
       | isImprovable inert_ev
-      , rhs `tcEqType` lookupFlattenTyVar ieqs ifsk
-      = mk_fd_eqns inert_ev $
-            [ Pair arg iarg
-            | (arg, iarg, True) <- zip3 args inert_args inj_args ]
+      = do { inert_rhs <- rewriteTyVar ifsk
+           ; return $ if rhs `tcEqType` inert_rhs
+                      then mk_fd_eqns inert_ev $
+                             [ Pair arg iarg
+                             | (arg, iarg, True) <- zip3 args inert_args inj_args ]
+                      else [] }
       | otherwise
-      = []
+      = return []
 
-    do_one_injective _ _ = pprPanic "interactFunEq 2" (ppr fam_tc)
+    do_one_injective _ _ = pprPanic "interactFunEq 2" (ppr fam_tc)
 
     --------------------
     mk_fd_eqns :: CtEvidence -> [TypeEqn] -> [FunDepEqn CtLoc]
@@ -1870,6 +1872,63 @@ See
  * Note [Evidence for quantified constraints] in Predicate
  * Note [Equality superclasses in quantified constraints]
    in TcCanonical
+
+Note [Flatten when discharging CFunEqCan]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+We have the following scenario (#16512):
+
+type family LV (as :: [Type]) (b :: Type) = (r :: Type) | r -> as b where
+  LV (a ': as) b = a -> LV as b
+
+[WD] w1 :: LV as0 (a -> b) ~ fmv1 (CFunEqCan)
+[WD] w2 :: fmv1 ~ (a -> fmv2) (CTyEqCan)
+[WD] w3 :: LV as0 b ~ fmv2 (CFunEqCan)
+
+We start with w1. Because LV is injective, we wish to see if the RHS of the
+equation matches the RHS of the CFunEqCan. The RHS of a CFunEqCan is always an
+fmv, so we "look through" to get (a -> fmv2). Then we run tcUnifyTyWithTFs.
+That performs the match, but it allows a type family application (such as the
+LV in the RHS of the equation) to match with anything. (See "Injective type
+families" by Stolarek et al., HS'15, Fig. 2) The matching succeeds, which
+means we can improve as0 (and b, but that's not interesting here). However,
+because the RHS of w1 can't see through fmv2 (we have no way of looking up a
+LHS of a CFunEqCan from its RHS, and this use case isn't compelling enough),
+we invent a new unification variable here. We thus get (as0 := a : as1).
+Rewriting:
+
+[WD] w1 :: LV (a : as1) (a -> b) ~ fmv1
+[WD] w2 :: fmv1 ~ (a -> fmv2)
+[WD] w3 :: LV (a : as1) b ~ fmv2
+
+We can now reduce both CFunEqCans, using the equation for LV. We get
+
+[WD] w2 :: (a -> LV as1 (a -> b)) ~ (a -> a -> LV as1 b)
+
+Now we decompose (and flatten) to
+
+[WD] w4 :: LV as1 (a -> b) ~ fmv3
+[WD] w5 :: fmv3 ~ (a -> fmv1)
+[WD] w6 :: LV as1 b ~ fmv4
+
+which is exactly where we started. These goals really are insoluble, but
+we would prefer not to loop. We thus need to find a way to bump the reduction
+depth, so that we can detect the loop and abort.
+
+The key observation is that we are performing a reduction. We thus wish
+to bump the level when discharging a CFunEqCan. Where does this bumped
+level go, though? It can't just go on the reduct, as that's a type. Instead,
+it must go on any CFunEqCans produced after flattening. We thus flatten
+when discharging, making sure that the level is bumped in the new
+fun-eqs. The flattening happens in reduce_top_fun_eq and the level
+is bumped when setting up the FlatM monad in TcFlatten.runFlatten.
+(This bumping will happen for call sites other than this one, but that
+makes sense -- any constraints emitted by the flattener are offshoots
+the work item and should have a higher level. We don't have any test
+cases that require the bumping in this other cases, but it's convenient
+and causes no harm to bump at every flatten.)
+
+Test case: typecheck/should_fail/T16512a
+
 -}
 
 --------------------
@@ -1898,6 +1957,7 @@ reduce_top_fun_eq :: CtEvidence -> TcTyVar -> (TcCoercion, TcType)
                   -> TcS (StopOrContinue Ct)
 -- We have found an applicable top-level axiom: use it to reduce
 -- Precondition: fsk is not free in rhs_ty
+-- ax_co :: F tys ~ rhs_ty, where F tys is the LHS of the old_ev
 reduce_top_fun_eq old_ev fsk (ax_co, rhs_ty)
   | not (isDerived old_ev)  -- Precondition of shortCutReduction
   , Just (tc, tc_args) <- tcSplitTyConApp_maybe rhs_ty
@@ -1912,7 +1972,11 @@ reduce_top_fun_eq old_ev fsk (ax_co, rhs_ty)
   = ASSERT2( not (fsk `elemVarSet` tyCoVarsOfType rhs_ty)
            , ppr old_ev $$ ppr rhs_ty )
            -- Guaranteed by Note [FunEq occurs-check principle]
-    do { dischargeFunEq old_ev fsk ax_co rhs_ty
+    do { (rhs_xi, flatten_co) <- flatten FM_FlattenAll old_ev rhs_ty
+             -- flatten_co :: rhs_xi ~ rhs_ty
+             -- See Note [Flatten when discharging CFunEqCan]
+       ; let total_co = ax_co `mkTcTransCo` mkTcSymCo flatten_co
+       ; dischargeFunEq old_ev fsk total_co rhs_xi
        ; traceTcS "doTopReactFunEq" $
          vcat [ text "old_ev:" <+> ppr old_ev
               , nest 2 (text ":=") <+> ppr ax_co ]
@@ -1926,16 +1990,16 @@ improveTopFunEqs ev fam_tc args fsk
   = return ()
 
   | otherwise
-  = do { ieqs <- getInertEqs
-       ; fam_envs <- getFamInstEnvs
-       ; eqns <- improve_top_fun_eqs fam_envs fam_tc args
-                                    (lookupFlattenTyVar ieqs fsk)
-       ; traceTcS "improveTopFunEqs" (vcat [ ppr fam_tc <+> ppr args <+> ppr fsk
+  = do { fam_envs <- getFamInstEnvs
+       ; rhs <- rewriteTyVar fsk
+       ; eqns <- improve_top_fun_eqs fam_envs fam_tc args rhs
+       ; traceTcS "improveTopFunEqs" (vcat [ ppr fam_tc <+> ppr args <+> ppr rhs
                                           , ppr eqns ])
        ; mapM_ (unifyDerived loc Nominal) eqns }
   where
-    loc = ctEvLoc ev  -- ToDo: this location is wrong; it should be FunDepOrigin2
-                      -- See #14778
+    loc = bumpCtLocDepth (ctEvLoc ev)
+        -- ToDo: this location is wrong; it should be FunDepOrigin2
+        -- See #14778
 
 improve_top_fun_eqs :: FamInstEnvs
                     -> TyCon -> [TcType] -> TcType
index e0dc5bc..d64a911 100644 (file)
@@ -1990,13 +1990,10 @@ zonkWCRec (WC { wc_simple = simple, wc_impl = implic })
        ; return (WC { wc_simple = simple', wc_impl = implic' }) }
 
 zonkSimples :: Cts -> TcM Cts
-zonkSimples cts = do { cts' <- mapBagM zonkCt' cts
+zonkSimples cts = do { cts' <- mapBagM zonkCt cts
                      ; traceTc "zonkSimples done:" (ppr cts')
                      ; return cts' }
 
-zonkCt' :: Ct -> TcM Ct
-zonkCt' ct = zonkCt ct
-
 {- Note [zonkCt behaviour]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~
 zonkCt tries to maintain the canonical form of a Ct.  For example,
@@ -2035,15 +2032,12 @@ zonkCt ct@(CDictCan { cc_ev = ev, cc_tyargs = args })
        ; args' <- mapM zonkTcType args
        ; return $ ct { cc_ev = ev', cc_tyargs = args' } }
 
-zonkCt ct@(CTyEqCan { cc_ev = ev, cc_tyvar = tv, cc_rhs = rhs })
-  = do { ev'    <- zonkCtEvidence ev
-       ; tv_ty' <- zonkTcTyVar tv
-       ; case getTyVar_maybe tv_ty' of
-           Just tv' -> do { rhs' <- zonkTcType rhs
-                          ; return ct { cc_ev    = ev'
-                                      , cc_tyvar = tv'
-                                      , cc_rhs   = rhs' } }
-           Nothing  -> return (mkNonCanonical ev') }
+zonkCt (CTyEqCan { cc_ev = ev })
+  = mkNonCanonical <$> zonkCtEvidence ev
+  -- CTyEqCan has some delicate invariants that may be violated by
+  -- zonking (documented with the Ct type) , so we don't want to create
+  -- a CTyEqCan here. Besides, this will be canonicalized again anyway,
+  -- so there is very little benefit in keeping the CTyEqCan constructor.
 
 zonkCt ct@(CIrredCan { cc_ev = ev }) -- Preserve the cc_insol flag
   = do { ev' <- zonkCtEvidence ev
index ca6022f..2d92564 100644 (file)
@@ -79,7 +79,7 @@ module TcSMonad (
 
     -- Inert CTyEqCans
     EqualCtList, findTyEqs, foldTyEqs, isInInertEqs,
-    lookupFlattenTyVar, lookupInertTyVar,
+    lookupInertTyVar,
 
     -- Inert solved dictionaries
     addSolvedDict, lookupSolvedDict,
@@ -233,7 +233,7 @@ It's very important to process equalities /first/:
 * (Kick-out) We want to apply this priority scheme to kicked-out
   constraints too (see the call to extendWorkListCt in kick_out_rewritable
   E.g. a CIrredCan can be a hetero-kinded (t1 ~ t2), which may become
-  homo-kinded when kicked out, and hence we want to priotitise it.
+  homo-kinded when kicked out, and hence we want to prioritise it.
 
 * (Derived equalities) Originally we tried to postpone processing
   Derived equalities, in the hope that we might never need to deal
@@ -257,6 +257,7 @@ So we arrange to put these particular class constraints in the wl_eqs.
   NB: since we do not currently apply the substitution to the
   inert_solved_dicts, the knot-tying still seems a bit fragile.
   But this makes it better.
+
 -}
 
 -- See Note [WorkList priorities]
@@ -763,8 +764,7 @@ The InertCans represents a collection of constraints with the following properti
     to the CTyEqCan equalities (modulo canRewrite of course;
     eg a wanted cannot rewrite a given)
 
-  * CTyEqCan equalities: see Note [Applying the inert substitution]
-                         in TcFlatten
+  * CTyEqCan equalities: see Note [inert_eqs: the inert equalities]
 
 Note [EqualCtList invariants]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
@@ -1519,25 +1519,6 @@ lookupInertTyVar ieqs tv
       Just (CTyEqCan { cc_rhs = rhs, cc_eq_rel = NomEq } : _ ) -> Just rhs
       _                                                        -> Nothing
 
-lookupFlattenTyVar :: InertEqs -> TcTyVar -> TcType
--- See Note [lookupFlattenTyVar]
-lookupFlattenTyVar ieqs ftv
-  = lookupInertTyVar ieqs ftv `orElse` mkTyVarTy ftv
-
-{- Note [lookupFlattenTyVar]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-Suppose we have an injective function F and
-  inert_funeqs:   F t1 ~ fsk1
-                  F t2 ~ fsk2
-  inert_eqs:      fsk1 ~ fsk2
-
-We never rewrite the RHS (cc_fsk) of a CFunEqCan.  But we /do/ want to
-get the [D] t1 ~ t2 from the injectiveness of F.  So we look up the
-cc_fsk of CFunEqCans in the inert_eqs when trying to find derived
-equalities arising from injectivity.
--}
-
-
 {- *********************************************************************
 *                                                                      *
                    Inert instances: inert_insts
@@ -1723,7 +1704,7 @@ kick_out_rewritable new_fr new_tv
 
     kicked_out :: WorkList
     -- NB: use extendWorkList to ensure that kicked-out equalities get priority
-    -- See Note [Prioritise equality constraints] (Kick-out).
+    -- See Note [Prioritise equalities] (Kick-out).
     -- The irreds may include non-canonical (hetero-kinded) equality
     -- constraints, which perhaps may have become soluble after new_tv
     -- is substituted; ditto the dictionaries, which may include (a~b)
@@ -3289,6 +3270,7 @@ dischargeFunEq :: CtEvidence -> TcTyVar -> TcCoercion -> TcType -> TcS ()
 --       - co :: F tys ~ xi
 --       - fmv/fsk `notElem` xi
 --       - fmv not filled (for Wanteds)
+--       - xi is flattened (and obeys Note [Almost function-free] in TcRnTypes)
 --
 -- Then for [W] or [WD], we actually fill in the fmv:
 --      set fmv := xi,
@@ -3568,11 +3550,12 @@ checkReductionDepth loc ty
          wrapErrTcS $
          solverDepthErrorTcS loc ty }
 
-matchFam :: TyCon -> [Type] -> TcS (Maybe (Coercion, TcType))
+matchFam :: TyCon -> [Type] -> TcS (Maybe (CoercionN, TcType))
+-- Given (F tys) return (ty, co), where co :: F tys ~N ty
 matchFam tycon args = wrapTcS $ matchFamTcM tycon args
 
-matchFamTcM :: TyCon -> [Type] -> TcM (Maybe (Coercion, TcType))
--- Given (F tys) return (ty, co), where co :: F tys ~ ty
+matchFamTcM :: TyCon -> [Type] -> TcM (Maybe (CoercionN, TcType))
+-- Given (F tys) return (ty, co), where co :: F tys ~N ty
 matchFamTcM tycon args
   = do { fam_envs <- FamInst.tcGetFamInstEnvs
        ; let match_fam_result
index c116e4f..e81e3e8 100644 (file)
@@ -81,7 +81,7 @@ module TcType (
   hasIPPred, isTauTy, isTauTyCon, tcIsTyVarTy, tcIsForAllTy,
   isPredTy, isTyVarClassPred, isTyVarHead, isInsolubleOccursCheck,
   checkValidClsArgs, hasTyVarHead,
-  isRigidTy,
+  isRigidTy, isAlmostFunctionFree,
 
   ---------------------------------
   -- Misc type manipulators
@@ -2057,6 +2057,24 @@ isRigidTy ty
   | isForAllTy ty                           = True
   | otherwise                               = False
 
+
+-- | Is this type *almost function-free*? See Note [Almost function-free]
+-- in TcRnTypes
+isAlmostFunctionFree :: TcType -> Bool
+isAlmostFunctionFree ty | Just ty' <- tcView ty = isAlmostFunctionFree ty'
+isAlmostFunctionFree (TyVarTy {})    = True
+isAlmostFunctionFree (AppTy ty1 ty2) = isAlmostFunctionFree ty1 &&
+                                       isAlmostFunctionFree ty2
+isAlmostFunctionFree (TyConApp tc args)
+  | isTypeFamilyTyCon tc = False
+  | otherwise            = all isAlmostFunctionFree args
+isAlmostFunctionFree (ForAllTy bndr _) = isAlmostFunctionFree (binderType bndr)
+isAlmostFunctionFree (FunTy _ ty1 ty2) = isAlmostFunctionFree ty1 &&
+                                         isAlmostFunctionFree ty2
+isAlmostFunctionFree (LitTy {})        = True
+isAlmostFunctionFree (CastTy ty _)     = isAlmostFunctionFree ty
+isAlmostFunctionFree (CoercionTy {})   = True
+
 {-
 ************************************************************************
 *                                                                      *
index e5d0f3c..ce9270c 100644 (file)
@@ -2027,11 +2027,12 @@ checkValidCoAxiom ax@(CoAxiom { co_ax_tc = fam_tc, co_ax_branches = branches })
      -- See Note [Verifying injectivity annotation] in FamInstEnv
     check_injectivity prev_branches cur_branch
       | Injective inj <- injectivity
-      = do { let conflicts =
+      = do { dflags <- getDynFlags
+           ; let conflicts =
                      fst $ foldl' (gather_conflicts inj prev_branches cur_branch)
                                  ([], 0) prev_branches
            ; mapM_ (\(err, span) -> setSrcSpan span $ addErr err)
-                   (makeInjectivityErrors ax cur_branch inj conflicts) }
+                   (makeInjectivityErrors dflags ax cur_branch inj conflicts) }
       | otherwise
       = return ()
 
@@ -2169,9 +2170,11 @@ checkFamPatBinders fam_tc qtvs pats rhs
        }
   where
     pat_tvs     = tyCoVarsOfTypes pats
-    inj_pat_tvs = fvVarSet $ injectiveVarsOfTypes pats
+    inj_pat_tvs = fvVarSet $ injectiveVarsOfTypes False pats
       -- The type variables that are in injective positions.
       -- See Note [Dodgy binding sites in type family instances]
+      -- NB: The False above is irrelevant, as we never have type families in
+      -- patterns.
       --
       -- NB: It's OK to use the nondeterministic `fvVarSet` function here,
       -- since the order of `inj_pat_tvs` is never revealed in an error
index 992d5ec..7805bc8 100644 (file)
@@ -816,11 +816,11 @@ lookupFamInstEnvConflicts envs fam_inst@(FamInst { fi_axiom = new_axiom })
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 
 Injectivity means that the RHS of a type family uniquely determines the LHS (see
-Note [Type inference for type families with injectivity]).  User informs about
+Note [Type inference for type families with injectivity]).  The user informs us about
 injectivity using an injectivity annotation and it is GHC's task to verify that
-that annotation is correct wrt. to type family equations. Whenever we see a new
-equation of a type family we need to make sure that adding this equation to
-already known equations of a type family does not violate injectivity annotation
+this annotation is correct w.r.t. type family equations. Whenever we see a new
+equation of a type family we need to make sure that adding this equation to the
+already known equations of a type family does not violate the injectivity annotation
 supplied by the user (see Note [Injectivity annotation]).  Of course if the type
 family has no injectivity annotation then no check is required.  But if a type
 family has injectivity annotation we need to make sure that the following
@@ -888,11 +888,12 @@ conditions hold:
 3. If the RHS of a type family equation is a type family application then the type
    family is rejected as not injective. This is checked by FamInst.isTFHeaded.
 
-4. If a LHS type variable that is declared as injective is not mentioned on
+4. If a LHS type variable that is declared as injective is not mentioned in an
    injective position in the RHS then the type family is rejected as not
    injective.  "Injective position" means either an argument to a type
    constructor or argument to a type family on injective position.
-   This is checked by FamInst.unusedInjTvsInRHS.
+   There are subtleties here. See Note [Coverage condition for injective type families]
+   in FamInst.
 
 See also Note [Injective type families] in TyCon
 -}
index b5d482c..19371df 100644 (file)
@@ -14,6 +14,7 @@ module TyCoFVs
         tyCoVarsOfCoList, tyCoVarsOfProv,
         almostDevoidCoVarOfCo,
         injectiveVarsOfType, injectiveVarsOfTypes,
+        invisibleVarsOfType, invisibleVarsOfTypes,
 
         noFreeVarsOfType, noFreeVarsOfTypes, noFreeVarsOfCo,
 
@@ -26,7 +27,7 @@ module TyCoFVs
 
 import GhcPrelude
 
-import {-# SOURCE #-} Type (coreView, tcView)
+import {-# SOURCE #-} Type (coreView, tcView, partitionInvisibleTypes)
 
 import TyCoRep
 import TyCon
@@ -632,8 +633,11 @@ almost_devoid_co_var_of_types (ty:tys) cv
 -- where @S1@ and @S2@ are arbitrary substitutions.
 --
 -- See @Note [When does a tycon application need an explicit kind signature?]@.
-injectiveVarsOfType :: Type -> FV
-injectiveVarsOfType = go
+injectiveVarsOfType :: Bool   -- ^ Should we look under injective type families?
+                              -- See Note [Coverage condition for injective type families]
+                              -- in FamInst.
+                    -> Type -> FV
+injectiveVarsOfType look_under_tfs = go
   where
     go ty                 | Just ty' <- coreView ty
                           = go ty'
@@ -642,15 +646,17 @@ injectiveVarsOfType = go
     go (FunTy _ ty1 ty2)  = go ty1 `unionFV` go ty2
     go (TyConApp tc tys)  =
       case tyConInjectivityInfo tc of
-        NotInjective  -> emptyFV
-        Injective inj -> mapUnionFV go $
-                         filterByList (inj ++ repeat True) tys
+        Injective inj
+          |  look_under_tfs || not (isTypeFamilyTyCon tc)
+          -> mapUnionFV go $
+             filterByList (inj ++ repeat True) tys
                          -- Oversaturated arguments to a tycon are
                          -- always injective, hence the repeat True
-    go (ForAllTy tvb ty) = tyCoFVsBndr tvb $ go ty
-    go LitTy{}           = emptyFV
-    go (CastTy ty _)     = go ty
-    go CoercionTy{}      = emptyFV
+        _ -> emptyFV
+    go (ForAllTy (Bndr tv _) ty) = go (tyVarKind tv) `unionFV` delFV tv (go ty)
+    go LitTy{}                   = emptyFV
+    go (CastTy ty _)             = go ty
+    go CoercionTy{}              = emptyFV
 
 -- | Returns the free variables of a 'Type' that are in injective positions.
 -- Specifically, it finds the free variables while:
@@ -662,8 +668,42 @@ injectiveVarsOfType = go
 -- * Ignoring the non-injective fields of a 'TyConApp'
 --
 -- See @Note [When does a tycon application need an explicit kind signature?]@.
-injectiveVarsOfTypes :: [Type] -> FV
-injectiveVarsOfTypes tys = mapUnionFV injectiveVarsOfType tys
+injectiveVarsOfTypes :: Bool -- ^ look under injective type families?
+                             -- See Note [Coverage condition for injective type families]
+                             -- in FamInst.
+                     -> [Type] -> FV
+injectiveVarsOfTypes look_under_tfs = mapUnionFV (injectiveVarsOfType look_under_tfs)
+
+
+------------- Invisible vars -----------------
+-- | Returns the set of variables that are used invisibly anywhere within
+-- the given type. A variable will be included even if it is used both visibly
+-- and invisibly. An invisible use site includes:
+--   * In the kind of a variable
+--   * In the kind of a bound variable in a forall
+--   * In a coercion
+--   * In a Specified or Inferred argument to a function
+-- See Note [VarBndrs, TyCoVarBinders, TyConBinders, and visibility] in TyCoRep
+invisibleVarsOfType :: Type -> FV
+invisibleVarsOfType = go
+  where
+    go ty                 | Just ty' <- coreView ty
+                          = go ty'
+    go (TyVarTy v)        = go (tyVarKind v)
+    go (AppTy f a)        = go f `unionFV` go a
+    go (FunTy _ ty1 ty2)  = go ty1 `unionFV` go ty2
+    go (TyConApp tc tys)  = tyCoFVsOfTypes invisibles `unionFV`
+                            invisibleVarsOfTypes visibles
+      where (invisibles, visibles) = partitionInvisibleTypes tc tys
+    go (ForAllTy tvb ty)  = tyCoFVsBndr tvb $ go ty
+    go LitTy{}            = emptyFV
+    go (CastTy ty co)     = tyCoFVsOfCo co `unionFV` go ty
+    go (CoercionTy co)    = tyCoFVsOfCo co
+
+-- | Like 'invisibleVarsOfType', but for many types.
+invisibleVarsOfTypes :: [Type] -> FV
+invisibleVarsOfTypes = mapUnionFV invisibleVarsOfType
+
 
 ------------- No free vars -----------------
 
index fe43ae4..1dfde74 100644 (file)
@@ -299,10 +299,9 @@ pprTypeApp tc tys
 ------------------
 -- | Display all kind information (with @-fprint-explicit-kinds@) when the
 -- provided 'Bool' argument is 'True'.
--- See @Note [Kind arguments in error messages]@ in "TcErrors".
+-- See @Note [Kind arguments in error messages]@ in TcErrors.
 pprWithExplicitKindsWhen :: Bool -> SDoc -> SDoc
 pprWithExplicitKindsWhen b
   = updSDocDynFlags $ \dflags ->
       if b then gopt_set dflags Opt_PrintExplicitKinds
            else dflags
-
index 51c3679..8bf7245 100644 (file)
@@ -2859,9 +2859,11 @@ tyConAppNeedsKindSig spec_inj_pos tc n_args
     injective_vars_of_binder :: TyConBinder -> FV
     injective_vars_of_binder (Bndr tv vis) =
       case vis of
-        AnonTCB VisArg -> injectiveVarsOfType (varType tv)
+        AnonTCB VisArg -> injectiveVarsOfType False -- conservative choice
+                                              (varType tv)
         NamedTCB argf  | source_of_injectivity argf
-                       -> unitFV tv `unionFV` injectiveVarsOfType (varType tv)
+                       -> unitFV tv `unionFV`
+                          injectiveVarsOfType False (varType tv)
         _              -> emptyFV
 
     source_of_injectivity Required  = True
index 4e2a498..446c9d9 100644 (file)
@@ -20,3 +20,5 @@ coreView :: Type -> Maybe Type
 tcView :: Type -> Maybe Type
 
 splitTyConApp_maybe :: HasDebugCallStack => Type -> Maybe (TyCon, [Type])
+
+partitionInvisibleTypes :: TyCon -> [Type] -> ([Type], [Type])
index 3b052f1..e77e755 100644 (file)
@@ -389,13 +389,18 @@ tcUnifyTyWithTFs twoWay t1 t2
   = case tc_unify_tys (const BindMe) twoWay True False
                        rn_env emptyTvSubstEnv emptyCvSubstEnv
                        [t1] [t2] of
-      Unifiable  (subst, _) -> Just $ niFixTCvSubst subst
-      MaybeApart (subst, _) -> Just $ niFixTCvSubst subst
+      Unifiable  (subst, _) -> Just $ maybe_fix subst
+      MaybeApart (subst, _) -> Just $ maybe_fix subst
       -- we want to *succeed* in questionable cases. This is a
       -- pre-unification algorithm.
       SurelyApart      -> Nothing
   where
-    rn_env = mkRnEnv2 $ mkInScopeSet $ tyCoVarsOfTypes [t1, t2]
+    in_scope = mkInScopeSet $ tyCoVarsOfTypes [t1, t2]
+    rn_env   = mkRnEnv2 in_scope
+
+    maybe_fix | twoWay    = niFixTCvSubst
+              | otherwise = mkTvSubst in_scope -- when matching, don't confuse
+                                               -- domain with range
 
 -----------------
 tcUnifyTys :: (TyCoVar -> BindFlag)
index d6cea5c..c484ba9 100644 (file)
@@ -387,7 +387,7 @@ filterByLists _          _      _      = []
 -- to 'True' go to the left; elements corresponding to 'False' go to the right.
 -- For example, @partitionByList [True, False, True] [1,2,3] == ([1,3], [2])@
 -- This function does not check whether the lists have equal
--- length.
+-- length; when one list runs out, the function stops.
 partitionByList :: [Bool] -> [a] -> ([a], [a])
 partitionByList = go [] []
   where
index 142509a..5963049 100644 (file)
@@ -8713,16 +8713,16 @@ Haskell <http://ics.p.lodz.pl/~stolarek/_media/pl:research:stolarek_peyton-jones
 Syntax of injectivity annotation
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 
-Injectivity annotation is added after type family head and consists of
+The injectivity annotation is added after the type family head and consists of
 two parts:
 
 -  a type variable that names the result of a type family. Syntax:
-   ``= tyvar`` or ``= (tyvar :: kind)``. Type variable must be fresh.
+   ``= tyvar`` or ``= (tyvar :: kind)``. The type variable must be fresh.
 
 -  an injectivity annotation of the form ``| A -> B``, where ``A`` is the
    result type variable (see previous bullet) and ``B`` is a list of
    argument type and kind variables in which type family is injective.
-   It is possible to omit some variables if type family is not injective
+   It is possible to omit some variables if the type family is not injective
    in them.
 
 Examples: ::
@@ -8738,15 +8738,15 @@ interpreted as associated type synonym default.
 
 .. _injective-ty-fams-typecheck:
 
-Verifying injectivity annotation against type family equations
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Verifying the injectivity annotation against type family equations
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 
 Once the user declares type family to be injective GHC must verify that
-this declaration is correct, ie. type family equations don't violate the
+this declaration is correct, i.e., that type family equations don't violate the
 injectivity annotation. A general idea is that if at least one equation
 (bullets (1), (2) and (3) below) or a pair of equations (bullets (4) and
 (5) below) violates the injectivity annotation then a type family is not
-injective in a way user claims and an error is reported. In the bullets
+injective in a way the user claims and an error is reported. In the bullets
 below *RHS* refers to the right-hand side of the type family equation
 being checked for injectivity. *LHS* refers to the arguments of that
 type family equation. Below are the rules followed when checking
@@ -8765,7 +8765,10 @@ injectivity of a type family:
    on injective position
    in the RHS GHC reports that the type family is not injective.
    Injective position means either argument to a type constructor or
-   injective argument to a type family.
+   injective argument to a type family. Type inference can potentially
+   loop when looking under injective type families in the RHS, so this
+   requires :extension:`UndecidableInstances`; GHC suggests enabling
+   the flag when it is necessary.
 
 4. *Open type families* Open type families are typechecked
    incrementally. This means that when a module is imported type family
index c6698d2..b171221 100644 (file)
 
 <interactive>:55:41: error:
     Type family equation violates injectivity annotation.
-    Kind variable ‘k1’ cannot be inferred from the right-hand side.
+    Type/kind variable ‘k1’
+    cannot be inferred from the right-hand side.
     In the type family equation:
       PolyKindVarsF @{[k1]} @[k2] ('[] @k1) = '[] @k2
         -- Defined at <interactive>:55:41
 
 <interactive>:60:15: error:
     Type family equation violates injectivity annotation.
-    Kind variable ‘k1’ cannot be inferred from the right-hand side.
+    Type/kind variable ‘k1’
+    cannot be inferred from the right-hand side.
     In the type family equation:
       PolyKindVars @[k1] @[k2] ('[] @k1) = '[] @k2
         -- Defined at <interactive>:60:15
 
 <interactive>:64:15: error:
     Type family equation violates injectivity annotation.
-    Kind variable ‘k’ cannot be inferred from the right-hand side.
+    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 and kind variables ‘k’, ‘a’, ‘b’
+    Type/kind variables ‘k’, ‘a’, ‘b’
     cannot be inferred from the right-hand side.
     In the type family equation:
       forall k (a :: k) (b :: k).
index 7779942..db976d6 100644 (file)
@@ -1,6 +1,7 @@
 {-# LANGUAGE TypeFamilyDependencies #-}
 {-# LANGUAGE FlexibleInstances #-}
 {-# LANGUAGE AllowAmbiguousTypes #-}
+{-# LANGUAGE UndecidableInstances #-}
 
 module T12522 where
 
index 7ed8ae1..a852109 100644 (file)
@@ -2,6 +2,7 @@
 {-# LANGUAGE KindSignatures #-}
 {-# LANGUAGE TypeFamilyDependencies #-}
 {-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE UndecidableInstances #-}
 
 module T12522b where
 
index 770f508..fc4cf8d 100644 (file)
@@ -1,4 +1,5 @@
 {-# LANGUAGE TypeFamilyDependencies #-}
+{-# LANGUAGE UndecidableInstances #-}
 
 module T13705 where
 
@@ -12,4 +13,3 @@ f _ = ()
 
 g :: D (F t) -> ()
 g x = f x
-
index e8b12c4..5188a8e 100644 (file)
@@ -2,6 +2,7 @@
 {-# LANGUAGE KindSignatures #-}
 {-# LANGUAGE TypeFamilyDependencies #-}
 {-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE UndecidableInstances #-}
 
 module T12522a where
 
@@ -20,4 +21,3 @@ def = undefined
 
 -- test :: Uncurried [Int, String] String
 test = def $ \n s -> I $ show n ++ s
-
index d3e3b66..c51b44f 100644 (file)
@@ -1,10 +1,10 @@
 
-T12522a.hs:22:26: error:
+T12522a.hs:23:26: error:
     • Ambiguous type variable ‘a0’ arising from a use of ‘show’
       prevents the constraint ‘(Show a0)’ from being solved.
       Relevant bindings include
-        n :: a0 (bound at T12522a.hs:22:15)
-        test :: Uncurried '[a0, [Char]] [Char] (bound at T12522a.hs:22:1)
+        n :: a0 (bound at T12522a.hs:23:15)
+        test :: Uncurried '[a0, [Char]] [Char] (bound at T12522a.hs:23:1)
       Probable fix: use a type annotation to specify what ‘a0’ should be.
       These potential instances exist:
         instance Show Ordering -- Defined in ‘GHC.Show’
index ef5166c..f96e10d 100644 (file)
@@ -6,6 +6,8 @@
 {-# LANGUAGE TypeFamilyDependencies #-}
 {-# LANGUAGE DataKinds, PolyKinds #-}
 {-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE UndecidableInstances #-}
+
 module T14369 where
 
 data family Sing (a :: k)
index 96e55d2..accd2d9 100644 (file)
@@ -1,9 +1,9 @@
 
-T14369.hs:27:5: error:
+T14369.hs:29:5: error:
     • Couldn't match type ‘Demote a’ with ‘Demote a1’
       Expected type: Sing x -> Maybe (Demote a1)
         Actual type: Sing x -> Demote (Maybe a)
     • In the expression: fromSing
       In an equation for ‘f’: f = fromSing
     • Relevant bindings include
-        f :: Sing x -> Maybe (Demote a1) (bound at T14369.hs:27:1)
+        f :: Sing x -> Maybe (Demote a1) (bound at T14369.hs:29:1)
index 65c78ae..e591fa9 100644 (file)
@@ -1,7 +1,7 @@
 
 T7788.hs:9:7: error:
     • Reduction stack overflow; size = 201
-      When simplifying the following type: F (Id (Fix Id))
+      When simplifying the following type: F (Fix Id)
       Use -freduction-depth=0 to disable this check
       (any upper bound you could choose might fail unpredictably with
        minor updates to GHC, so disabling the check is recommended if
index b62badd..2bd5c2a 100644 (file)
@@ -2,7 +2,7 @@
 T9554.hs:11:9: error:
     • Reduction stack overflow; size = 201
       When simplifying the following type:
-        F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F Bool)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
+        F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F Bool))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
       Use -freduction-depth=0 to disable this check
       (any upper bound you could choose might fail unpredictably with
        minor updates to GHC, so disabling the check is recommended if
@@ -13,7 +13,7 @@ T9554.hs:11:9: error:
 T9554.hs:13:17: error:
     • Reduction stack overflow; size = 201
       When simplifying the following type:
-        F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F Bool)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
+        F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F Bool))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
       Use -freduction-depth=0 to disable this check
       (any upper bound you could choose might fail unpredictably with
        minor updates to GHC, so disabling the check is recommended if
index 01857c3..abef2b1 100644 (file)
@@ -8,4 +8,4 @@ newtype Main.Foo2 (a_0 :: *)
 newtype Main.Foo3
   = Main.Foo3 (Data.Proxy.Proxy (Main.Foo3Fam2 GHC.Types.Int :: *))
 newtype Main.Foo4
-  = Main.Foo4 (Data.Proxy.Proxy (Main.Foo4Fam2 GHC.Types.Int))
+  = Main.Foo4 (Data.Proxy.Proxy (Main.Foo4Fam2 GHC.Types.Int :: *))
index 88c14c2..5c4d513 100644 (file)
@@ -1,5 +1,6 @@
 {-# LANGUAGE GADTs, TypeOperators, PolyKinds, DataKinds,
-             TypeFamilyDependencies, RankNTypes, LambdaCase, EmptyCase #-}
+             TypeFamilyDependencies, RankNTypes, LambdaCase, EmptyCase,
+             UndecidableInstances #-}
 
 module T13822 where
 
index 8605cec..e8a1943 100644 (file)
@@ -175,7 +175,7 @@ barapp2 :: Int
 barapp2 = bar 1
 
 -- Declarations below test more liberal RHSs of injectivity annotations:
--- permiting variables to appear in different order than the one in which they
+-- permitting variables to appear in different order than the one in which they
 -- were declared.
 type family H a b = r | r -> b a
 type family Hc a b = r | r -> b a where
diff --git a/testsuite/tests/typecheck/should_fail/T16512a.hs b/testsuite/tests/typecheck/should_fail/T16512a.hs
new file mode 100644 (file)
index 0000000..120fb00
--- /dev/null
@@ -0,0 +1,42 @@
+{-# LANGUAGE DataKinds              #-}
+{-# LANGUAGE GADTs                  #-}
+{-# LANGUAGE TypeFamilyDependencies #-}
+{-# LANGUAGE TypeOperators          #-}
+{-# LANGUAGE ViewPatterns           #-}
+{-# LANGUAGE UndecidableInstances   #-}
+
+module T16512a where
+
+import Data.Kind
+  ( Type )
+
+-- HOAS representation
+data AST (a :: Type) :: Type where
+  (:$) :: AST ( a -> b ) -> AST a -> AST b
+  -- Lam :: ( AST a -> AST b ) -> AST ( a -> b )
+  -- PrimOp :: PrimOp op a => AST a
+  -- ...
+
+data ASTs (as :: [Type]) :: Type where
+  NilASTs :: ASTs '[]
+  ConsAST :: AST a -> ASTs as -> ASTs (a ': as)
+
+type family ListVariadic (as :: [Type]) (b :: Type) = (r :: Type) | r -> as b where
+  ListVariadic (a ': as) b = a -> ListVariadic as b
+  -- ListVariadic '[] ()     = ()
+  -- ListVariadic '[] Bool   = Bool
+  -- ListVariadic '[] Word   = Word
+  -- ListVariadic '[] Int    = Int
+  -- ListVariadic '[] Float  = Float
+  -- ListVariadic '[] Double = Double
+  -- ...
+
+data AnApplication b where
+  AnApplication :: AST (ListVariadic as b) -> ASTs as -> AnApplication b
+
+unapply :: AST b -> AnApplication b
+unapply (f :$ a)
+  = case unapply f of
+        AnApplication g as ->
+          AnApplication g (a `ConsAST` as)
+-- no other cases with this simplified AST
diff --git a/testsuite/tests/typecheck/should_fail/T16512a.stderr b/testsuite/tests/typecheck/should_fail/T16512a.stderr
new file mode 100644 (file)
index 0000000..f18e973
--- /dev/null
@@ -0,0 +1,12 @@
+
+T16512a.hs:41:25: error:
+    • Reduction stack overflow; size = 201
+      When simplifying the following type: ListVariadic as b
+      Use -freduction-depth=0 to disable this check
+      (any upper bound you could choose might fail unpredictably with
+       minor updates to GHC, so disabling the check is recommended if
+       you're sure that type checking should terminate)
+    • In the first argument of ‘AnApplication’, namely ‘g’
+      In the expression: AnApplication g (a `ConsAST` as)
+      In a case alternative:
+          AnApplication g as -> AnApplication g (a `ConsAST` as)
diff --git a/testsuite/tests/typecheck/should_fail/T16512b.hs b/testsuite/tests/typecheck/should_fail/T16512b.hs
new file mode 100644 (file)
index 0000000..ad2a824
--- /dev/null
@@ -0,0 +1,9 @@
+{-# LANGUAGE TypeFamilyDependencies #-}
+
+module T16512b where
+
+type family G a = r | r -> a where
+  G [a] = [G a]
+
+-- this needs -XUndecidableInstances.
+-- See Note [Coverage condition for injective type families] in FamInst
diff --git a/testsuite/tests/typecheck/should_fail/T16512b.stderr b/testsuite/tests/typecheck/should_fail/T16512b.stderr
new file mode 100644 (file)
index 0000000..82a3311
--- /dev/null
@@ -0,0 +1,9 @@
+
+T16512b.hs:6:3: error:
+    • Type family equation violates injectivity annotation.
+      Type variable ‘a’ cannot be inferred from the right-hand side.
+      Using UndecidableInstances might help
+      In the type family equation:
+        G [a] = [G a] -- Defined at T16512b.hs:6:3
+    • In the equations for closed type family ‘G’
+      In the type family declaration for ‘G’
index 84af180..8fb124a 100644 (file)
@@ -59,28 +59,30 @@ T6018fail.hs:53:15: error:
 
 T6018fail.hs:61:10: error:
     Type family equation violates injectivity annotation.
-    Kind variable ‘k1’ cannot be inferred from the right-hand side.
+    Type/kind variable ‘k1’
+    cannot be inferred from the right-hand side.
     In the type family equation:
       PolyKindVarsF @{[k1]} @[k2] ('[] @k1) = '[] @k2
         -- Defined at T6018fail.hs:61:10
 
 T6018fail.hs:64:15: error:
     Type family equation violates injectivity annotation.
-    Kind variable ‘k1’ cannot be inferred from the right-hand side.
+    Type/kind variable ‘k1’
+    cannot be inferred from the right-hand side.
     In the type family equation:
       PolyKindVars @[k1] @[k2] ('[] @k1) = '[] @k2
         -- Defined at T6018fail.hs:64:15
 
 T6018fail.hs:68:15: error:
     Type family equation violates injectivity annotation.
-    Kind variable ‘k’ cannot be inferred from the right-hand side.
+    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 T6018fail.hs:68:15
 
 T6018fail.hs:72:15: error:
     Type family equation violates injectivity annotation.
-    Type and kind variables ‘k’, ‘a’, ‘b’
+    Type/kind variables ‘k’, ‘a’, ‘b’
     cannot be inferred from the right-hand side.
     In the type family equation:
       forall k (a :: k) (b :: k).
@@ -136,7 +138,7 @@ T6018fail.hs:115:15: error:
 
 T6018fail.hs:120:15: error:
     Type family equation violates injectivity annotation.
-    Type and kind variables ‘k’, ‘c’
+    Type/kind variables ‘k’, ‘c’
     cannot be inferred from the right-hand side.
     In the type family equation:
       forall k a b (c :: k).
index 5c36a0d..adb2c9c 100644 (file)
@@ -24,7 +24,7 @@ T6018failclosed.hs:19:5: error:
 
 T6018failclosed.hs:25:5: error:
     • Type family equation violates injectivity annotation.
-      Type and kind variables ‘k1’, ‘b’
+      Type/kind variables ‘k1’, ‘b’
       cannot be inferred from the right-hand side.
       In the type family equation:
         forall k1 k2 (b :: k1) (c :: k2).
@@ -87,7 +87,7 @@ T6018failclosed.hs:61:3: error:
 
 T6018failclosed.hs:66:5: error:
     • Type family equation violates injectivity annotation.
-      Kind variable ‘k’ cannot be inferred from the right-hand side.
+      Type/kind variable ‘k’ cannot be inferred from the right-hand side.
       In the type family equation:
         forall k (a :: k) (b :: k).
           Gc @k a b = Int -- Defined at T6018failclosed.hs:66:5
index 18e94f7..3f8dfc0 100644 (file)
@@ -543,5 +543,7 @@ test('UnliftedNewtypesMismatchedKindRecord', normal, compile_fail, [''])
 test('UnliftedNewtypesMultiFieldGadt', normal, compile_fail, [''])
 test('T13834', normal, compile_fail, [''])
 test('T17077', normal, compile_fail, [''])
+test('T16512a', normal, compile_fail, [''])
+test('T16512b', normal, compile_fail, [''])
 test('T17213', [extra_files(['T17213a.hs'])], multimod_compile_fail, ['T17213', '-v0'])
 test('T17355', normal, compile_fail, [''])