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

#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: | -------------------------------------+------------------------------------- Comment (by diatchki): My thinking was as follows: we are treating `Nat` and `Symbol` as just infinite families of type constructors. This makes is tricky to define class instances involving them, as we essentially need to write infinitely many instances. For example: {{{ instance MyClass (T 0) where ... instance MyClass (T 1) where ... ...etc... }}} To avoid having to provide some special mechanism for declaring such instances, we just define one special class that captures this pattern, and the instances are "magically" provided by GHC. For `Nat` it is called `KnownNat`: {{{ instance KnownNat 0 where ... instance KnownNat 1 where ... ... etc .. }}} This makes it possible to define "infinite" instances for any class like this: {{{ instance KnownNat n => MyClass (T n) where ... }}} We do the exact same thing for `Typeable`: {{{ instance KnownNat n => Typeable (n :: Nat) where ... }}} The `KnownNat` constraint provides the run-time representation of the number, which is used to build the run-time representation of the type. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15322#comment:3 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#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: | -------------------------------------+------------------------------------- Comment (by diatchki): We are using the same system for `Typeable`. Have a look in `Data.Typeable.Internal` (in `base`): the functions `typeNatTypeRep` and `typeSymbolTypeRep` make the run-time representations used by the corresponding `Typeable` instances. The `ds_ev_typeable` function in `deSugar/DsBinds` just uses these functions when it needs to make evidence for `Typeable`. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15322#comment:5 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#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: | -------------------------------------+------------------------------------- Comment (by goldfire): This seems unfortunate to me. I wonder if it would be better to have {{{#!hs getNat :: TypeRep (n :: Nat) -> Natural }}} and then dispense with `KnownNat`. If I were guessing which were primitive between `KnownNat` and `Typeable`, I would guess `Typeable`. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15322#comment:7 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#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: | -------------------------------------+------------------------------------- Comment (by diatchki): Well, the evidence for `KnownNat` is just a simple integer, while the corresponding `TypeRep` is a much more heavy-weight structure, containing hashes, strings, etc. Since these are created on demand for type- literals, we would be doing additional allocation and hashing at run-time. There are many cases where `KnowNat` is useful without the additional functionality provided by `Typeable`, so I think that the current system makes sense. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15322#comment:9 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#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: | -------------------------------------+------------------------------------- Comment (by Simon Peyton Jones ): In [changeset:"7ce6f642a2806c425ba21d48a077d997703cf25b/ghc" 7ce6f642/ghc]: {{{ #!CommitTicketReference repository="ghc" revision="7ce6f642a2806c425ba21d48a077d997703cf25b" Add comments on Typeable (n :: Nat) See Note [Typeable for Nat and Symbol] in TcInteract, which I added after discussion on Trac #15322 }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15322#comment:11 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#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: | -------------------------------------+------------------------------------- Comment (by simonpj): My patch makes the reporting of unnecessary constraints more consistent -- in particular, accounting for built-in constraints. The original program still fails in the same way, for the reason explained in comment:1. What is the "real" fix? Well, despite comment:1 ''we'' know that `Typeable (n+1)` is never going to simplify to `Typeable n` (at least, not without using instances), because we know that `n+1 /= n`. But doesn't know that. The plug-in, I imagine, allows GHC to solve `KnownNat (n+1)` from `KnownNat n`. We want the plugin ''also'' to be able to say that `n` '''is apart from''' `n+1`; that is, they can never be equal. This is a property of `(+)`. So I think that perhaps domain-specific apartness should be part of what a typechecker plugin can specify. I'll leave this ticket open to discuss that idea. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15322#comment:13 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#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: | -------------------------------------+------------------------------------- Comment (by LeanderK): A bit of community-feedback: I have used type-nats a few times and every time I used them, I have been bitten by GHC not recognizing apartness between nats. I think the ability for a plugin to provide the functionality would make them way more useful! -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15322#comment:15 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#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: | -------------------------------------+------------------------------------- Comment (by diatchki): I don't think the apartness issue is specific to `KnownNat` or nats for that matter, it really is more about type functions. From what I've seen, people tend to notice the issue more when working with nats for two reasons (1) they are used to `0` and `succ` being constructors, and so one can define things inductively using them; (2) when using type nats, one simply uses type functions a lot more than in ordinary code. I also think that it would be quite cool to work out a system for matching on type functions (at least in some special cases), but I'd rather not do it through plugins. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15322#comment:17 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#15322: `KnownNat` does not imply `Typeable` any more when used with plugin -------------------------------------+------------------------------------- Reporter: chshersh | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.8.1 Component: Compiler | Version: 8.4.3 Resolution: | Keywords: | typeable,knownnat,TypeCheckerPlugins 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 adamgundry): * keywords: typeable,knownnat => typeable,knownnat,TypeCheckerPlugins * cc: adamgundry (added) -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15322#comment:20 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler