[GHC] #15909: prepareAlts does not take into account equalities which are in scope

GHC ghc-devs at haskell.org
Fri Nov 16 16:06:13 UTC 2018


#15909: prepareAlts does not take into account equalities which are in scope
-------------------------------------+-------------------------------------
        Reporter:  mpickering        |                Owner:  (none)
            Type:  bug               |               Status:  new
        Priority:  normal            |            Milestone:  8.6.3
       Component:  Compiler          |              Version:  8.6.2
      Resolution:                    |             Keywords:
Operating System:  Unknown/Multiple  |         Architecture:
                                     |  Unknown/Multiple
 Type of failure:  None/Unknown      |            Test Case:
      Blocked By:                    |             Blocking:
 Related Tickets:                    |  Differential Rev(s):
       Wiki Page:                    |
-------------------------------------+-------------------------------------

Comment (by simonpj):

 Reasoning about equalities is the business of the typechecker, and the
 simplifier doesn't do much.

 But it does do some things; e.g. it tries to reduce type-family
 applications.

 It would be reasonable to try to make it do more; and indeed to support
 the pattern-match overlap stuff we have an API for the typechecker that
 can be called externally.  I don't know if it's the ''right'' API for this
 purpose.

 To make this work we'd have to accumulate the "givens" as we go down. Not
 too hard. I'd be inclined to do this in a separate pass, NOT the
 simplifier which has too much else to do.  Just possibly the occurrence
 analyser, though I worry about slowing it down.

 Another tricky point is that I'd like to be able to prove that every case
 is exhaustive, and a Lint-checkable property.  But if I later remove the
 second parameter to f2 (it is dead) then it won't be provable anymore.
 This problem is more basic than fancy equalities.  Consider
 {{{
 case x of
   Red -> e1
   DEFAULT -> let v = case x of
                        Red -> e2
                        Blue -> e3
                        Green -> e4
              in blah
 }}}
 we can prune the `Red` branch out of the `case` in the RHS of `v`. But now
 imagine floating the `v`-binding:
 {{{
 let v = case x of
           Blue -> e3
           Green -> e4
 in case x of
   Red -> e1
   DEFAULT -> blah
 }}}
 This is actually still correct, but it's not ''obviously'' correct.

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


More information about the ghc-tickets mailing list