Looping with type level naturals
When compiling the code below, I run into an error with GHC 7.10.1:
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE EmptyDataDecls #-}
{-# LANGUAGE ExplicitNamespaces #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE TypeOperators #-}
module Loop ( ) where
import Data.Type.Equality ( (:~:)(Refl) )
import Prelude (Maybe(..), undefined)
import GHC.TypeLits ( Nat, type (<=))
data V (n::Nat)
testEq :: (m <= n) => V m -> V n -> Maybe (m :~: n)
testEq = undefined
uext :: (1 <= m, m <= n) => V m -> V n -> V n
uext e w =
case testEq e w of
Just Refl -> e
The error I get in GHC 7.10.1 is:
% ghc -c Loop.hs
Loop.hs:21:9:
Context reduction stack overflow; size = 102
Use -fcontext-stack=N to increase stack size to N
(1 GHC.TypeLits.<=? n) ~ 'GHC.Types.True
GHC 7.8.4 compiles this without errors.
Trac metadata
Trac field | Value |
---|---|
Version | 7.10.1 |
Type | Bug |
TypeOfFailure | OtherFailure |
Priority | normal |
Resolution | Unresolved |
Component | Compiler |
Test case | |
Differential revisions | |
BlockedBy | |
Related | |
Blocking | |
CC | |
Operating system | MacOS X |
Architecture | x86_64 (amd64) |