[GHC] #15009: Float equalities past local equalities

[GHC]

#15009: Float equalities past local equalities
-------------------------------------+-------------------------------------
        Reporter:  goldfire          |                Owner:  (none)
            Type:  feature request   |               Status:  closed
        Priority:  normal            |            Milestone:  8.4.3
       Component:  Compiler          |              Version:  8.2.2
      Resolution:  fixed             |             Keywords:
Operating System:  Unknown/Multiple  |         Architecture:
                                     |  Unknown/Multiple
 Type of failure:  None/Unknown      |            Test Case:  gadt/T15009
      Blocked By:                    |             Blocking:
 Related Tickets:                    |  Differential Rev(s):
       Wiki Page:                    |
-------------------------------------+-------------------------------------

Comment (by nfrisby):

 Very happy to see the progress on this ticket! I think it would even be
 worthwhile for GHC to be a bit more aggressive here. In particular, in the
 snippet below, I'd like GHC to infer that {{{test :: () -> NT ((:~:) Char)
 Maybe}}}. I see this comment's example as decomposing the ticket's example
 {{{T1}}} into {{{:~:}}} and {{{NT}}}: the equality constraint and the
 {{{forall}}} need not be collocated.

 If I understand correctly, the key hurdle to that inference is revealed on
 line 3640 of the tc-trace below and the reason {{{getNoGivenEqs}}} reports
 {{{False}}} here is because {{{x_a1d8[sk:2]}}} is level 2 whereas the
 implication is level 3.

 I haven't found any Notes explaining why {{{getNoGivenEqs}}} checks that
 the skolem is from the current implication. Would it be safe and
 worthwhile to relax this check to, for example, as in this this particular
 case, require that there be no givens between the skolem's level and the
 current implication's level? (Or more loosely perhaps: no such equality-
 like givens, or even no equality-like givens involving this skolem?)

 {{{
 $ cat Test.hs
 {-# LANGUAGE GADTs, LambdaCase, Rank2Types #-}
 {-# OPTIONS_GHC -ddump-tc-trace #-}
 module Test where
 import Data.Type.Equality
 newtype NT f g = MkNT{appNT :: forall x. f x -> g x}
 test () = MkNT (\case Refl -> Just 'c')

 $ ./ghc-8.6.0.20180810/bin/ghc.exe --make Test.hs >catch 2>&1

 $ grep --text -B7 -A5 -n -e 'May have given eq' catch
 [snip]
 --
 3634-  final wc = WC {wc_simple =
 3635-                   [WD] hole{co_a1dv} {1}:: g_a1d6[tau:1]
 3636-                                            GHC.Prim.~# Maybe
 (CNonCanonical)
 3637-                   [WD] hole{co_a1dy} {2}:: a_a1dx[tau:1]
 3638-                                            GHC.Prim.~# Char
 (CNonCanonical)}
 3639-  current evbinds  = {}
 3640-getNoGivenEqs
 3641:  May have given equalities
 3642-  Skols: []
 3643-  Inerts: {Equalities: [G] co_a1dj {0}:: x_a1d8[sk:2]
 3644-                                         GHC.Prim.~# a_a1dx[tau:1]
 (CTyEqCan)
 3645-           Unsolved goals = 0}
 3646-  Insols: {}
 --
 [snip]
 }}}

 Thank you for your time. -Nick

 P.S. - My Reddit post from a few months ago gives a bit more discussion of
 this kind of example;
 https://www.reddit.com/r/haskell/comments/8h9mz8/a_way_to_improve_inference_under_gadt_patterns/
 Thanks again, Richard, for pointed me here from there; timely!

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