Re-engineer Given flatten-skolems
authorSimon Peyton Jones <simonpj@microsoft.com>
Fri, 26 May 2017 08:31:38 +0000 (09:31 +0100)
committerSimon Peyton Jones <simonpj@microsoft.com>
Fri, 26 May 2017 08:32:29 +0000 (09:32 +0100)
The big change here is to fix an outright bug in flattening of Givens,
albeit one that is very hard to exhibit.  Suppose we have the constraint
    forall a. (a ~ F b) => ..., (forall c. ....(F b)...) ...

Then
 - we'll flatten the (F) b to a fsk, say  (F b ~ fsk1)
 - we'll rewrite the (F b) inside the inner implication to 'fsk1'
 - when we leave the outer constraint we are suppose to unflatten;
   but that fsk1 will still be there
 - if we re-simplify the entire outer implication, we'll re-flatten
   the Given (F b) to, say, (F b ~ fsk2)
Now we have two fsks standing for the same thing, and that is very
wrong.

Solution: make fsks behave more like fmvs:
 - A flatten-skolem is now a MetaTyVar, whose MetaInfo is FlatSkolTv
 - We "fill in" that meta-tyvar when leaving the implication
 - The old FlatSkol form of TcTyVarDetails is gone completely
 - We track the flatten-skolems for the current implication in
   a new field of InertSet, inert_fsks.

See Note [The flattening story] in TcFlatten.

In doing this I found various other things to fix:

* I removed the zonkSimples from TcFlatten.unflattenWanteds; it wasn't
  needed.   But I added one in TcSimplify.floatEqualities, which does
  the zonk precisely when it is needed.

* Trac #13674 showed up a case where we had
     - an insoluble Given,   e.g.  a ~ [a]
     - the same insoluble Wanted   a ~ [a]
  We don't use the Given to rewwrite the Wanted (obviously), but
  we therefore ended up reporting
      Can't deduce (a ~ [a]) from (a ~ [a])
  which is silly.

  Conclusion: when reporting errors, make the occurs check "win"
  See Note [Occurs check wins] in TcErrors

26 files changed:
compiler/typecheck/TcCanonical.hs
compiler/typecheck/TcErrors.hs
compiler/typecheck/TcFlatten.hs
compiler/typecheck/TcHsSyn.hs
compiler/typecheck/TcInteract.hs
compiler/typecheck/TcMType.hs
compiler/typecheck/TcRnTypes.hs
compiler/typecheck/TcSMonad.hs
compiler/typecheck/TcSimplify.hs
compiler/typecheck/TcType.hs
compiler/typecheck/TcUnify.hs
testsuite/tests/deriving/should_fail/T7148.stderr
testsuite/tests/gadt/T3169.stderr
testsuite/tests/gadt/T7558.stderr
testsuite/tests/indexed-types/should_fail/T13674.hs [new file with mode: 0644]
testsuite/tests/indexed-types/should_fail/T13674.stderr [new file with mode: 0644]
testsuite/tests/indexed-types/should_fail/T4272.stderr
testsuite/tests/indexed-types/should_fail/T9662.stderr
testsuite/tests/indexed-types/should_fail/all.T
testsuite/tests/typecheck/should_compile/FD3.stderr
testsuite/tests/typecheck/should_compile/T9834.stderr
testsuite/tests/typecheck/should_fail/mc19.stderr
testsuite/tests/typecheck/should_fail/mc21.stderr
testsuite/tests/typecheck/should_fail/mc22.stderr
testsuite/tests/typecheck/should_fail/tcfail191.stderr
testsuite/tests/typecheck/should_fail/tcfail193.stderr

index 5dddd5d..77bf63d 100644 (file)
@@ -1538,7 +1538,7 @@ Suppose we have  [G] Num (F [a])
 then we flatten to
      [G] Num fsk
      [G] F [a] ~ fsk
 then we flatten to
      [G] Num fsk
      [G] F [a] ~ fsk
-where fsk is a flatten-skolem (FlatSkol). Suppose we have
+where fsk is a flatten-skolem (FlatSkolTv). Suppose we have
       type instance F [a] = a
 then we'll reduce the second constraint to
      [G] a ~ fsk
       type instance F [a] = a
 then we'll reduce the second constraint to
      [G] a ~ fsk
index eacdbb6..c9e07fc 100644 (file)
@@ -1466,7 +1466,7 @@ mkEqErr1 ctxt ct   -- Wanted or derived;
                NomEq  -> empty
                ReprEq -> mkCoercibleExplanation rdr_env fam_envs ty1 ty2
        ; dflags <- getDynFlags
                NomEq  -> empty
                ReprEq -> mkCoercibleExplanation rdr_env fam_envs ty1 ty2
        ; dflags <- getDynFlags
-       ; traceTc "mkEqErr1" (ppr ct $$ pprCtOrigin (ctOrigin ct))
+       ; traceTc "mkEqErr1" (ppr ct $$ pprCtOrigin (ctOrigin ct) $$ ppr keep_going)
        ; let report = mconcat [important wanted_msg, important coercible_msg,
                                relevant_bindings binds_msg]
        ; if keep_going
        ; let report = mconcat [important wanted_msg, important coercible_msg,
                                relevant_bindings binds_msg]
        ; if keep_going
@@ -1604,15 +1604,21 @@ reportEqErr ctxt report ct oriented ty1 ty2
   where misMatch = important $ misMatchOrCND ctxt ct oriented ty1 ty2
         eqInfo = important $ mkEqInfoMsg ct ty1 ty2
 
   where misMatch = important $ misMatchOrCND ctxt ct oriented ty1 ty2
         eqInfo = important $ mkEqInfoMsg ct ty1 ty2
 
-mkTyVarEqErr :: DynFlags -> ReportErrCtxt -> Report -> Ct
+mkTyVarEqErr, mkTyVarEqErr'
+  :: DynFlags -> ReportErrCtxt -> Report -> Ct
              -> Maybe SwapFlag -> TcTyVar -> TcType -> TcM ErrMsg
 -- tv1 and ty2 are already tidied
 mkTyVarEqErr dflags ctxt report ct oriented tv1 ty2
              -> Maybe SwapFlag -> TcTyVar -> TcType -> TcM ErrMsg
 -- tv1 and ty2 are already tidied
 mkTyVarEqErr dflags ctxt report ct oriented tv1 ty2
-  | isUserSkolem ctxt tv1   -- ty2 won't be a meta-tyvar, or else the thing would
+  = do { traceTc "mkTyVarEqErr" (ppr ct $$ ppr tv1 $$ ppr ty2)
+       ; mkTyVarEqErr' dflags ctxt report ct oriented tv1 ty2 }
+
+mkTyVarEqErr' dflags ctxt report ct oriented tv1 ty2
+  | not insoluble_occurs_check   -- See Note [Occurs check wins]
+  , isUserSkolem ctxt tv1   -- ty2 won't be a meta-tyvar, or else the thing would
                             -- be oriented the other way round;
                             -- see TcCanonical.canEqTyVarTyVar
                             -- be oriented the other way round;
                             -- see TcCanonical.canEqTyVarTyVar
-  || isSigTyVar tv1 && not (isTyVarTy ty2)
-  || ctEqRel ct == ReprEq && not insoluble_occurs_check
+    || isSigTyVar tv1 && not (isTyVarTy ty2)
+    || ctEqRel ct == ReprEq
      -- the cases below don't really apply to ReprEq (except occurs check)
   = mkErrorMsgFromCt ctxt ct $ mconcat
         [ important $ misMatchOrCND ctxt ct oriented ty1 ty2
      -- the cases below don't really apply to ReprEq (except occurs check)
   = mkErrorMsgFromCt ctxt ct $ mconcat
         [ important $ misMatchOrCND ctxt ct oriented ty1 ty2
@@ -1827,7 +1833,6 @@ extraTyVarInfo ctxt tv
   = ASSERT2( isTyVar tv, ppr tv )
     case tcTyVarDetails tv of
           SkolemTv {}   -> pprSkol implics tv
   = ASSERT2( isTyVar tv, ppr tv )
     case tcTyVarDetails tv of
           SkolemTv {}   -> pprSkol implics tv
-          FlatSkol {}   -> pp_tv <+> text "is a flattening type variable"
           RuntimeUnk {} -> pp_tv <+> text "is an interactive-debugger skolem"
           MetaTv {}     -> empty
   where
           RuntimeUnk {} -> pp_tv <+> text "is an interactive-debugger skolem"
           MetaTv {}     -> empty
   where
@@ -2016,7 +2021,22 @@ mkExpectedActualMsg ty1 ty2 (TypeEqOrigin { uo_actual = act
 
 mkExpectedActualMsg _ _ _ _ _ = panic "mkExpectedAcutalMsg"
 
 
 mkExpectedActualMsg _ _ _ _ _ = panic "mkExpectedAcutalMsg"
 
-{-
+{- Note [Insoluble occurs check wins]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Consider [G] a ~ [a],  [W] a ~ [a] (Trac #13674).  The Given is insoluble
+so we don't use it for rewriting.  The Wanted is also insoluble, and
+we don't solve it from the Given.  It's very confusing to say
+    Cannot solve a ~ [a] from given constraints a ~ [a]
+
+And indeed even thinking about the Givens is silly; [W] a ~ [a] is
+just as insoluble as Int ~ Bool.
+
+Conclusion: if there's an insoluble occurs check (isInsolubleOccursCheck)
+then report it first.
+
+(NB: there are potentially-soluble ones, like (a ~ F a b), and we don't
+wnat to be as draconian with them.)
+
 Note [Expanding type synonyms to make types similar]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 
 Note [Expanding type synonyms to make types similar]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 
index dc211c6..650cbd8 100644 (file)
@@ -4,7 +4,7 @@ module TcFlatten(
    FlattenMode(..),
    flatten, flattenManyNom,
 
    FlattenMode(..),
    flatten, flattenManyNom,
 
-   unflatten,
+   unflattenWanteds
  ) where
 
 #include "HsVersions.h"
  ) where
 
 #include "HsVersions.h"
@@ -36,31 +36,50 @@ import Control.Arrow ( first )
 Note [The flattening story]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 * A CFunEqCan is either of form
 Note [The flattening story]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 * A CFunEqCan is either of form
-     [G] <F xis> : F xis ~ fsk   -- fsk is a FlatSkol
-     [W]       x : F xis ~ fmv   -- fmv is a unification variable,
-                                 -- but untouchable,
-                                 -- with MetaInfo = FlatMetaTv
+     [G] <F xis> : F xis ~ fsk   -- fsk is a FlatSkolTv
+     [W]       x : F xis ~ fmv   -- fmv is a FlatMetaTv
   where
      x is the witness variable
   where
      x is the witness variable
-     fsk/fmv is a flatten skolem
      xis are function-free
      xis are function-free
-  CFunEqCans are always [Wanted], or [Given], never [Derived]
+     fsk/fmv is a flatten skolem;
+        it is always untouchable (level 0)
 
 
-  fmv untouchable just means that in a CTyVarEq, say,
-       fmv ~ Int
-  we do NOT unify fmv.
+* CFunEqCans can have any flavour: [G], [W], [WD] or [D]
 
 * KEY INSIGHTS:
 
    - A given flatten-skolem, fsk, is known a-priori to be equal to
 
 * KEY INSIGHTS:
 
    - A given flatten-skolem, fsk, is known a-priori to be equal to
-     F xis (the LHS), with <F xis> evidence
+     F xis (the LHS), with <F xis> evidence.  The fsk is still a
+     unification variable, but it is "owned" by its CFunEqCan, and
+     is filled in (unflattened) only by unflattenGivens.
 
    - A unification flatten-skolem, fmv, stands for the as-yet-unknown
 
    - A unification flatten-skolem, fmv, stands for the as-yet-unknown
-     type to which (F xis) will eventually reduce
+     type to which (F xis) will eventually reduce.  It is filled in
+     only by dischargeFmv.
 
 
-* Inert set invariant: if F xis1 ~ fsk1, F xis2 ~ fsk2
-                       then xis1 /= xis2
-  i.e. at most one CFunEqCan with a particular LHS
+   - All fsk/fmv variables are "untouchable".  To make it simple to test,
+     we simply give them TcLevel=0.  This means that in a CTyVarEq, say,
+       fmv ~ Int
+     we NEVER unify fmv.
+
+   - A unification flatten-skolems, fmv, ONLY gets unified when either
+       a) The CFunEqCan takes a step, using an axiom
+       b) By unflattenWanteds
+    They are never unified in any other form of equality.
+    For example [W] ffmv ~ Int  is stuck; it does not unify with fmv.
+
+* We *never* substitute in the RHS (i.e. the fsk/fmv) of a CFunEqCan.
+  That would destroy the invariant about the shape of a CFunEqCan,
+  and it would risk wanted/wanted interactions. The only way we
+  learn information about fsk is when the CFunEqCan takes a step.
+
+  However we *do* substitute in the LHS of a CFunEqCan (else it
+  would never get to fire!)
+
+* Unflattening:
+   - We unflatten Givens when leaving their scope (see unflattenGivens)
+   - We unflatten Wanteds at the end of each attempt to simplify the
+     wanteds; see unflattenWanteds, called from solveSimpleWanteds.
 
 * Each canonical [G], [W], or [WD] CFunEqCan x : F xis ~ fsk/fmv
   has its own distinct evidence variable x and flatten-skolem fsk/fmv.
 
 * Each canonical [G], [W], or [WD] CFunEqCan x : F xis ~ fsk/fmv
   has its own distinct evidence variable x and flatten-skolem fsk/fmv.
@@ -70,7 +89,11 @@ Note [The flattening story]
   In contrast a [D] CFunEqCan shares its fmv with its partner [W],
   but does not "own" it.  If we reduce a [D] F Int ~ fmv, where
   say type instance F Int = ty, then we don't discharge fmv := ty.
   In contrast a [D] CFunEqCan shares its fmv with its partner [W],
   but does not "own" it.  If we reduce a [D] F Int ~ fmv, where
   say type instance F Int = ty, then we don't discharge fmv := ty.
-  Rather we simply generate [D] fmv ~ ty
+  Rather we simply generate [D] fmv ~ ty (in TcInteract.reduce_top_fun_eq)
+
+* Inert set invariant: if F xis1 ~ fsk1, F xis2 ~ fsk2
+                       then xis1 /= xis2
+  i.e. at most one CFunEqCan with a particular LHS
 
 * Function applications can occur in the RHS of a CTyEqCan.  No reason
   not allow this, and it reduces the amount of flattening that must occur.
 
 * Function applications can occur in the RHS of a CTyEqCan.  No reason
   not allow this, and it reduces the amount of flattening that must occur.
@@ -104,20 +127,6 @@ Note [The flattening story]
     - Add new wanted to flat cache
     - Discharge x = F cos ; x2
 
     - Add new wanted to flat cache
     - Discharge x = F cos ; x2
 
-* Unification flatten-skolems, fmv, ONLY get unified when either
-    a) The CFunEqCan takes a step, using an axiom
-    b) During un-flattening
-  They are never unified in any other form of equality.
-  For example [W] ffmv ~ Int  is stuck; it does not unify with fmv.
-
-* We *never* substitute in the RHS (i.e. the fsk/fmv) of a CFunEqCan.
-  That would destroy the invariant about the shape of a CFunEqCan,
-  and it would risk wanted/wanted interactions. The only way we
-  learn information about fsk is when the CFunEqCan takes a step.
-
-  However we *do* substitute in the LHS of a CFunEqCan (else it
-  would never get to fire!)
-
 * [Interacting rule]
     (inert)     [W] x1 : F tys ~ fmv1
     (work item) [W] x2 : F tys ~ fmv2
 * [Interacting rule]
     (inert)     [W] x1 : F tys ~ fmv1
     (work item) [W] x2 : F tys ~ fmv2
@@ -1476,8 +1485,8 @@ flattens to
 We must solve both!
 -}
 
 We must solve both!
 -}
 
-unflatten :: Cts -> Cts -> TcS Cts
-unflatten tv_eqs funeqs
+unflattenWanteds :: Cts -> Cts -> TcS Cts
+unflattenWanteds tv_eqs funeqs
  = do { tclvl    <- getTcLevel
 
       ; traceTcS "Unflattening" $ braces $
  = do { tclvl    <- getTcLevel
 
       ; traceTcS "Unflattening" $ braces $
@@ -1506,10 +1515,7 @@ unflatten tv_eqs funeqs
       ; let all_flat = tv_eqs `andCts` funeqs
       ; traceTcS "Unflattening done" $ braces (pprCts all_flat)
 
       ; let all_flat = tv_eqs `andCts` funeqs
       ; traceTcS "Unflattening done" $ braces (pprCts all_flat)
 
-          -- Step 5: zonk the result
-          -- Motivation: makes them nice and ready for the next step
-          --             (see TcInteract.solveSimpleWanteds)
-      ; zonkSimples all_flat }
+      ; return all_flat }
   where
     ----------------
     unflatten_funeq :: Ct -> Cts -> TcS Cts
   where
     ----------------
     unflatten_funeq :: Ct -> Cts -> TcS Cts
index 1b9fed9..b75d59b 100644 (file)
@@ -1557,7 +1557,6 @@ zonkTyVarOcc env@(ZonkEnv zonk_unbound_tyvar tv_env _) tv
   = case tcTyVarDetails tv of
          SkolemTv {}    -> lookup_in_env
          RuntimeUnk {}  -> lookup_in_env
   = case tcTyVarDetails tv of
          SkolemTv {}    -> lookup_in_env
          RuntimeUnk {}  -> lookup_in_env
-         FlatSkol ty    -> zonkTcTypeToType env ty
          MetaTv { mtv_ref = ref }
            -> do { cts <- readMutVar ref
                  ; case cts of
          MetaTv { mtv_ref = ref }
            -> do { cts <- readMutVar ref
                  ; case cts of
index 4368fcb..83dc10c 100644 (file)
@@ -160,6 +160,7 @@ solveSimpleGivens givens
 solveSimpleWanteds :: Cts -> TcS WantedConstraints
 -- NB: 'simples' may contain /derived/ equalities, floated
 --     out from a nested implication. So don't discard deriveds!
 solveSimpleWanteds :: Cts -> TcS WantedConstraints
 -- NB: 'simples' may contain /derived/ equalities, floated
 --     out from a nested implication. So don't discard deriveds!
+-- The result is not necessarily zonked
 solveSimpleWanteds simples
   = do { traceTcS "solveSimpleWanteds {" (ppr simples)
        ; dflags <- getDynFlags
 solveSimpleWanteds simples
   = do { traceTcS "solveSimpleWanteds {" (ppr simples)
        ; dflags <- getDynFlags
@@ -199,12 +200,13 @@ solveSimpleWanteds simples
 solve_simple_wanteds :: WantedConstraints -> TcS (Int, WantedConstraints)
 -- Try solving these constraints
 -- Affects the unification state (of course) but not the inert set
 solve_simple_wanteds :: WantedConstraints -> TcS (Int, WantedConstraints)
 -- Try solving these constraints
 -- Affects the unification state (of course) but not the inert set
+-- The result is not necessarily zonked
 solve_simple_wanteds (WC { wc_simple = simples1, wc_insol = insols1, wc_impl = implics1 })
   = nestTcS $
     do { solveSimples simples1
        ; (implics2, tv_eqs, fun_eqs, insols2, others) <- getUnsolvedInerts
        ; (unif_count, unflattened_eqs) <- reportUnifications $
 solve_simple_wanteds (WC { wc_simple = simples1, wc_insol = insols1, wc_impl = implics1 })
   = nestTcS $
     do { solveSimples simples1
        ; (implics2, tv_eqs, fun_eqs, insols2, others) <- getUnsolvedInerts
        ; (unif_count, unflattened_eqs) <- reportUnifications $
-                                          unflatten tv_eqs fun_eqs
+                                          unflattenWanteds tv_eqs fun_eqs
             -- See Note [Unflatten after solving the simple wanteds]
        ; return ( unif_count
                 , WC { wc_simple = others `andCts` unflattened_eqs
             -- See Note [Unflatten after solving the simple wanteds]
        ; return ( unif_count
                 , WC { wc_simple = others `andCts` unflattened_eqs
@@ -2241,6 +2243,13 @@ Other notes:
      - natural numbers
      - Typeable
 
      - natural numbers
      - Typeable
 
+* Flatten-skolems: we do not treat a flatten-skolem as unifiable
+  for this purpose.
+  E.g.   f :: Eq (F a) => [a] -> [a]
+         f xs = ....(xs==xs).....
+  Here we get [W] Eq [a], and we don't want to refrain from solving
+  it because of the given (Eq (F a)) constraint!
+
 * The given-overlap problem is arguably not easy to appear in practice
   due to our aggressive prioritization of equality solving over other
   constraints, but it is possible. I've added a test case in
 * The given-overlap problem is arguably not easy to appear in practice
   due to our aggressive prioritization of equality solving over other
   constraints, but it is possible. I've added a test case in
@@ -2274,7 +2283,7 @@ Other notes:
   in point.
 
 All of this is disgustingly delicate, so to discourage people from writing
   in point.
 
 All of this is disgustingly delicate, so to discourage people from writing
-simplifiable class givens, we warn about signatures that contain them;#
+simplifiable class givens, we warn about signatures that contain them;
 see TcValidity Note [Simplifiable given constraints].
 -}
 
 see TcValidity Note [Simplifiable given constraints].
 -}
 
index 1ae9066..d26b257 100644 (file)
@@ -550,8 +550,13 @@ instSkolTyCoVarX mk_tcv subst tycovar
 newFskTyVar :: TcType -> TcM TcTyVar
 newFskTyVar fam_ty
   = do { uniq <- newUnique
 newFskTyVar :: TcType -> TcM TcTyVar
 newFskTyVar fam_ty
   = do { uniq <- newUnique
-       ; let name = mkSysTvName uniq (fsLit "fsk")
-       ; return (mkTcTyVar name (typeKind fam_ty) (FlatSkol fam_ty)) }
+       ; ref  <- newMutVar Flexi
+       ; let details = MetaTv { mtv_info  = FlatSkolTv
+                              , mtv_ref   = ref
+                              , mtv_tclvl = fmvTcLevel }
+             name = mkMetaTyVarName uniq (fsLit "fsk")
+       ; return (mkTcTyVar name (typeKind fam_ty) details) }
+
 {-
 Note [Kind substitution when instantiating]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 {-
 Note [Kind substitution when instantiating]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
@@ -593,10 +598,9 @@ newFmvTyVar :: TcType -> TcM TcTyVar
 newFmvTyVar fam_ty
   = do { uniq <- newUnique
        ; ref  <- newMutVar Flexi
 newFmvTyVar fam_ty
   = do { uniq <- newUnique
        ; ref  <- newMutVar Flexi
-       ; cur_lvl <- getTcLevel
        ; let details = MetaTv { mtv_info  = FlatMetaTv
                               , mtv_ref   = ref
        ; let details = MetaTv { mtv_info  = FlatMetaTv
                               , mtv_ref   = ref
-                              , mtv_tclvl = fmvTcLevel cur_lvl }
+                              , mtv_tclvl = fmvTcLevel }
              name = mkMetaTyVarName uniq (fsLit "s")
        ; return (mkTcTyVar name (typeKind fam_ty) details) }
 
              name = mkMetaTyVarName uniq (fsLit "s")
        ; return (mkTcTyVar name (typeKind fam_ty) details) }
 
@@ -707,7 +711,7 @@ writeMetaTyVarRef tyvar ref ty
     tv_lvl = tcTyVarLevel tyvar
     ty_lvl = tcTypeLevel ty
 
     tv_lvl = tcTyVarLevel tyvar
     ty_lvl = tcTypeLevel ty
 
-    level_check_ok = isFmvTyVar tyvar
+    level_check_ok = isFlattenTyVar tyvar
                   || not (ty_lvl `strictlyDeeperThan` tv_lvl)
     level_check_msg = ppr ty_lvl $$ ppr tv_lvl $$ ppr tyvar $$ ppr ty
 
                   || not (ty_lvl `strictlyDeeperThan` tv_lvl)
     level_check_msg = ppr ty_lvl $$ ppr tv_lvl $$ ppr tyvar $$ ppr ty
 
@@ -768,6 +772,7 @@ newAnonMetaTyVar meta_info kind
               s = case meta_info of
                         TauTv       -> fsLit "t"
                         FlatMetaTv  -> fsLit "fmv"
               s = case meta_info of
                         TauTv       -> fsLit "t"
                         FlatMetaTv  -> fsLit "fmv"
+                        FlatSkolTv  -> fsLit "fsk"
                         SigTv       -> fsLit "a"
         ; details <- newMetaDetails meta_info
         ; return (mkTcTyVar name kind details) }
                         SigTv       -> fsLit "a"
         ; details <- newMetaDetails meta_info
         ; return (mkTcTyVar name kind details) }
@@ -998,7 +1003,7 @@ zonkQuantifiedTyVar tv
 
       MetaTv {} -> skolemiseUnboundMetaTyVar tv
 
 
       MetaTv {} -> skolemiseUnboundMetaTyVar tv
 
-      _other -> pprPanic "zonkQuantifiedTyVar" (ppr tv) -- FlatSkol, RuntimeUnk
+      _other -> pprPanic "zonkQuantifiedTyVar" (ppr tv) -- RuntimeUnk
 
 defaultTyVar :: Bool      -- True <=> please default this kind variable to *
              -> TcTyVar   -- If it's a MetaTyVar then it is unbound
 
 defaultTyVar :: Bool      -- True <=> please default this kind variable to *
              -> TcTyVar   -- If it's a MetaTyVar then it is unbound
@@ -1490,7 +1495,6 @@ zonkTcTyVar tv
   = case tcTyVarDetails tv of
       SkolemTv {}   -> zonk_kind_and_return
       RuntimeUnk {} -> zonk_kind_and_return
   = case tcTyVarDetails tv of
       SkolemTv {}   -> zonk_kind_and_return
       RuntimeUnk {} -> zonk_kind_and_return
-      FlatSkol ty   -> zonkTcType ty
       MetaTv { mtv_ref = ref }
          -> do { cts <- readMutVar ref
                ; case cts of
       MetaTv { mtv_ref = ref }
          -> do { cts <- readMutVar ref
                ; case cts of
index e5e9eb2..e018d5d 100644 (file)
@@ -1589,8 +1589,8 @@ data Ct
         --    *never* over-saturated (because if so
         --    we should have decomposed)
 
         --    *never* over-saturated (because if so
         --    we should have decomposed)
 
-      cc_fsk    :: TcTyVar  -- [Given]  always a FlatSkol skolem
-                            -- [Wanted] always a FlatMetaTv unification variable
+      cc_fsk    :: TcTyVar  -- [Given]  always a FlatSkolTv
+                            -- [Wanted] always a FlatMetaTv
         -- See Note [The flattening story] in TcFlatten
     }
 
         -- See Note [The flattening story] in TcFlatten
     }
 
index f7153f8..434553d 100644 (file)
@@ -52,7 +52,7 @@ module TcSMonad (
     getNoGivenEqs, setInertCans,
     getInertEqs, getInertCans, getInertGivens,
     getInertInsols,
     getNoGivenEqs, setInertCans,
     getInertEqs, getInertCans, getInertGivens,
     getInertInsols,
-    emptyInert, getTcSInerts, setTcSInerts,
+    getTcSInerts, setTcSInerts,
     matchableGivens, prohibitedSuperClassSolve,
     getUnsolvedInerts,
     removeInertCts, getPendingScDicts,
     matchableGivens, prohibitedSuperClassSolve,
     getUnsolvedInerts,
     removeInertCts, getPendingScDicts,
@@ -383,6 +383,16 @@ data InertSet
               -- Canonical Given, Wanted, Derived
               -- Sometimes called "the inert set"
 
               -- Canonical Given, Wanted, Derived
               -- Sometimes called "the inert set"
 
+       , inert_fsks :: [(TcTyVar, TcType)]
+              -- A list of (fsk, ty) pairs; we add one element when we flatten
+              -- a function application in a Given constraint, creating
+              -- a new fsk in newFlattenSkolem.  When leaving a nested scope,
+              -- unflattenGivens unifies fsk := ty
+              --
+              -- We could also get this info from inert_funeqs, filtered by
+              -- level, but it seems simpler and more direct to capture the
+              -- fsk as we generate them.
+
        , inert_flat_cache :: ExactFunEqMap (TcCoercion, TcType, CtFlavour)
               -- See Note [Type family equations]
               -- If    F tys :-> (co, rhs, flav),
        , inert_flat_cache :: ExactFunEqMap (TcCoercion, TcType, CtFlavour)
               -- See Note [Type family equations]
               -- If    F tys :-> (co, rhs, flav),
@@ -421,6 +431,7 @@ emptyInert
                          , inert_irreds   = emptyCts
                          , inert_insols   = emptyCts }
        , inert_flat_cache    = emptyExactFunEqs
                          , inert_irreds   = emptyCts
                          , inert_insols   = emptyCts }
        , inert_flat_cache    = emptyExactFunEqs
+       , inert_fsks          = []
        , inert_solved_dicts  = emptyDictMap }
 
 
        , inert_solved_dicts  = emptyDictMap }
 
 
@@ -1814,24 +1825,21 @@ getNoGivenEqs :: TcLevel          -- TcLevel of this implication
 -- See Note [When does an implication have given equalities?]
 getNoGivenEqs tclvl skol_tvs
   = do { inerts@(IC { inert_eqs = ieqs, inert_irreds = iirreds
 -- See Note [When does an implication have given equalities?]
 getNoGivenEqs tclvl skol_tvs
   = do { inerts@(IC { inert_eqs = ieqs, inert_irreds = iirreds
-                    , inert_funeqs = funeqs
                     , inert_insols = insols })
               <- getInertCans
                     , inert_insols = insols })
               <- getInertCans
-       ; let local_fsks = foldFunEqs add_fsk funeqs emptyVarSet
-
-             has_given_eqs = foldrBag ((||) . ev_given_here . ctEvidence) False
+       ; let has_given_eqs = foldrBag ((||) . ev_given_here . ctEvidence) False
                                       (iirreds `unionBags` insols)
                                       (iirreds `unionBags` insols)
-                          || anyDVarEnv (eqs_given_here local_fsks) ieqs
+                          || anyDVarEnv eqs_given_here ieqs
 
        ; traceTcS "getNoGivenEqs" (vcat [ ppr has_given_eqs, ppr inerts
                                         , ppr insols])
        ; return (not has_given_eqs, insols) }
   where
 
        ; traceTcS "getNoGivenEqs" (vcat [ ppr has_given_eqs, ppr inerts
                                         , ppr insols])
        ; return (not has_given_eqs, insols) }
   where
-    eqs_given_here :: VarSet -> EqualCtList -> Bool
-    eqs_given_here local_fsks [CTyEqCan { cc_tyvar = tv, cc_ev = ev }]
+    eqs_given_here :: EqualCtList -> Bool
+    eqs_given_here [CTyEqCan { cc_tyvar = tv, cc_ev = ev }]
                               -- Givens are always a sigleton
                               -- Givens are always a sigleton
-      = not (skolem_bound_here local_fsks tv) && ev_given_here ev
-    eqs_given_here _ = False
+      = not (skolem_bound_here tv) && ev_given_here ev
+    eqs_given_here _ = False
 
     ev_given_here :: CtEvidence -> Bool
     -- True for a Given bound by the curent implication,
 
     ev_given_here :: CtEvidence -> Bool
     -- True for a Given bound by the curent implication,
@@ -1840,16 +1848,10 @@ getNoGivenEqs tclvl skol_tvs
       =  isGiven ev
       && tclvl == ctLocLevel (ctEvLoc ev)
 
       =  isGiven ev
       && tclvl == ctLocLevel (ctEvLoc ev)
 
-    add_fsk :: Ct -> VarSet -> VarSet
-    add_fsk ct fsks | CFunEqCan { cc_fsk = tv, cc_ev = ev } <- ct
-                    , isGiven ev = extendVarSet fsks tv
-                    | otherwise  = fsks
-
     skol_tv_set = mkVarSet skol_tvs
     skol_tv_set = mkVarSet skol_tvs
-    skolem_bound_here local_fsks tv -- See Note [Let-bound skolems]
+    skolem_bound_here tv -- See Note [Let-bound skolems]
       = case tcTyVarDetails tv of
           SkolemTv {} -> tv `elemVarSet` skol_tv_set
       = case tcTyVarDetails tv of
           SkolemTv {} -> tv `elemVarSet` skol_tv_set
-          FlatSkol {} -> not (tv `elemVarSet` local_fsks)
           _           -> False
 
 -- | Returns Given constraints that might,
           _           -> False
 
 -- | Returns Given constraints that might,
@@ -1889,9 +1891,11 @@ matchableGivens loc_w pred (IS { inert_cans = inert_cans })
     -- bindable when unifying with givens. That ensures that we
     -- conservatively assume that a meta tyvar might get unified with
     -- something that matches the 'given', until demonstrated
     -- bindable when unifying with givens. That ensures that we
     -- conservatively assume that a meta tyvar might get unified with
     -- something that matches the 'given', until demonstrated
-    -- otherwise.
-    bind_meta_tv tv | isMetaTyVar tv = BindMe
-                    | otherwise      = Skolem
+    -- otherwise.  More info in Note [Instance and Given overlap]
+    -- in TcInteract
+    bind_meta_tv tv | isMetaTyVar tv
+                    , not (isFskTyVar tv) = BindMe
+                    | otherwise           = Skolem
 
 prohibitedSuperClassSolve :: CtLoc -> CtLoc -> Bool
 -- See Note [Solving superclass constraints] in TcInstDcls
 
 prohibitedSuperClassSolve :: CtLoc -> CtLoc -> Bool
 -- See Note [Solving superclass constraints] in TcInstDcls
@@ -2413,6 +2417,8 @@ runTcSWithEvBinds ev_binds_var tcs
        ; when (count > 0) $
          csTraceTcM $ return (text "Constraint solver steps =" <+> int count)
 
        ; when (count > 0) $
          csTraceTcM $ return (text "Constraint solver steps =" <+> int count)
 
+       ; unflattenGivens inert_var
+
 #if defined(DEBUG)
        ; ev_binds <- TcM.getTcEvBindsMap ev_binds_var
        ; checkForCyclicBinds ev_binds
 #if defined(DEBUG)
        ; ev_binds <- TcM.getTcEvBindsMap ev_binds_var
        ; checkForCyclicBinds ev_binds
@@ -2420,6 +2426,7 @@ runTcSWithEvBinds ev_binds_var tcs
 
        ; return res }
 
 
        ; return res }
 
+----------------------------
 #if defined(DEBUG)
 checkForCyclicBinds :: EvBindMap -> TcM ()
 checkForCyclicBinds ev_binds_map
 #if defined(DEBUG)
 checkForCyclicBinds :: EvBindMap -> TcM ()
 checkForCyclicBinds ev_binds_map
@@ -2447,6 +2454,7 @@ checkForCyclicBinds ev_binds_map
             -- Note [Deterministic SCC] in Digraph.
 #endif
 
             -- Note [Deterministic SCC] in Digraph.
 #endif
 
+----------------------------
 setEvBindsTcS :: EvBindsVar -> TcS a -> TcS a
 setEvBindsTcS ref (TcS thing_inside)
  = TcS $ \ env -> thing_inside (env { tcs_ev_binds = ref })
 setEvBindsTcS :: EvBindsVar -> TcS a -> TcS a
 setEvBindsTcS ref (TcS thing_inside)
  = TcS $ \ env -> thing_inside (env { tcs_ev_binds = ref })
@@ -2460,8 +2468,9 @@ nestImplicTcS ref inner_tclvl (TcS thing_inside)
                    , tcs_count         = count
                    } ->
     do { inerts <- TcM.readTcRef old_inert_var
                    , tcs_count         = count
                    } ->
     do { inerts <- TcM.readTcRef old_inert_var
-       ; let nest_inert = inerts { inert_flat_cache = emptyExactFunEqs }
-                                     -- See Note [Do not inherit the flat cache]
+       ; let nest_inert = emptyInert { inert_cans         = inert_cans inerts
+                                     , inert_solved_dicts = inert_solved_dicts inerts }
+                          -- See Note [Do not inherit the flat cache]
        ; new_inert_var <- TcM.newTcRef nest_inert
        ; new_wl_var    <- TcM.newTcRef emptyWorkList
        ; let nest_env = TcSEnv { tcs_ev_binds      = ref
        ; new_inert_var <- TcM.newTcRef nest_inert
        ; new_wl_var    <- TcM.newTcRef emptyWorkList
        ; let nest_env = TcSEnv { tcs_ev_binds      = ref
@@ -2472,6 +2481,8 @@ nestImplicTcS ref inner_tclvl (TcS thing_inside)
        ; res <- TcM.setTcLevel inner_tclvl $
                 thing_inside nest_env
 
        ; res <- TcM.setTcLevel inner_tclvl $
                 thing_inside nest_env
 
+       ; unflattenGivens new_inert_var
+
 #if defined(DEBUG)
        -- Perform a check that the thing_inside did not cause cycles
        ; ev_binds <- TcM.getTcEvBindsMap ref
 #if defined(DEBUG)
        -- Perform a check that the thing_inside did not cause cycles
        ; ev_binds <- TcM.getTcEvBindsMap ref
@@ -2627,15 +2638,6 @@ unifyTyVar tv ty
        ; TcM.writeMetaTyVar tv ty
        ; TcM.updTcRef (tcs_unified env) (+1) }
 
        ; TcM.writeMetaTyVar tv ty
        ; TcM.updTcRef (tcs_unified env) (+1) }
 
-unflattenFmv :: TcTyVar -> TcType -> TcS ()
--- Fill a flatten-meta-var, simply by unifying it.
--- This does NOT count as a unification in tcs_unified.
-unflattenFmv tv ty
-  = ASSERT2( isMetaTyVar tv, ppr tv )
-    TcS $ \ _ ->
-    do { TcM.traceTc "unflattenFmv" (ppr tv <+> text ":=" <+> ppr ty)
-       ; TcM.writeMetaTyVar tv ty }
-
 reportUnifications :: TcS a -> TcS (Int, a)
 reportUnifications (TcS thing_inside)
   = TcS $ \ env ->
 reportUnifications :: TcS a -> TcS (Int, a)
 reportUnifications (TcS thing_inside)
   = TcS $ \ env ->
@@ -2790,8 +2792,12 @@ which will result in two Deriveds to end up in the insoluble set:
   wc_insols = (c ~ [c]) [D], (c ~ [c]) [D]
 -}
 
   wc_insols = (c ~ [c]) [D], (c ~ [c]) [D]
 -}
 
--- Flatten skolems
--- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+{- *********************************************************************
+*                                                                      *
+*                Flatten skolems                                       *
+*                                                                      *
+********************************************************************* -}
+
 newFlattenSkolem :: CtFlavour -> CtLoc
                  -> TyCon -> [TcType]                    -- F xis
                  -> TcS (CtEvidence, Coercion, TcTyVar)  -- [G/WD] x:: F xis ~ fsk
 newFlattenSkolem :: CtFlavour -> CtLoc
                  -> TyCon -> [TcType]                    -- F xis
                  -> TcS (CtEvidence, Coercion, TcTyVar)  -- [G/WD] x:: F xis ~ fsk
@@ -2806,9 +2812,14 @@ newFlattenSkolem flav loc tc xis
     new_skolem
       | Given <- flav
       = do { fsk <- wrapTcS (TcM.newFskTyVar fam_ty)
     new_skolem
       | Given <- flav
       = do { fsk <- wrapTcS (TcM.newFskTyVar fam_ty)
-           ; let co = mkNomReflCo fam_ty
-           ; ev  <- newGivenEvVar loc (mkPrimEqPred fam_ty (mkTyVarTy fsk),
-                                       EvCoercion co)
+
+           -- Extend the inert_fsks list, for use by unflattenGivens
+           ; updInertTcS $ \is -> is { inert_fsks = (fsk, fam_ty) : inert_fsks is }
+
+           -- Construct the Refl evidence
+           ; let pred = mkPrimEqPred fam_ty (mkTyVarTy fsk)
+                 co   = mkNomReflCo fam_ty
+           ; ev  <- newGivenEvVar loc (pred, EvCoercion co)
            ; return (ev, co, fsk) }
 
       | otherwise  -- Generate a [WD] for both Wanted and Derived
            ; return (ev, co, fsk) }
 
       | otherwise  -- Generate a [WD] for both Wanted and Derived
@@ -2817,6 +2828,25 @@ newFlattenSkolem flav loc tc xis
            ; (ev, hole_co) <- newWantedEq loc Nominal fam_ty (mkTyVarTy fmv)
            ; return (ev, hole_co, fmv) }
 
            ; (ev, hole_co) <- newWantedEq loc Nominal fam_ty (mkTyVarTy fmv)
            ; return (ev, hole_co, fmv) }
 
