Marge Bot pushed to branch master at Glasgow Haskell Compiler / GHC

Commits:

4 changed files:

Changes:

  • compiler/GHC/Tc/Types/Constraint.hs
    ... ... @@ -1181,9 +1181,12 @@ dropMisleading (WC { wc_simple = simples, wc_impl = implics, wc_errors = errors
    1181 1181 
                , wc_impl   = mapBag drop_implic implics
    1182 1182 
                , wc_errors  = filterBag keep_delayed_error errors }
    1183 1183
    1184 
    -    keep_ct ct = case classifyPredType (ctPred ct) of
    1185 
    -                    ClassPred {} -> False
    1186 
    -                    _ -> True
    1184 
    +    keep_ct ct
    1185 
    +      = case classifyPredType (ctPred ct) of
    1186 
    +           ClassPred cls _ -> isEqualityClass cls
    1187 
    +             -- isEqualityClass: see (CERR2) in Note [Constraints and errors]
    1188 
    +             --                  in GHC.Tc.Utils.Monad
    1189 
    +           _ -> True
    1187 1190
    1188 1191 
         keep_delayed_error (DE_Hole hole) = isOutOfScopeHole hole
    1189 1192 
         keep_delayed_error (DE_NotConcrete {}) = True

  • compiler/GHC/Tc/Utils/Monad.hs
    ... ... @@ -1385,11 +1385,13 @@ tryCaptureConstraints thing_inside
    1385 1385 
                               tcTryM thing_inside
    1386 1386
    1387 1387 
            -- See Note [Constraints and errors]
    1388 
    -       ; let lie_to_keep = case mb_res of
    1389 
    -                             Nothing -> dropMisleading lie
    1390 
    -                             Just {} -> lie
    1391 
    -
    1392 
    -       ; return (mb_res, lie_to_keep) }
    1388 
    +       ; case mb_res of
    1389 
    +            Just {} -> return (mb_res, lie)
    1390 
    +            Nothing -> do { let pruned_lie = dropMisleading lie
    1391 
    +                          ; traceTc "tryCaptureConstraints" $
    1392 
    +                            vcat [ text "lie:" <+> ppr lie
    1393 
    +                                 , text "dropMisleading lie:" <+> ppr pruned_lie ]
    1394 
    +                          ; return (Nothing, pruned_lie) } }
    1393 1395
    1394 1396 
     captureConstraints :: TcM a -> TcM (a, WantedConstraints)
    1395 1397 
     -- (captureConstraints m) runs m, and returns the type constraints it generates
    ... ... @@ -2066,28 +2068,51 @@ It's distressingly delicate though:
    2066 2068 
       emitted some constraints with skolem-escape problems.
    2067 2069
    2068 2070 
     * If we discard too /few/ constraints, we may get the misleading
    2069 
    -  class constraints mentioned above.  But we may /also/ end up taking
    2070 
    -  constraints built at some inner level, and emitting them at some
    2071 
    -  outer level, and then breaking the TcLevel invariants
    2072 
    -  See Note [TcLevel invariants] in GHC.Tc.Utils.TcType
    2073 
    -
    2074 
    -So dropMisleading has a horridly ad-hoc structure.  It keeps only
    2075 
    -/insoluble/ flat constraints (which are unlikely to very visibly trip
    2076 
    -up on the TcLevel invariant, but all /implication/ constraints (except
    2077 
    -the class constraints inside them).  The implication constraints are
    2078 
    -OK because they set the ambient level before attempting to solve any
    2079 
    -inner constraints.  Ugh! I hate this. But it seems to work.
    2080 
    -
    2081 
    -However note that freshly-generated constraints like (Int ~ Bool), or
    2082 
    -((a -> b) ~ Int) are all CNonCanonical, and hence won't be flagged as
    2083 
    -insoluble.  The constraint solver does that.  So they'll be discarded.
    2084 
    -That's probably ok; but see th/5358 as a not-so-good example:
    2085 
    -   t1 :: Int
    2086 
    -   t1 x = x   -- Manifestly wrong
    2087 
    -
    2088 
    -   foo = $(...raises exception...)
    2089 
    -We report the exception, but not the bug in t1.  Oh well.  Possible
    2090 
    -solution: make GHC.Tc.Utils.Unify.uType spot manifestly-insoluble constraints.
    2071 
    +  class constraints mentioned above.
    2072 
    +
    2073 
    +  We may /also/ end up taking constraints built at some inner level, and
    2074 
    +  emitting them (via the exception catching in `tryCaptureConstraints` at some
    2075 
    +  outer level, and then breaking the TcLevel invariants See Note [TcLevel
    2076 
    +  invariants] in GHC.Tc.Utils.TcType
    2077 
    +
    2078 
    +So `dropMisleading` has a horridly ad-hoc structure:
    2079 
    +
    2080 
    +* It keeps only /insoluble/ flat constraints (which are unlikely to very visibly
    2081 
    +  trip up on the TcLevel invariant
    2082 
    +
    2083 
    +* But it keeps all /implication/ constraints (except the class constraints
    2084 
    +  inside them).  The implication constraints are OK because they set the ambient
    2085 
    +  level before attempting to solve any inner constraints.
    2086 
    +
    2087 
    +Ugh! I hate this. But it seems to work.
    2088 
    +
    2089 
    +Other wrinkles
    2090 
    +
    2091 
    +(CERR1) Note that freshly-generated constraints like (Int ~ Bool), or
    2092 
    +    ((a -> b) ~ Int) are all CNonCanonical, and hence won't be flagged as
    2093 
    +    insoluble.  The constraint solver does that.  So they'll be discarded.
    2094 
    +    That's probably ok; but see th/5358 as a not-so-good example:
    2095 
    +       t1 :: Int
    2096 
    +       t1 x = x   -- Manifestly wrong
    2097 
    +
    2098 
    +       foo = $(...raises exception...)
    2099 
    +    We report the exception, but not the bug in t1.  Oh well.  Possible
    2100 
    +    solution: make GHC.Tc.Utils.Unify.uType spot manifestly-insoluble constraints.
    2101 
    +
    2102 
    +(CERR2) In #26015 I found that from the constraints
    2103 
    +           [W] alpha ~ Int      -- A class constraint
    2104 
    +           [W] F alpha ~# Bool  -- An equality constraint
    2105 
    +  we were dropping the first (becuase it's a class constraint) but not the
    2106 
    +  second, and then getting a misleading error message from the second.  As
    2107 
    +  #25607 shows, we can get not just one but a zillion bogus messages, which
    2108 
    +  conceal the one genuine error.  Boo.
    2109 
    +
    2110 
    +  For now I have added an even more ad-hoc "drop class constraints except
    2111 
    +  equality classes (~) and (~~)"; see `dropMisleading`.  That just kicks the can
    2112 
    +  down the road; but this problem seems somewhat rare anyway.  The code in
    2113 
    +  `dropMisleading` hasn't changed for years.
    2114 
    +
    2115 
    +It would be great to have a more systematic solution to this entire mess.
    2091 2116
    2092 2117
    2093 2118 
     ************************************************************************

  • testsuite/tests/typecheck/should_fail/T26015.hs
    1 
    +{-# LANGUAGE MonoLocalBinds, GADTs, TypeFamilies #-}
    2 
    +
    3 
    +module Foo where
    4 
    +
    5 
    +type family F a
    6 
    +type instance F Int = Bool
    7 
    +
    8 
    +data T where
    9 
    +  T1 :: a -> T
    10 
    +  T2 :: Int -> T
    11 
    +
    12 
    +woo :: (a ~ Int) => Int -> F a
    13 
    +woo = error "urk"
    14 
    +
    15 
    +f x = case x of
    16 
    +         T1 y -> not (woo 3)
    17 
    +         T2 -> True

  • testsuite/tests/typecheck/should_fail/T26015.stderr
    1 
    +T26015.hs:17:10: error: [GHC-27346]
    2 
    +    • The data constructor ‘T2’ should have 1 argument, but has been given none
    3 
    +    • In the pattern: T2
    4 
    +      In a case alternative: T2 -> True
    5 
    +      In the expression:
    6 
    +        case x of
    7 
    +          T1 y -> not (woo 3)
    8 
    +          T2 -> True
    9 
    +

    • —
    View it on GitLab.
    You're receiving this email because of your account on gitlab.haskell.org. Manage all notifications · Help