#4385: Type-level natural numbers
----------------------------------------+-----------------------------------
Reporter: diatchki | Owner: diatchki
Type: feature request | Status: new
Priority: normal | Milestone: 7.2.1
Component: Compiler (Type checker) | Version:
Keywords: | Testcase:
Blockedby: | Difficulty:
Os: Unknown/Multiple | Blocking:
Architecture: Unknown/Multiple | Failure: None/Unknown
----------------------------------------+-----------------------------------
Comment(by diatchki):
Hello,
For the moment, there is no support for ad-hoc proofs. The problem you
describe might occur when GHC encounters a type signature but it cannot
show that the context of the type signature is sufficient to justify the
function's implementation. As you say, this may be because GHC does not
know enough math. In this case, one would have to either change (or
remove) the type signature, or change the implementation (and, if the
inference seems obvious, then send an e-mail to the GHC list so that we
can teach GHC some more math :-).
{{{unsafeCoerce}}} works as usual but I've never had to use it because,
usually, there is something different one can do. For example, the array
indexes that you mentioned use type-nats as a phantom type only, so the
library could provide arbitrary coercion functions, including something
based on manual evidence construction, but I have not really thought about
that.
--
Ticket URL: <http://hackage.haskell.org/trac/ghc/ticket/4385#comment:16>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler
_______________________________________________
Glasgow-haskell-bugs mailing list
Glasgow-haskell-bugs@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-bugs