+----------------------------
+unflattenGivens :: IORef InertSet -> TcM ()
+-- Unflatten all the fsks created by flattening types in Given
+-- constraints We must be sure to do this, else we end up with
+-- flatten-skolems buried in any residual Wanteds
+--
+-- NB: this is the /only/ way that a fsk (MetaDetails = FlatSkolTv)
+--     is filled in. Nothing else does so.
+--
+-- It's here (rather than in TcFlatten) becuause the Right Places
+-- to call it are in runTcSWithEvBinds/nestImplicTcS, where it
+-- is nicely paired with the creation an empty inert_fsks list.
+unflattenGivens inert_var
+ = do { inerts <- TcM.readTcRef inert_var
+       ; mapM_ flatten_one (inert_fsks inerts) }
+  where
+    flatten_one (fsk, ty) = TcM.writeMetaTyVar fsk ty
+
+----------------------------
 extendFlatCache :: TyCon -> [Type] -> (TcCoercion, TcType, CtFlavour) -> TcS ()
 extendFlatCache tc xi_args stuff@(_, ty, fl)
   | isGivenOrWDeriv fl  -- Maintain the invariant that inert_flat_cache
 extendFlatCache :: TyCon -> [Type] -> (TcCoercion, TcType, CtFlavour) -> TcS ()
 extendFlatCache tc xi_args stuff@(_, ty, fl)
   | isGivenOrWDeriv fl  -- Maintain the invariant that inert_flat_cache
@@ -2832,6 +2862,33 @@ extendFlatCache tc xi_args stuff@(_, ty, fl)
   | otherwise
   = return ()
 
   | otherwise
   = return ()
 
+----------------------------
+unflattenFmv :: TcTyVar -> TcType -> TcS ()
+-- Fill a flatten-meta-var, simply by unifying it.
+-- This does NOT count as a unification in tcs_unified.
+unflattenFmv tv ty
+  = ASSERT2( isMetaTyVar tv, ppr tv )
+    TcS $ \ _ ->
+    do { TcM.traceTc "unflattenFmv" (ppr tv <+> text ":=" <+> ppr ty)
+       ; TcM.writeMetaTyVar tv ty }
+
+----------------------------
+demoteUnfilledFmv :: TcTyVar -> TcS ()
+-- If a flatten-meta-var is still un-filled,
+-- turn it into an ordinary meta-var
+demoteUnfilledFmv fmv
+  = wrapTcS $ do { is_filled <- TcM.isFilledMetaTyVar fmv
+                 ; unless is_filled $
+                   do { tv_ty <- TcM.newFlexiTyVarTy (tyVarKind fmv)
+                      ; TcM.writeMetaTyVar fmv tv_ty } }
+
+
+{- *********************************************************************
+*                                                                      *
+*                Instantaiation etc
+*                                                                      *
+********************************************************************* -}
+
 -- Instantiations
 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 
 -- Instantiations
 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 
