[GHC] #14899: Significant compilation time regression between 8.4 and HEAD due to coverage checking

[GHC]

#14899: Significant compilation time regression between 8.4 and HEAD due to
coverage checking
-------------------------------------+-------------------------------------
        Reporter:  RyanGlScott       |                Owner:  (none)
            Type:  bug               |               Status:  new
        Priority:  highest           |            Milestone:  8.6.1
       Component:  Compiler          |              Version:  8.5
      Resolution:                    |             Keywords:
                                     |  PatternMatchWarnings
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 RyanGlScott):

 (Warning: half-baked thoughts follow.)

 For reasons that I don't fully understand, it seems that coverage-checking
 guards is not nearly as efficient as coverage-checking raw constructor
 patterns. In that case, a question arises: why are we desugaring coercion
 patterns (like what data family constructors give you) to guards? It seems
 that we could handle coercion patterns in a fairly natural way by
 extending the algorithm from [https://www.microsoft.com/en-us/research/wp-
 content/uploads/2016/08/gadtpm-acm.pdf GADTs Meet Their Match] slightly.

 First, we could extend the pattern syntax (figure 2 from the GADTs Meet
 Their Match paper) to include coercion patterns directly:

 {{{
 p,x ::= x | K p_1 ... p_n | G | (p |> co)
 }}}

 Where `co : τ_1 ~ τ_2` is a coercion.

 Then, we could extend the coverage checking algorithm in figure 3 to
 include a case for coercion patterns. For instance:

 {{{
 C ((p |> co) q_1 ... q_n) (Γ ⊢ u_0 u_1 ... u_n ⊳ Δ)
   = C (p q_1 ... q_n) (Γ, y : τ_1 ⊢ y u_0 u_1 ... u_n ⊳ Δ')
   where
     Γ ⊢ p   : τ_1
     Γ ⊢ u_o : τ_2
     Γ ⊢ c   : τ_1 ~ τ_2
     y#Γ
     Δ' = Δ ∪ u ≈ (p |> co)
 }}}

 And similarly for U and D. That way, we wouldn't need guards at all
 here—we'd just have an extra case for coercion patterns that "pushes
 through" the types as necessary.

 Does this sound plausible?

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