[GHC] #15147: Type checker plugin receives Wanteds that are not completely unflattened

[GHC]

#15147: Type checker plugin receives Wanteds that are not completely unflattened
-------------------------------------+-------------------------------------
           Reporter:  nfrisby        |             Owner:  (none)
               Type:  bug            |            Status:  new
           Priority:  normal         |         Milestone:  8.6.1
          Component:  Compiler       |           Version:  8.4.1
  (Type checker)                     |
           Keywords:  type checker   |  Operating System:  Unknown/Multiple
  plugins                            |
       Architecture:                 |   Type of failure:  None/Unknown
  Unknown/Multiple                   |
          Test Case:                 |        Blocked By:
           Blocking:                 |   Related Tickets:
Differential Rev(s):                 |         Wiki Page:
-------------------------------------+-------------------------------------
 With the following, a plugin will receive a wanted constraint that
 includes a `fsk` flattening skolem.

 {{{
 -- "Reduced" via the plugin
 type family F u v where {}
 type family G a b where {}

 data D p where
   DC :: (p ~ F x (G () ())) => D p
 }}}

 (Please ignore the apparent ambiguity regarding `x`; the goal is for the
 plugin to eliminate any ambiguity.)

 A do-nothing plugin that merely logs its inputs gives the following for
 the ambiguity check on DC.

 {{{
 given
   [G] $d~_a4oh {0}:: (p_a4o2[sk:2] :: *)
                      ~ (p_a4o2[sk:2] :: *) (CDictCan)
   [G] $d~~_a4oi {0}:: (p_a4o2[sk:2] :: *)
                       ~~ (p_a4o2[sk:2] :: *) (CDictCan)
   [G] co_a4od {0}:: (G () () :: *)
                     ~# (fsk_a4oc[fsk:0] :: *) (CFunEqCan)
   [G] co_a4of {0}:: (F x_a4o3[sk:2] fsk_a4oc[fsk:0] :: *)
                     ~# (fsk_a4oe[fsk:0] :: *) (CFunEqCan)
   [G] co_a4og {1}:: (fsk_a4oe[fsk:0] :: *)
                     ~# (p_a4o2[sk:2] :: *) (CTyEqCan)
 derived
 wanted
   [WD] hole{co_a4or} {3}:: (F x_a4o6[tau:2] fsk_a4oc[fsk:0] :: *)
                            ~# (p_a4o2[sk:2] :: *) (CNonCanonical)
 untouchables [fsk_a4oe[fsk:0], fsk_a4oc[fsk:0], x_a4o3[sk:2],
 p_a4o2[sk:2]]
 }}}

 Note the `fsk_a4oc[fsk:0]` tyvar in the Wanted constraint, which is why
 I'm opening this ticket. Its presence contradicts  the "The wanteds will
 be unflattened and zonked" claim from
 https://ghc.haskell.org/trac/ghc/wiki/Plugins/TypeChecker#Callingpluginsfromthetypechecker
 section.

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