@@ -2845,15 +2902,6 @@ newFlexiTcSTy knd = wrapTcS (TcM.newFlexiTyVarTy knd)
 cloneMetaTyVar :: TcTyVar -> TcS TcTyVar
 cloneMetaTyVar tv = wrapTcS (TcM.cloneMetaTyVar tv)
 
 cloneMetaTyVar :: TcTyVar -> TcS TcTyVar
 cloneMetaTyVar tv = wrapTcS (TcM.cloneMetaTyVar tv)
 
-demoteUnfilledFmv :: TcTyVar -> TcS ()
--- If a flatten-meta-var is still un-filled,
--- turn it into an ordinary meta-var
-demoteUnfilledFmv fmv
-  = wrapTcS $ do { is_filled <- TcM.isFilledMetaTyVar fmv
-                 ; unless is_filled $
-                   do { tv_ty <- TcM.newFlexiTyVarTy (tyVarKind fmv)
-                      ; TcM.writeMetaTyVar fmv tv_ty } }
-
 instFlexi :: [TKVar] -> TcS TCvSubst
 instFlexi = instFlexiX emptyTCvSubst
 
 instFlexi :: [TKVar] -> TcS TCvSubst
 instFlexi = instFlexiX emptyTCvSubst
 
index 557d40d..a611198 100644 (file)
@@ -615,8 +615,8 @@ simplifyInfer rhs_tclvl infer_mode sigs name_taus wanteds
                         psig_givens = mkGivens loc psig_theta_vars
                   ; _ <- solveSimpleGivens psig_givens
                          -- See Note [Add signature contexts as givens]
                         psig_givens = mkGivens loc psig_theta_vars
                   ; _ <- solveSimpleGivens psig_givens
                          -- See Note [Add signature contexts as givens]
