[GHC] #15696: Derived Ord instance for enumerations with more than 8 elements seems to be incorrect

[GHC]

#15696: Derived Ord instance for enumerations with more than 8 elements seems to be
incorrect
-------------------------------------+-------------------------------------
        Reporter:  mrkkrp            |                Owner:  osa1
            Type:  bug               |               Status:  patch
        Priority:  highest           |            Milestone:  8.6.2
       Component:  Compiler          |              Version:  8.6.1
      Resolution:                    |             Keywords:
Operating System:  Unknown/Multiple  |         Architecture:
 Type of failure:  Incorrect result  |  Unknown/Multiple
  at runtime                         |            Test Case:
      Blocked By:                    |             Blocking:
 Related Tickets:  #14677, #15155    |  Differential Rev(s):  Phab:D5196,
       Wiki Page:                    |  Phab:D5201
-------------------------------------+-------------------------------------

Comment (by simonpj):

 The rabbit hole gets deeper. In `T10482` We have a data constructor
 `FooPair`
 that is strict in both arguments, and an expression like
 {{{
 foo f k
  = case f of
      FooPair x y -> case burble of
                       True -> case x of
                                 FooPair p q -> ...
                       False -> ...
 }}}
 Previously we floated that inner `case x` out to get
 {{{
 foo f k
  = case f of
      FooPair x y -> case x of
                       FooPair p q -> case burble of
                                        True -> ...
                                        False -> ...
 }}}
 which is nice and strict.

 '''So firstly''': the reasoning in item (3) of comment:60 is right for
 case-binders,
 but not for the binders of a constructor pattern (the binder-swap stuff
 doesn't
 apply to them).  So rather than make the change in item (3), we could
 instead
 just refrain from giving an "evald-unfolding" to the case binder.  This
 happens here, in `Simplify.simplAlts`
 {{{
         ; (env1, case_bndr1) <- simplBinder env0 case_bndr
         ; let case_bndr2 = case_bndr1 `setIdUnfolding` evaldUnfolding
               env2       = modifyInScope env1 case_bndr2
               -- See Note [Case binder evaluated-ness]
 }}}
 We could try (a) undoing the change in item (3), and (b) removing the
 above
 meddling with `case_bndr`.  NB: `Note [Case binder evaluated-ness]` is, I
 believe, out of date; we now skip the lifted args of primpos in `app_ok`.

 '''Secondly''' I think we can improve w/w, even for the case
 where that case-expression is not floated out. It's all to do with
 `Note [Add demands for strict constructors]` in `DmdAnal`,
 and the function `addDataConStrictness`.  This special treatment is
 ineffective
 here because (in the first code for foo above), `x` is really used lazily
 in the alternative.  And yet it'd be sound to unpack it.

 So here's an idea:

 * Delete all the stuff about `addDataConStrictness` from `DmdAnal`.

 * Instead, add it into `WwLib` thus:
 {{{
   | isStrictDmd dmd
   , Just cs <- splitProdDmd_maybe dmd
       -- See Note [Unpacking arguments with product and polymorphic
 demands]
   , not (has_inlineable_prag && isClassPred arg_ty)
       -- See Note [Do not unpack class dictionaries]
   , Just (data_con, inst_tys, inst_con_arg_tys, co)
              <- deepSplitProductType_maybe fam_envs arg_ty
   , cs `equalLength` inst_con_arg_tys
       -- See Note [mkWWstr and unsafeCoerce]
   = do { (uniq1:uniqs) <- getUniquesM
         ; let   cs'       = addDataConStrictness data_con cs
 <---------------- NEW
                 unpk_args = zipWith3 mk_ww_arg uniqs inst_con_arg_tys cs'
                 unbox_fn  = mkUnpackCase (Var arg) co uniq1
                                          data_con unpk_args
                 arg_no_unf = zapStableUnfolding arg
 }}}
   That is, add one new line, and transfer the defn of
 `addDataConStrictness` from `DmdAnal`.

 This actually works, even without implementing "Firstly" -- I tried it.

 '''And thirdly''', I noticed that `addDataConStrictness` makes the demand
 stricter
 like this
 {{{
     add dmd str | isMarkedStrict str
                 , not (isAbsDmd dmd) = dmd `bothDmd` seqDmd
                 | otherwise          = dmd
 }}}
 But `bothDmd seqDmd` messes up the cardinality information!  I doubt this
 is important
 but better to define (in `Demand`)
 {{{
 strictifyDmd :: Demand -> Demand
 strictifyDmd dmd@(JD { sd = str })
   = dmd { sd = str `bothArgStr` Str VanStr HeadStr }
 }}}
 and call it from `addDataConStrictness`.

 I think either Firstly or Secondly should fix the regressions, but all
 three should be good.

-- 
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/15696#comment:77>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler