#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@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