-                  ; solveWanteds wanteds }
-       ; wanted_transformed_incl_derivs <- TcM.zonkWC wanted_transformed_incl_derivs
+                  ; wanteds' <- solveWanteds wanteds
+                  ; TcS.zonkWC wanteds' }
 
        -- Find quant_pred_candidates, the predicates that
        -- we'll consider quantifying over
 
        -- Find quant_pred_candidates, the predicates that
        -- we'll consider quantifying over
@@ -1953,20 +1953,29 @@ floatEqualities skols no_given_eqs
                 wanteds@(WC { wc_simple = simples })
   | not no_given_eqs  -- There are some given equalities, so don't float
   = return (emptyBag, wanteds)   -- Note [Float Equalities out of Implications]
                 wanteds@(WC { wc_simple = simples })
   | not no_given_eqs  -- There are some given equalities, so don't float
   = return (emptyBag, wanteds)   -- Note [Float Equalities out of Implications]
+
   | otherwise
   | otherwise
-  = do { outer_tclvl <- TcS.getTcLevel
+  = do { -- First zonk: the inert set (from whence they came) are is fully
+         -- zonked, but unflattening may have filled in unification
+         -- variables, and we /must/ see them.  Otherwise we may float
+         -- constraints that mention the skolems!
+         simples <- TcS.zonkSimples simples
+
+       -- Now we can pick the ones to float
+       ; let (float_eqs, remaining_simples) = partitionBag (usefulToFloat skol_set) simples
+             skol_set = mkVarSet skols
+
+       -- Promote any unification variables mentioned in the floated equalities
+       -- See Note [Promoting unification variables]
+       ; outer_tclvl <- TcS.getTcLevel
        ; mapM_ (promoteTyVarTcS outer_tclvl)
                (tyCoVarsOfCtsList float_eqs)
        ; mapM_ (promoteTyVarTcS outer_tclvl)
                (tyCoVarsOfCtsList float_eqs)
-           -- See Note [Promoting unification variables]
 
        ; traceTcS "floatEqualities" (vcat [ text "Skols =" <+> ppr skols
                                           , text "Simples =" <+> ppr simples
                                           , text "Floated eqs =" <+> ppr float_eqs])
        ; return ( float_eqs
                 , wanteds { wc_simple = remaining_simples } ) }
 
        ; traceTcS "floatEqualities" (vcat [ text "Skols =" <+> ppr skols
                                           , text "Simples =" <+> ppr simples
                                           , text "Floated eqs =" <+> ppr float_eqs])
        ; return ( float_eqs
                 , wanteds { wc_simple = remaining_simples } ) }
-  where
-    skol_set = mkVarSet skols
-    (float_eqs, remaining_simples) = partitionBag (usefulToFloat skol_set) simples
 
 usefulToFloat :: VarSet -> Ct -> Bool
 usefulToFloat skol_set ct   -- The constraint is un-flattened and de-canonicalised
 
 usefulToFloat :: VarSet -> Ct -> Bool
 usefulToFloat skol_set ct   -- The constraint is un-flattened and de-canonicalised
index bd72981..e22dfc3 100644 (file)
@@ -496,10 +496,6 @@ data TcTyVarDetails
                   --          when looking up instances
                   -- See Note [Binding when looking up instances] in InstEnv
 
                   --          when looking up instances
                   -- See Note [Binding when looking up instances] in InstEnv
 
-  | FlatSkol      -- A flatten-skolem.  It stands for the TcType, and zonking
-       TcType     -- will replace it by that type.
-                  -- See Note [The flattening story] in TcFlatten
-
   | RuntimeUnk    -- Stands for an as-yet-unknown type in the GHCi
                   -- interactive context
 
   | RuntimeUnk    -- Stands for an as-yet-unknown type in the GHCi
                   -- interactive context
 
@@ -523,21 +519,26 @@ data MetaInfo
                    -- never contains any ForAlls.
 
    | SigTv         -- A variant of TauTv, except that it should not be
                    -- never contains any ForAlls.
 
    | SigTv         -- A variant of TauTv, except that it should not be
-                   -- unified with a type, only with a type variable
+                   --   unified with a type, only with a type variable
                    -- See Note [Signature skolems]
 
    | FlatMetaTv    -- A flatten meta-tyvar
                    -- It is a meta-tyvar, but it is always untouchable, with level 0
                    -- See Note [The flattening story] in TcFlatten
 
                    -- See Note [Signature skolems]
 
    | FlatMetaTv    -- A flatten meta-tyvar
                    -- It is a meta-tyvar, but it is always untouchable, with level 0
                    -- See Note [The flattening story] in TcFlatten
 
+   | FlatSkolTv    -- A flatten skolem tyvar
+                   -- Just like FlatMetaTv, but is comletely "owned" by
+                   --   its Given CFunEqCan.
+                   -- It is filled in /only/ by unflattenGivens
+                   -- See Note [The flattening story] in TcFlatten
+
 instance Outputable MetaDetails where
   ppr Flexi         = text "Flexi"
   ppr (Indirect ty) = text "Indirect" <+> ppr ty
 
 pprTcTyVarDetails :: TcTyVarDetails -> SDoc
 -- For debugging
 instance Outputable MetaDetails where
   ppr Flexi         = text "Flexi"
   ppr (Indirect ty) = text "Indirect" <+> ppr ty
 
 pprTcTyVarDetails :: TcTyVarDetails -> SDoc
 -- For debugging
-pprTcTyVarDetails (RuntimeUnk {})  = text "rt"
-pprTcTyVarDetails (FlatSkol {})    = text "fsk"
+pprTcTyVarDetails (RuntimeUnk {})      = text "rt"
 pprTcTyVarDetails (SkolemTv lvl True)  = text "ssk" <> colon <> ppr lvl
 pprTcTyVarDetails (SkolemTv lvl False) = text "sk"  <> colon <> ppr lvl
 pprTcTyVarDetails (MetaTv { mtv_info = info, mtv_tclvl = tclvl })
 pprTcTyVarDetails (SkolemTv lvl True)  = text "ssk" <> colon <> ppr lvl
 pprTcTyVarDetails (SkolemTv lvl False) = text "sk"  <> colon <> ppr lvl
 pprTcTyVarDetails (MetaTv { mtv_info = info, mtv_tclvl = tclvl })
@@ -546,7 +547,8 @@ pprTcTyVarDetails (MetaTv { mtv_info = info, mtv_tclvl = tclvl })
     pp_info = case info of
                 TauTv      -> text "tau"
                 SigTv      -> text "sig"
     pp_info = case info of
                 TauTv      -> text "tau"
                 SigTv      -> text "sig"
