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

Previous Topic Next Topic
 
classic Classic list List threaded Threaded
20 messages Options
Reply | Threaded
Open this post in threaded view
|

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

GHC - devs mailing list
#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
           Keywords:                 |  Operating System:  Unknown/Multiple
  typeable,knownnat                  |
       Architecture:                 |   Type of failure:  GHC rejects
  Unknown/Multiple                   |  valid program
          Test Case:                 |        Blocked By:
           Blocking:                 |   Related Tickets:  #10348
Differential Rev(s):                 |         Wiki Page:
-------------------------------------+-------------------------------------
 I have the following Haskell code which uses `ghc-typelits-knownnat-0.5`
 package as a plugin:

 {{{#!hs
 {-# LANGUAGE DataKinds           #-}
 {-# LANGUAGE ScopedTypeVariables #-}
 {-# LANGUAGE TypeOperators       #-}

 {-# OPTIONS_GHC -fplugin GHC.TypeLits.KnownNat.Solver #-}

 module Nats where

 import Data.Proxy (Proxy (..))
 import Data.Typeable (Typeable)
 import GHC.TypeLits (KnownNat, type (+))

 f :: forall n . (Typeable n, KnownNat n) => Proxy n -> ()
 f _ = ()
 f _ = f (Proxy :: Proxy (n + 1))
 }}}

 When I try to compile this code I observe the following error message:

 {{{
     • Could not deduce (Typeable (n + 1)) arising from a use of ‘f’
       from the context: (Typeable n, KnownNat n)
         bound by the type signature for:
                    f :: forall (n :: ghc-prim-0.5.2.0:GHC.Types.Nat).
                         (Typeable n, KnownNat n) =>
                         Proxy n -> ()
         at src/Nats.hs:13:1-57
     • In the expression: f (Proxy :: Proxy (n + 1))
       In an equation for ‘f’: f _ = f (Proxy :: Proxy (n + 1))
    |
 15 | f _ = f (Proxy :: Proxy (n + 1))
    |       ^^^^^^^^^^^^^^^^^^^^^^^^^^

 }}}

 This code works for both GHC-8.2.2 and GHC-8.0.2. I found similar ticket
 with exactly this problem but looks like this is broken again: #10348
 (bug).

 Originally reported at Github for `ghc-typelits-knownnat` package:

 * https://github.com/clash-lang/ghc-typelits-knownnat/issues/21

 `ghc-typelits-knownnat` package correctly infers `KnownNat (n + 1)`
 constraint so GHC should be able to infer `Typeable (n + 1)`.

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

_______________________________________________
ghc-tickets mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-tickets
Reply | Threaded
Open this post in threaded view
|

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

GHC - devs mailing list
#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 <[hidden email]>
 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

_______________________________________________
ghc-tickets mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-tickets
Reply | Threaded
Open this post in threaded view
|

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

GHC - devs mailing list
In reply to this post by GHC - devs mailing list
#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 chshersh):

 simonpj, thanks a lot for your response. This workaround works perfectly
 for me!

 Regarding simpler example: I tried to come up with example which doesn't
 involve plugin. But didn't manage to do it. I don't know how to launch my
 example with single `ghc` command. What I did: I created very simple
 project with `cabal init`, added `ghc-typelits-knownnat == 0.5` to `build-
 depends` in `.cabal` file and built given source code snippet.

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

_______________________________________________
ghc-tickets mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-tickets
Reply | Threaded
Open this post in threaded view
|

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

GHC - devs mailing list
In reply to this post by GHC - devs mailing list
#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

_______________________________________________
ghc-tickets mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-tickets
Reply | Threaded
Open this post in threaded view
|

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

GHC - devs mailing list
In reply to this post by GHC - devs mailing list
#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):

 >  This makes it possible to define "infinite" instances for any class
 like this:

 Well, how does the `KnownNat` constraint help in defining the instance for
 `MyClass (T n)`?  Presumably, because `KnownNat` lets you use `natSign`:
 {{{
 class KnownNat (n :: Nat) where
   natSing :: SNat n
 }}}
 If that's what you need for `instance MyClass (T n)`, then that makes
 perfect sense.

 But it makes no such sense for `Typeable`.  How does having `KnownNat n`
 available help you write the `Typeable` instance?

 I think we just need built-in behaviour for `Typeable (n :: Nat)`, without
 any reference to `KnownNat`, don't we?   There is ''some'' such built-in
 behaviour already, but I don't understand what it is, and it's clearly
 dodgy as this ticket shows.

 Would you like to elaborate your description of what happens now?

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

_______________________________________________
ghc-tickets mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-tickets
Reply | Threaded
Open this post in threaded view
|

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

GHC - devs mailing list
In reply to this post by GHC - devs mailing list
#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

_______________________________________________
ghc-tickets mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-tickets
Reply | Threaded
Open this post in threaded view
|

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

GHC - devs mailing list
In reply to this post by GHC - devs mailing list
#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):

 OK, now I understand. I'll add this comment to `TcInteract`:
 {{{
 Note [Typeable for Nat and Symbol]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 We have special Typeable instances for Nat and Symbol.  Roughly we
 have this instance, implemented here by doTyLit:
       instance KnownNat n => Typeable (n :: Nat) where
          typeRep = tyepNatTypeRep @n
 where
    Data.Typeable.Internals.typeNatTypeRep :: KnownNat a => TypeRep a

 Ultimately typeNatTypeRep uses 'natSing' from KnownNat to get a
 runtime value 'n'; it turns it into a string with 'show' and uses
 that to whiz up a TypeRep TyCon for 'n', with mkTypeLitTyCon.
 See #10348.

 Because of this rule it's inadvisable (see #15322) to have a constraint
     f :: (Typeable (n :: Nat)) => blah
 in a function signature; it gives rise to overlap problems just as
 if you'd written
     f :: Eq [a] => blah
 }}}
 Note the "inadvisable" part, which is what this ticket is about.  It just
 wasn't at all clear to me, and hence perhaps not to others.

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

_______________________________________________
ghc-tickets mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-tickets
Reply | Threaded
Open this post in threaded view
|

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

GHC - devs mailing list
In reply to this post by GHC - devs mailing list
#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

_______________________________________________
ghc-tickets mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-tickets
Reply | Threaded
Open this post in threaded view
|

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

GHC - devs mailing list
In reply to this post by GHC - devs mailing list
#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):

 Dispensing with `KnownNat` would be a worthwhile simplification.

 How would we implement `getNat`?  It might not be hard: just add an extra
 data constructor to `TyCon` perhaps.  But someone would have to think
 about it.

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

_______________________________________________
ghc-tickets mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-tickets
Reply | Threaded
Open this post in threaded view
|

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

GHC - devs mailing list
In reply to this post by GHC - devs mailing list
#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

_______________________________________________
ghc-tickets mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-tickets
Reply | Threaded
Open this post in threaded view
|

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

GHC - devs mailing list
In reply to this post by GHC - devs mailing list
#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):

 > Well, the evidence for KnownNat is just a simple integer, while the
 corresponding TypeRep is a much more heavy-weight structure

 That's a fair point.

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

_______________________________________________
ghc-tickets mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-tickets
Reply | Threaded
Open this post in threaded view
|

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

GHC - devs mailing list
In reply to this post by GHC - devs mailing list
#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 <simonpj@…>):

 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

_______________________________________________
ghc-tickets mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-tickets
Reply | Threaded
Open this post in threaded view
|

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

GHC - devs mailing list
In reply to this post by GHC - devs mailing list
#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 <simonpj@…>):

 In [changeset:"45f44e2c9d5db2f25c52abb402f197c20579400f/ghc" 45f44e2/ghc]:
 {{{
 #!CommitTicketReference repository="ghc"
 revision="45f44e2c9d5db2f25c52abb402f197c20579400f"
 Refactor validity checking for constraints

 There are several changes here.

 * TcInteract has gotten too big, so I moved all the class-instance
   matching out of TcInteract into a new module ClsInst. It parallels
   the FamInst module.

   The main export of ClsInst is matchGlobalInst.
   This now works in TcM not TcS.

 * A big reason to make matchGlobalInst work in TcM is that we can
   then use it from TcValidity.checkSimplifiableClassConstraint.
   That extends checkSimplifiableClassConstraint to work uniformly
   for built-in instances, which means that we now get a warning
   if we have givens (Typeable x, KnownNat n); see Trac #15322.

 * This change also made me refactor LookupInstResult, in particular
   by adding the InstanceWhat field.  I also changed the name of the
   type to ClsInstResult.

   Then instead of matchGlobalInst reporting a staging error (which is
   inappropriate for the call from TcValidity), we can do so in
   TcInteract.checkInstanceOK.

 * In TcValidity, we now check quantified constraints for termination.
   For example, this signature should be rejected:
      f :: (forall a. Eq (m a) => Eq (m a)) => blah
   as discussed in Trac #15316.   The main change here is that
   TcValidity.check_pred_help now uses classifyPredType, and has a
   case for ForAllPred which it didn't before.

   This had knock-on refactoring effects in TcValidity.
 }}}

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

_______________________________________________
ghc-tickets mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-tickets
Reply | Threaded
Open this post in threaded view
|

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

GHC - devs mailing list
In reply to this post by GHC - devs mailing list
#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

_______________________________________________
ghc-tickets mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-tickets
Reply | Threaded
Open this post in threaded view
|

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

GHC - devs mailing list
In reply to this post by GHC - devs mailing list
#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 goldfire):

 * cc: dotwani@… (added)


Comment:

 I really like the idea of domain-specific apartness. It's the perfect
 complement to the way that plugins can expand the equality relation, as my
 student Divesh (now in cc) and I have been exploring...

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

_______________________________________________
ghc-tickets mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-tickets
Reply | Threaded
Open this post in threaded view
|

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

GHC - devs mailing list
In reply to this post by GHC - devs mailing list
#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

_______________________________________________
ghc-tickets mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-tickets
Reply | Threaded
Open this post in threaded view
|

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

GHC - devs mailing list
In reply to this post by GHC - devs mailing list
#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):

 > 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

 Interesting. Another possibility would be to build into GHC more knowledge
 about `KnownNat`.

 But making it possible for plugins to specify apartness would also be
 good.

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

_______________________________________________
ghc-tickets mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-tickets
Reply | Threaded
Open this post in threaded view
|

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

GHC - devs mailing list
In reply to this post by GHC - devs mailing list
#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

_______________________________________________
ghc-tickets mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-tickets
Reply | Threaded
Open this post in threaded view
|

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

GHC - devs mailing list
In reply to this post by GHC - devs mailing list
#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):

 You are right, the issue mostly stems from the fact (I think? At least
 that is the most common problem where it all breaks down) that I can't
 convince the typechecker that things defined by induction (through 0 and
 (n+1)) are valid and hold for every n.

 I have no idea what the best technical solution would be. I am just a
 user. Here's a related issue: https://github.com/clash-lang/ghc-typelits-
 natnormalise/issues/13, which is very similar to the usual pains when I
 use type-level nats.

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

_______________________________________________
ghc-tickets mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-tickets
Reply | Threaded
Open this post in threaded view
|

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

GHC - devs mailing list
In reply to this post by GHC - devs mailing list
#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

_______________________________________________
ghc-tickets mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-tickets