Piyush, I don't think the behavior of your example is consistent with
#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]: 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