-                FlatMetaTv -> text "fuv"
+                FlatMetaTv -> text "fmv"
+                FlatSkolTv -> text "fsk"
 
 
 {- *********************************************************************
 
 
 {- *********************************************************************
@@ -715,7 +717,7 @@ Note [TcLevel assignment]
 ~~~~~~~~~~~~~~~~~~~~~~~~~
 We arrange the TcLevels like this
 
 ~~~~~~~~~~~~~~~~~~~~~~~~~
 We arrange the TcLevels like this
 
-   0   Level for flatten meta-vars
+   0   Level for all flatten meta-vars
    1   Top level
    2   First-level implication constraints
    3   Second-level implication constraints
    1   Top level
    2   First-level implication constraints
    3   Second-level implication constraints
@@ -727,9 +729,9 @@ The flatten meta-vars are all at level 0, just to make them untouchable.
 maxTcLevel :: TcLevel -> TcLevel -> TcLevel
 maxTcLevel (TcLevel a) (TcLevel b) = TcLevel (a `max` b)
 
 maxTcLevel :: TcLevel -> TcLevel -> TcLevel
 maxTcLevel (TcLevel a) (TcLevel b) = TcLevel (a `max` b)
 
-fmvTcLevel :: TcLevel -> TcLevel
+fmvTcLevel :: TcLevel
 -- See Note [TcLevel assignment]
 -- See Note [TcLevel assignment]
-fmvTcLevel = TcLevel 0
+fmvTcLevel = TcLevel 0
 
 topTcLevel :: TcLevel
 -- See Note [TcLevel assignment]
 
 topTcLevel :: TcLevel
 -- See Note [TcLevel assignment]
@@ -763,7 +765,6 @@ tcTyVarLevel tv
     case tcTyVarDetails tv of
           MetaTv { mtv_tclvl = tv_lvl } -> tv_lvl
           SkolemTv tv_lvl _             -> tv_lvl
     case tcTyVarDetails tv of
           MetaTv { mtv_tclvl = tv_lvl } -> tv_lvl
           SkolemTv tv_lvl _             -> tv_lvl
-          FlatSkol ty                   -> tcTypeLevel ty
           RuntimeUnk                    -> topTcLevel
 
 tcTypeLevel :: TcType -> TcLevel
           RuntimeUnk                    -> topTcLevel
 
 tcTypeLevel :: TcType -> TcLevel
@@ -1167,20 +1168,15 @@ isFmvTyVar tv
         MetaTv { mtv_info = FlatMetaTv } -> True
         _                                -> False
 
         MetaTv { mtv_info = FlatMetaTv } -> True
         _                                -> False
 
--- | True of both given and wanted flatten-skolems (fak and usk)
-isFlattenTyVar tv
+isFskTyVar tv
   = ASSERT2( tcIsTcTyVar tv, ppr tv )
     case tcTyVarDetails tv of
   = ASSERT2( tcIsTcTyVar tv, ppr tv )
     case tcTyVarDetails tv of
-        FlatSkol {}                      -> True
-        MetaTv { mtv_info = FlatMetaTv } -> True
+        MetaTv { mtv_info = FlatSkolTv } -> True
         _                                -> False
 
         _                                -> False
 
--- | True of FlatSkol skolems only
-isFskTyVar tv
-  = ASSERT2( tcIsTcTyVar tv, ppr tv )
-    case tcTyVarDetails tv of
-        FlatSkol {} -> True
-        _           -> False
+-- | True of both given and wanted flatten-skolems (fak and usk)
+isFlattenTyVar tv
+  = isFmvTyVar tv || isFskTyVar tv
 
 isSkolemTyVar tv
   = ASSERT2( tcIsTcTyVar tv, ppr tv )
 
 isSkolemTyVar tv
   = ASSERT2( tcIsTcTyVar tv, ppr tv )
index e103d20..3f1d77a 100644 (file)
@@ -1603,7 +1603,6 @@ canSolveByUnification tclvl tv xi
                                         SigTv -> True
                                         _     -> False
                        SkolemTv {} -> True
                                         SigTv -> True
                                         _     -> False
                        SkolemTv {} -> True
-                       FlatSkol {} -> False
                        RuntimeUnk  -> True
 
 {- Note [Fmv Orientation Invariant]
                        RuntimeUnk  -> True
 
 {- Note [Fmv Orientation Invariant]
index f8e5055..ee42cc9 100644 (file)
@@ -1,18 +1,14 @@
 
 T7148.hs:27:40: error:
 
 T7148.hs:27:40: error:
-    • Couldn't match type ‘b’ with ‘Tagged a b’
+    • Occurs check: cannot construct the infinite type: b ~ Tagged a b
         arising from the coercion of the method ‘iso2’
           from type ‘forall b1. SameType b1 () -> SameType b1 b’
             to type ‘forall b1. SameType b1 () -> SameType b1 (Tagged a b)’
         arising from the coercion of the method ‘iso2’
           from type ‘forall b1. SameType b1 () -> SameType b1 b’
             to type ‘forall b1. SameType b1 () -> SameType b1 (Tagged a b)’
-      ‘b’ is a rigid type variable bound by
-        the deriving clause for ‘IsoUnit (Tagged a b)’ at T7148.hs:27:40-46
     • When deriving the instance for (IsoUnit (Tagged a b))
 
 T7148.hs:27:40: error:
     • When deriving the instance for (IsoUnit (Tagged a b))
 
 T7148.hs:27:40: error:
-    • Couldn't match type ‘b’ with ‘Tagged a b’
+    • Occurs check: cannot construct the infinite type: b ~ Tagged a b
         arising from the coercion of the method ‘iso1’
           from type ‘forall b1. SameType () b1 -> SameType b b1’
             to type ‘forall b1. SameType () b1 -> SameType (Tagged a b) b1’
         arising from the coercion of the method ‘iso1’
           from type ‘forall b1. SameType () b1 -> SameType b b1’
             to type ‘forall b1. SameType () b1 -> SameType (Tagged a b) b1’
-      ‘b’ is a rigid type variable bound by
-        the deriving clause for ‘IsoUnit (Tagged a b)’ at T7148.hs:27:40-46
     • When deriving the instance for (IsoUnit (Tagged a b))
     • When deriving the instance for (IsoUnit (Tagged a b))
index 4bc39a7..d0f650b 100644 (file)
@@ -1,10 +1,6 @@
 
 T3169.hs:13:22: error:
 
 T3169.hs:13:22: error:
-    • Couldn't match type ‘elt’ with ‘Map b elt’
-      ‘elt’ is a rigid type variable bound by
-        the type signature for:
-          lookup :: forall elt. (a, b) -> Map (a, b) elt -> Maybe elt
-        at T3169.hs:12:3-8
+    • Occurs check: cannot construct the infinite type: elt ~ Map b elt
       Expected type: Map a (Map b elt)
         Actual type: Map (a, b) elt
     • In the second argument of ‘lookup’, namely ‘m’
       Expected type: Map a (Map b elt)
         Actual type: Map (a, b) elt
     • In the second argument of ‘lookup’, namely ‘m’
index ff90037..568f64f 100644 (file)
@@ -1,10 +1,6 @@
 
 T7558.hs:8:4: error:
 
 T7558.hs:8:4: error:
-    • Couldn't match type ‘a’ with ‘Maybe a’
-      ‘a’ is a rigid type variable bound by
-        the type signature for:
-          f :: forall a. T a a -> Bool
-        at T7558.hs:7:1-18
+    • Occurs check: cannot construct the infinite type: a ~ Maybe a
       Inaccessible code in
         a pattern with constructor:
           MkT :: forall a b. a ~ Maybe b => a -> Maybe b -> T a b,
       Inaccessible code in
         a pattern with constructor:
           MkT :: forall a b. a ~ Maybe b => a -> Maybe b -> T a b,
diff --git a/testsuite/tests/indexed-types/should_fail/T13674.hs b/testsuite/tests/indexed-types/should_fail/T13674.hs
new file mode 100644 (file)
index 0000000..4d9a81d
--- /dev/null
@@ -0,0 +1,56 @@
+{-# LANGUAGE ConstraintKinds #-}
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TypeApplications #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE TypeOperators #-}
+
+module T13674 where
+
+import Data.Proxy
+import GHC.Exts (Constraint)
+import GHC.TypeLits
+import Unsafe.Coerce (unsafeCoerce)
+
+data Dict :: Constraint -> * where
+  Dict :: a => Dict a
+
+infixr 9 :-
+newtype a :- b = Sub (a => Dict b)
+
+-- | Given that @a :- b@, derive something that needs a context @b@, using the context @a@
+(\\) :: a => (b => r) -> (a :- b) -> r
+r \\ Sub Dict = r
+
+newtype Magic n = Magic (KnownNat n => Dict (KnownNat n))
+
+magic :: forall n m o. (Integer -> Integer -> Integer) -> (KnownNat n, KnownNat m) :- KnownNat o
+magic f = Sub $ unsafeCoerce (Magic Dict) (natVal (Proxy :: Proxy n) `f` natVal (Proxy :: Proxy m))
+
+type family Lcm :: Nat -> Nat -> Nat where
+
+axiom :: forall a b. Dict (a ~ b)
+axiom = unsafeCoerce (Dict :: Dict (a ~ a))
+
+lcmNat :: forall n m. (KnownNat n, KnownNat m) :- KnownNat (Lcm n m)
+lcmNat = magic lcm
+
+lcmIsIdempotent :: forall n. Dict (n ~ Lcm n n)
+lcmIsIdempotent = axiom
+
+newtype GF (n :: Nat) = GF Integer
+
+x :: GF 5
+x = GF 3
+
+y :: GF 5
+y = GF 4
+
+foo :: (KnownNat m, KnownNat n) => GF m -> GF n -> GF (Lcm m n)
+foo m@(GF x) n@(GF y) = GF $ (x*y) `mod` (lcm (natVal m) (natVal n))
+
+bar :: (KnownNat m)  => GF m -> GF m -> GF m
+bar (x :: GF m) y = foo x y - foo y x \\ lcmNat @m @m \\ Sub @() (lcmIsIdempotent @m)
diff --git a/testsuite/tests/indexed-types/should_fail/T13674.stderr b/testsuite/tests/indexed-types/should_fail/T13674.stderr
new file mode 100644 (file)
index 0000000..53a7cb7
--- /dev/null
@@ -0,0 +1,28 @@
+
+T13674.hs:56:21: error:
+    • Occurs check: cannot construct the infinite type: m ~ Lcm m m
+      Expected type: GF m
+        Actual type: GF (Lcm m m)
+    • In the first argument of ‘(-)’, namely ‘foo x y’
+      In the expression:
+        foo x y - foo y x \\ lcmNat @m @m \\ Sub @() (lcmIsIdempotent @m)
+      In an equation for ‘bar’:
+          bar (x :: GF m) y
+            = foo x y - foo y x \\ lcmNat @m @m \\ Sub @() (lcmIsIdempotent @m)
+    • Relevant bindings include
+        y :: GF m (bound at T13674.hs:56:17)
+        x :: GF m (bound at T13674.hs:56:6)
+        bar :: GF m -> GF m -> GF m (bound at T13674.hs:56:1)
+
+T13674.hs:56:31: error:
+    • Occurs check: cannot construct the infinite type: m ~ Lcm m m
+      Expected type: GF m
+        Actual type: GF (Lcm m m)
+    • In the first argument of ‘(\\)’, namely ‘foo y x’
+      In the first argument of ‘(\\)’, namely ‘foo y x \\ lcmNat @m @m’
+      In the second argument of ‘(-)’, namely
+        ‘foo y x \\ lcmNat @m @m \\ Sub @() (lcmIsIdempotent @m)’
+    • Relevant bindings include
+        y :: GF m (bound at T13674.hs:56:17)
+        x :: GF m (bound at T13674.hs:56:6)
+        bar :: GF m -> GF m -> GF m (bound at T13674.hs:56:1)
index f60711a..f0c5ab5 100644 (file)
@@ -1,10 +1,7 @@
 
 T4272.hs:15:26: error:
 
 T4272.hs:15:26: error:
-    • Couldn't match type ‘a’ with ‘TermFamily a a’
-      ‘a’ is a rigid type variable bound by
-        the type signature for:
-          laws :: forall a b. TermLike a => TermFamily a a -> b
-        at T4272.hs:14:1-53
+    • Occurs check: cannot construct the infinite type:
+        a ~ TermFamily a a
       Expected type: TermFamily a (TermFamily a a)
         Actual type: TermFamily a a
     • In the first argument of ‘terms’, namely
       Expected type: TermFamily a (TermFamily a a)
         Actual type: TermFamily a a
     • In the first argument of ‘terms’, namely
index 3cdc60a..54b0566 100644 (file)
@@ -1,7 +1,7 @@
 
 T9662.hs:47:8: error:
 
 T9662.hs:47:8: error:
-    • Couldn't match type ‘m’ with ‘Int’
-      ‘m’ is a rigid type variable bound by
+    • Couldn't match type ‘k’ with ‘Int’
+      ‘k’ is a rigid type variable bound by
         the type signature for:
           test :: forall sh k m n.
                   Shape (((sh :. k) :. m) :. n) -> Shape (((sh :. m) :. n) :. k)
         the type signature for:
           test :: forall sh k m n.
                   Shape (((sh :. k) :. m) :. n) -> Shape (((sh :. m) :. n) :. k)
index 9cad8e1..24abd30 100644 (file)
@@ -133,3 +133,4 @@ test('T12867', normal, compile_fail, [''])
 test('T7102', [ expect_broken(7102) ], ghci_script, ['T7102.script'])
 test('T7102a', normal, ghci_script, ['T7102a.script'])
 test('T13271', normal, compile_fail, [''])
 test('T7102', [ expect_broken(7102) ], ghci_script, ['T7102.script'])
 test('T7102a', normal, ghci_script, ['T7102a.script'])
 test('T13271', normal, compile_fail, [''])
+test('T13674', normal, compile_fail, [''])
index d7ac728..85728da 100644 (file)
@@ -1,13 +1,9 @@
 
 FD3.hs:15:15: error:
 
 FD3.hs:15:15: error:
-    • Couldn't match type ‘a’ with ‘(String, a)’
+    • Occurs check: cannot construct the infinite type: a ~ (String, a)
         arising from a functional dependency between:
           constraint ‘MkA (String, a) a’ arising from a use of ‘mkA’
           instance ‘MkA a1 a1’ at FD3.hs:12:10-16
         arising from a functional dependency between:
           constraint ‘MkA (String, a) a’ arising from a use of ‘mkA’
           instance ‘MkA a1 a1’ at FD3.hs:12:10-16
-      ‘a’ is a rigid type variable bound by
-        the type signature for:
-          translate :: forall a. (String, a) -> A a
-        at FD3.hs:14:1-31
     • In the expression: mkA a
       In an equation for ‘translate’: translate a = mkA a
     • Relevant bindings include
     • In the expression: mkA a
       In an equation for ‘translate’: translate a = mkA a
     • Relevant bindings include
index 303b1de..01b003f 100644 (file)
@@ -1,8 +1,6 @@
 
 T9834.hs:23:10: warning: [-Wdeferred-type-errors (in -Wdefault)]
 
 T9834.hs:23:10: warning: [-Wdeferred-type-errors (in -Wdefault)]
-    • Couldn't match type ‘p’ with ‘(->) (p a0)’
-      ‘p’ is a rigid type variable bound by
-        the class declaration for ‘ApplicativeFix’ at T9834.hs:21:39
+    • Occurs check: cannot construct the infinite type: p ~ (->) (p a0)
       Expected type: (forall (q :: * -> *).
                       Applicative q =>
                       Comp p q a -> Comp p q a)
       Expected type: (forall (q :: * -> *).
                       Applicative q =>
                       Comp p q a -> Comp p q a)
index cffb7f6..1b9682e 100644 (file)
@@ -1,10 +1,6 @@
 
 mc19.hs:10:31: error:
 
 mc19.hs:10:31: error:
-    • Couldn't match type ‘a’ with ‘[a]’
-      ‘a’ is a rigid type variable bound by
-        a type expected by the context:
-          forall a. [a] -> [a]
-        at mc19.hs:10:10-35
+    • Occurs check: cannot construct the infinite type: a ~ [a]
       Expected type: [a] -> [a]
         Actual type: [a] -> [[a]]
     • In the expression: inits
       Expected type: [a] -> [a]
         Actual type: [a] -> [[a]]
     • In the expression: inits
index 9cffcfb..014628f 100644 (file)
@@ -1,10 +1,6 @@
 
 mc21.hs:12:26: error:
 
 mc21.hs:12:26: error:
-    • Couldn't match type ‘a’ with ‘[a]’
-      ‘a’ is a rigid type variable bound by
-        a type expected by the context:
-          forall a. [a] -> [[a]]
-        at mc21.hs:(11,9)-(12,31)
+    • Occurs check: cannot construct the infinite type: a ~ [a]
       Expected type: [a] -> [[a]]
         Actual type: [[a]] -> [[a]]
     • In the expression: take 5
       Expected type: [a] -> [[a]]
         Actual type: [[a]] -> [[a]]
     • In the expression: take 5
index ec82baf..40a754a 100644 (file)
@@ -1,10 +1,6 @@
 
 mc22.hs:10:26: error:
 
 mc22.hs:10:26: error:
-    • Couldn't match type ‘a’ with ‘t a’
-      ‘a’ is a rigid type variable bound by
-        a type expected by the context:
-          forall a. [a] -> [t a]
-        at mc22.hs:(9,9)-(10,31)
+    • Occurs check: cannot construct the infinite type: a ~ t a
       Expected type: [a] -> [t a]
         Actual type: [t a] -> [t a]
     • In the expression: take 5
       Expected type: [a] -> [t a]
         Actual type: [t a] -> [t a]
     • In the expression: take 5
index 8eb11f9..125c2d8 100644 (file)
@@ -1,10 +1,6 @@
 
 tcfail191.hs:11:26: error:
 
 tcfail191.hs:11:26: error:
-    • Couldn't match type ‘a’ with ‘[a]’
-      ‘a’ is a rigid type variable bound by
-        a type expected by the context:
-          forall a. [a] -> [[a]]
-        at tcfail191.hs:(10,9)-(11,31)
+    • Occurs check: cannot construct the infinite type: a ~ [a]
       Expected type: [a] -> [[a]]
         Actual type: [[a]] -> [[a]]
     • In the expression: take 5
       Expected type: [a] -> [[a]]
         Actual type: [[a]] -> [[a]]
     • In the expression: take 5
index 6259dfc..028e2f0 100644 (file)
@@ -1,10 +1,6 @@
 
 tcfail193.hs:10:31: error:
 
 tcfail193.hs:10:31: error:
-    • Couldn't match type ‘a’ with ‘[a]’
-      ‘a’ is a rigid type variable bound by
-        a type expected by the context:
-          forall a. [a] -> [a]
-        at tcfail193.hs:10:10-35
+    • Occurs check: cannot construct the infinite type: a ~ [a]
       Expected type: [a] -> [a]
         Actual type: [a] -> [[a]]
     • In the expression: inits
       Expected type: [a] -> [a]
         Actual type: [a] -> [[a]]
     • In the expression: inits