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

19 Jul 2018

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

 }}}

 I get:

 {{{
 ezyang@autobox:~/Dev/ghc-known-nat$ inplace/bin/ghc-stage2 --backpack
 test.bkp -fforce-recomp
 [1 of 1] Processing p
   [1 of 2] Compiling Abstract[sig]    ( p/Abstract.hsig, nothing )
   [2 of 2] Compiling Util             ( p/Util.hs, nothing )

 test.bkp:12:11: error:
     • Overlapping instances for KnownNat Foo
         arising from a use of ‘natVal’
       Matching instances:
         instance [safe] KnownNat Foo -- Defined at test.bkp:6:14
       There exists a (perhaps superclass) match:
       (The choice depends on the instantiation of ‘’
        To pick the first instance above, use IncoherentInstances
        when compiling the other instance declarations)
     • In the expression: natVal (Proxy :: Proxy Foo)
       In an equation for ‘foo’: foo = natVal (Proxy :: Proxy Foo)
    |
 12 |     foo = natVal (Proxy :: Proxy Foo)
    |           ^^^^^^^^^^^^^^^^^^^^^^^^^^^

 }}}

 The overlap occurs before Concrete is considered at all.

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