Opened 5 months ago

Last modified 6 weeks ago

#15322 new bug

`KnownNat` does not imply `Typeable` any more when used with plugin

Reported by: chshersh Owned by:
Priority: normal Milestone: 8.8.1
Component: Compiler Version: 8.4.3
Keywords: typeable, knownnat, TypeCheckerPlugins Cc: diatchki, dotwani@…, adamgundry
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: GHC rejects valid program Test Case:
Blocked By: Blocking:
Related Tickets: #10348 Differential Rev(s):
Wiki Page:

Description

I have the following Haskell code which uses ghc-typelits-knownnat-0.5 package as a plugin:

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

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

Change History (20)

comment:1 Changed 5 months ago by simonpj

Cc: diatchki added

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

comment:2 Changed 5 months ago 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.

comment:3 Changed 5 months ago 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.

comment:4 Changed 5 months ago 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?

comment:5 Changed 5 months ago 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.

comment:6 Changed 5 months ago 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.

comment:7 Changed 5 months ago by goldfire

This seems unfortunate to me. I wonder if it would be better to have

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.

comment:8 Changed 5 months ago 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.

comment:9 Changed 5 months ago 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.

comment:10 Changed 5 months ago 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.

comment:11 Changed 5 months ago by Simon Peyton Jones <simonpj@…>

In 7ce6f642/ghc:

Add comments on Typeable (n :: Nat)

See Note [Typeable for Nat and Symbol] in TcInteract,
which I added after discussion on Trac #15322

comment:12 Changed 5 months ago by Simon Peyton Jones <simonpj@…>

In 45f44e2/ghc:

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.

comment:13 Changed 5 months ago 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.

comment:14 Changed 5 months ago by goldfire

Cc: dotwani@… added

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

comment:15 Changed 4 months ago 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!

comment:16 Changed 4 months ago 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.

comment:17 Changed 4 months ago 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.

comment:18 Changed 4 months ago 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.

comment:19 Changed 4 months ago by bgamari

Milestone: 8.6.18.8.1

These won't be fixed for in GHC 8.6.

comment:20 Changed 6 weeks ago by adamgundry

Cc: adamgundry added
Keywords: TypeCheckerPlugins added
Note: See TracTickets for help on using tickets.