[GHC] #15379: Don't reject user-written instances of KnownNat and friends in hsig files

[GHC]

#15379: Don't reject user-written instances of KnownNat and friends in hsig files
-------------------------------------+-------------------------------------
        Reporter:  ezyang            |                Owner:  (none)
            Type:  bug               |               Status:  new
        Priority:  normal            |            Milestone:  8.6.1
       Component:  Compiler          |              Version:  8.4.3
      Resolution:                    |             Keywords:  backpack
Operating System:  Unknown/Multiple  |         Architecture:
                                     |  Unknown/Multiple
 Type of failure:  None/Unknown      |            Test Case:
      Blocked By:                    |             Blocking:
 Related Tickets:                    |  Differential Rev(s):
       Wiki Page:                    |
-------------------------------------+-------------------------------------

Comment (by ppk):

 Replying to [comment:7 simonpj]:
 > The current implementation only ever has instances for `KnownNat 1`,
 `KnownNat 2` etc.  This is described in `Note [KnownNat & KnownSymbol and
 EvLit]` in `TcInteract`.
 >

 Yes that note was quite useful in fact.

 > But now you want to allow `instance KnownNat T` for some abstract type
 `T`; you explain this well in comment:4.
 >
 > Very well; but I really dislike messing with `matchInstEnv`.  Better:
 make `mathKnownNat` have an `otherwise` case that, instead of returning
 `NoInstance` uses `matchInstEnv`.  With  a careful `Note` to explain.
 >

 Okey I will think about it and try it out. The only thing puzzling for me
 is that the old code is returning Overlapping instances, which to me
 appears to be finding too many instances rather than finding too few. So
 there is some problem with my comment:4 which I cannot really pin-point.

 > [snip]
 >
 > But `Typeable` can fail; I wonder if you might end up wanting a
 `Typeable` instance in a `hsig` file.  I think that's all... but the big
 point is that GHC's treatment of built-in classes may need attention
 because of Backpack; KnownNat is just an example.

 Again the `Typeable` instances in backpack works fine //even with the old
 version// of the code (unlike `KnownNat` or `KnownSymbol`). In fact, I
 realised and has tweaked the test case to have all
 the three problematic classes (KnownNat, KnownSymbol and Typeable) but
 only the first two was giving
 the overlapping instance error.

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