Re: [GHC] #10134: Pattern Matching Causes Infinite Type Error

4 Mar 2015

      #10134: Pattern Matching Causes Infinite Type Error
-------------------------------------+-------------------------------------
        Reporter:  dongen            |                   Owner:
            Type:  bug               |                  Status:  new
        Priority:  normal            |               Milestone:
       Component:  Compiler          |                 Version:  7.8.4
      Resolution:                    |                Keywords:
Operating System:  Unknown/Multiple  |            Architecture:
 Type of failure:  None/Unknown      |  Unknown/Multiple
      Blocked By:                    |               Test Case:
 Related Tickets:                    |                Blocking:
                                     |  Differential Revisions:
-------------------------------------+-------------------------------------

Comment (by dongen):

 OK. I've managed to trim down the problem to a few lines.

 I'm including the contents of three files (it wasn't clear how to attach).
 Dummy1, which mainly contains type definitions that are needed in my real
 modules, Dummy2, which contains a datatype and a function, the type of
 which ``causes'' the problem, and Dummy3, which has the bug.

 If you compile Dummy3, you get an error. If you comment that line out and
 uncomment the three previous lines, you'll see that all is fine.

 In short, I wouldn't expect this behaviour (but I haven't programmed in
 Haskell for a long time).

 {{{
...
-- Dummy1.lhs
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
...
module Dummy1( Dummy1, Exponential, Positive ) where
import CLaSH.Prelude
...
data Dummy1 n a = Dummy1
    { tree :: Vec n a -- | The converging computation.
    } deriving Show
...
type Exponential n
    = ( Positive n
      , KnownNat (2^n)
      , KnownNat ((2^n)-1)
      , KnownNat ((2^n)-2)
      , KnownNat ((2^(n-1))+((2^(n-1))-1))
      , (((2^n)-1)+1)~(2^n)
      , (((2^n)-2)+1)~((2^n)-1)
      , ((2^(n-1)-1)*2)~(2^n-2)
      , (2^n-2+1)~((2^(n-1))+((2^(n-1))-1))
      , (((2^(n-1))+((2^(n-1))-1))*2)~((2^n)+((2^n)-2))
      )
...
type Positive n
    = ( KnownNat n
      , KnownNat (n-1)
      , ((n-1)+1)~n
      )
}}}
 {{{
...
-- Dummy2.lhs
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE AllowAmbiguousTypes #-}
...
module Dummy2( Dummy2, nextDummy2 ) where
...
import CLaSH.Prelude
import Dummy1
...
-- |  Data type for arc consistency convergence circuit
-- |  * The delay of the circuit is @2*(n+d)@.
data Dummy2 n d = Dummy2
   { dummy :: Vec ((n+d)) Bool
   } deriving Show
...
nextDummy2
    :: ( KnownNat n
       , KnownNat d
       , Exponential (n+d)
       , Positive (2*(n+d))
       )
    => Dummy2 n d
    -> ( Dummy2 n d, Bool )
nextDummy2 cv = error []
}}}

 {{{
...
-- Dummy3.lhs
{-# LANGUAGE MultiParamTypeClasses #-}
...
module Dummy3( Dummy3 ) where
...
import CLaSH.Prelude
import Dummy1
import Dummy2
...
data Dummy3 n d = Dummy3
   { dummy2 :: Dummy2 n d
   } deriving Show
...
nextDummy3
    :: (
         Exponential d
       , Exponential n
       , Exponential (n+d)
       , Positive (2*(n+d))
       , ((2^n)*(2^d))~(2^(n+d))
       )
    => Dummy3 n d -> Dummy3 n d
nextDummy3 ac
   = Dummy3 { dummy2 = dummyFst }
   where -- dummy2' = nextDummy2 (dummy2 ac)
         -- dummyFst = fst dummy2'
         -- dummySnd = snd dummy2'
         (dummyFst,dummySnd) = nextDummy2 (dummy2 ac)
--
Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10134#comment:4
GHC http://www.haskell.org/ghc/
The Glasgow Haskell Compiler