[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:  patch
        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):  Phab:D4988
       Wiki Page:                    |
-------------------------------------+-------------------------------------

Comment (by ppk):

 Replying to [comment:12 ezyang]:
 > Piyush, I don't think the behavior of your example is consistent with
 the hypothesis. Consider the following program:
 >
 > {{{
 > {-# LANGUAGE DataKinds, KindSignatures #-}
 > unit p where
 >   signature Abstract where
 >     import GHC.TypeLits
 >     data Foo :: Nat
 >     instance KnownNat Foo
 >
 >   module Util where
 >     import Data.Proxy
 >     import Abstract
 >     import GHC.TypeLits
 >     foo = natVal (Proxy :: Proxy Foo)
 >
 > }}}

 Yes I realised it yesterday when I went back and tested with a similar
 example. In the backpack case, the comment:4 is the correct analysis: we
 know that the type T in question has a `KnownNat` instance but cannot find
 its dictionary. Unfortunately the error it triggers is not a cannot find
 instance but the following.

 <https://github.com/piyush-
 kurur/ghc/blame/55a3f8552c9dc9b84e204ec6623c698912795347/compiler/typecheck/TcErrors.hs#L2484-L2501>

 (Notice the match on null `match_given` in that code).

 This also explains why the cleanup suggested by @simonpj works because
 `matchKnownNat` now does
 not try generating instances on the fly and fails but actually looks up
 the environment. The real explanation therefore looks like an unfortunate
 error message and the explanation
 in comment:4 is the correct one.

 Please let me know if this real explanation makes sense ;-)

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