#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_... 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