[GHC] #9273: TypeNats and record syntax don't compile
GHC
ghc-devs at haskell.org
Sun Jul 6 00:17:34 UTC 2014
#9273: TypeNats and record syntax don't compile
----------------------------------------------+----------------------------
Reporter: br1 | Owner:
Type: bug | Status: closed
Priority: normal | Milestone:
Component: Compiler (Type checker) | Version: 7.8.2
Resolution: invalid | Keywords:
Operating System: Unknown/Multiple | Architecture:
Type of failure: GHC rejects valid program | Unknown/Multiple
Test Case: | Difficulty: Unknown
Blocking: | Blocked By:
| Related Tickets:
----------------------------------------------+----------------------------
Changes (by rwbarton):
* status: new => closed
* resolution: => invalid
Comment:
That's because record syntax additionally defines an accessor function
{{{
sNatPred :: SNat (n+1) -> SNat n
sNatPred (SNatS x) = x
}}}
which you cannot define manually using the non-record syntax `SNat`
either. As the error message says, GHC does not (yet) know that `n+1`
determines `n`, so it cannot type check the above definition because as
far as it is concerned, `x` might have type `SNat n1` for some other `n1`
with `n1+1 = n+1`. Once the Nat solver is improved, your record syntax
`SNat` should compile.
--
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/9273#comment:1>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler
More information about the ghc-tickets
mailing list