[GHC] #15322: `KnownNat` does not imply `Typeable` any more when used with plugin

[GHC]

#15322: `KnownNat` does not imply `Typeable` any more when used with plugin
-------------------------------------+-------------------------------------
        Reporter:  chshersh          |                Owner:  (none)
            Type:  bug               |               Status:  new
        Priority:  normal            |            Milestone:  8.6.1
       Component:  Compiler          |              Version:  8.4.3
      Resolution:                    |             Keywords:
                                     |  typeable,knownnat
Operating System:  Unknown/Multiple  |         Architecture:
 Type of failure:  GHC rejects       |  Unknown/Multiple
  valid program                      |            Test Case:
      Blocked By:                    |             Blocking:
 Related Tickets:  #10348            |  Differential Rev(s):
       Wiki Page:                    |
-------------------------------------+-------------------------------------
Changes (by simonpj):

 * cc: diatchki (added)


Comment:

 #15322

 Does this need the plugin to demonstrate the bug?  It complicate
 reproduction, and indeed I'm not sure how to set up the plugin.

 ------------

 I do know a bit about what's going on.  I think this bug is a consequence
 of this patch
 {{{
 commit c41ccbfa8aaeb99dd9a36cb3d99993f0fa039cdc
 Author: Simon Peyton Jones <simonpj at microsoft.com>
 Date:   Tue Sep 26 15:02:09 2017 +0100

     Omit Typeable from the "naturally coherent" list

     In doing something else (Trac #14218) I tripped over the
     definition of "naturally coherent" classes.  This patch

     - Cocuments properly what that means

     - Removes Typeable from the list, because now we know what
       it meams, Typeable clearly doesn't belong.

     No regressions.

     (Actually the term "naturally coherent" seems a bit off.
     More like "invertible" or something.  But I left it.)
 }}}
 The issue here is this.  We have
 {{{
   [G] Typeable n   [G] KnownNat n
   [W] Typeable (n+1)
 }}}
 Can we use `TcInteract.doTyLit` to simplify the `[W]` goal, by
 instead generating `[W] KnownNat (n+1)`?  GHC does not do so,
 because suppose we had instead got:
 {{{
  [G] Typeable x
  [G] Typeable (F [x])
 }}}
 where `type family F (x::Nat) :: Nat`.   Now we don't want to do
 the `doTyLit` thing because then we'd be stuck... we'd have
 `[W] KnownNat (F [x])` with no way to solve it.

 Instead, by deferring that choice, GHC is hoping that later we'll
 reduce `F [x]  -->  x` and bingo we'd have `[W] Typeable x` which we
 can solve from the Given.  Background info: this "deferring" business is
 implmented by this code in `TcInteract`:
 {{{
 matchClassInst dflags inerts clas tys loc
 -- First check whether there is an in-scope Given that could
 -- match this constraint.  In that case, do not use any instance
 -- whether top level, or local quantified constraints.
 -- ee Note [Instance and Given overlap]
   | not (xopt LangExt.IncoherentInstances dflags)
   , not (naturallyCoherentClass clas)
   , let matchable_givens = matchableGivens loc pred inerts
   , not (isEmptyBag matchable_givens)
   = do { traceTcS "Delaying instance application" $
            vcat [ text "Work item=" <+> pprClassPred clas tys
                 , text "Potential matching givens:" <+> ppr
 matchable_givens ]
        ; return NotSure }
 }}}

 Returning to the example, I'm pretty suspicous of the whole `doTyLit`
 thing (introduced by Iavor in Trac #10348).  It seems to say that
 really the ''only'' way to solve `Typeable (ty :: Nat)` is by proving
 `KnonwNat ty`, which seems to me like replacing a simple goal with a
 complicated one.

 One possible workaround for you may be to remove the `Typeable n`
 constraint
 since it is (I think) mysteriously implied by `Typeable` (c.f. Trac
 #10348).
 I say "mysteriously" because `Typeable` is not a superclass of `KonwnNat`.

 Iavor, I'm a bit lost here.

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