[GHC] #2151: GADTs in function Patterns

[GHC]

#2151: GADTs in function Patterns
----------------------+-----------------------------------------------------
 Reporter:  hpacheco  |          Owner:  chak    
     Type:  bug       |         Status:  new     
 Priority:  normal    |      Milestone:          
Component:  Compiler  |        Version:  6.9     
 Severity:  blocker   |     Resolution:          
 Keywords:            |     Difficulty:  Unknown 
 Testcase:            |   Architecture:  Multiple
       Os:  Multiple  |  
----------------------+-----------------------------------------------------
Changes (by simonpj):

  * owner:  => chak
  * difficulty:  => Unknown

Old description:

> I have found a bug on the compiler (at least ghc >6.8.2). For some module
> (yes, the example does nothing at all):
>
> module Test where
>
> data Type a where
>     Func :: Type a -> Type b -> Type (a -> b)
>     PF :: Type a -> Type (PF a)
>
> data PF a where
>     ID :: PF (a -> a)
>
> test :: Type a -> a -> a
> test (PF (Func _ _)) ID = ID
>
> I get the impossible:
>
> $ ghci Test.hs -fglasgow-exts
> GHCi, version 6.9.20080303: http://www.haskell.org/ghc/  :? for help
> Loading package base ... linking ... done.
> [1 of 1] Compiling Test             ( Test.hs, interpreted )
> ghc-6.9.20080303: panic! (the 'impossible' happened)
>   (GHC version 6.9.20080303 for i386-apple-darwin):
>     Coercion.splitCoercionKindOf
>     $co${tc aog} [tv]
>     <pred>t_ao8{tv} [tau] ~ a{tv aob} [sk] -> a{tv aob} [sk]
> Please report this as a GHC bug:  http://www.haskell.org/ghc/reportabug
>
> However, the following implementations of test compiles ok:
>
> test :: Type a -> a -> a
> test (PF _) ID = ID
>
> test :: Type a -> a -> a
> test (PF (Func _ _)) x = x
>
> It has something to do with mixing different GADTs contructors.
>
> NOTE: This same code used to work fine in ghc 6.6, but I have ben told
> the whole GADT type checing was redone in 6.9. However, with 6.8.2 I
> still get the same error.

New description:

 I have found a bug on the compiler (at least ghc >6.8.2). For some module
 (yes, the example does nothing at all):
 {{{
 module Test where

 data Type a where
     Func :: Type a -> Type b -> Type (a -> b)
     PF :: Type a -> Type (PF a)

 data PF a where
     ID :: PF (a -> a)

 test :: Type a -> a -> a
 test (PF (Func _ _)) ID = ID
 }}}
 I get the impossible:
 {{{
 $ ghci Test.hs -fglasgow-exts
 GHCi, version 6.9.20080303: http://www.haskell.org/ghc/  :? for help
 Loading package base ... linking ... done.
 [1 of 1] Compiling Test             ( Test.hs, interpreted )
 ghc-6.9.20080303: panic! (the 'impossible' happened)
   (GHC version 6.9.20080303 for i386-apple-darwin):
     Coercion.splitCoercionKindOf
     $co${tc aog} [tv]
     <pred>t_ao8{tv} [tau] ~ a{tv aob} [sk] -> a{tv aob} [sk]
 Please report this as a GHC bug:  http://www.haskell.org/ghc/reportabug
 }}}
 However, the following implementations of test compiles ok:
 {{{
 test :: Type a -> a -> a
 test (PF _) ID = ID

 test :: Type a -> a -> a
 test (PF (Func _ _)) x = x
 }}}
 It has something to do with mixing different GADTs contructors.

 NOTE: This same code used to work fine in ghc 6.6, but I have ben told the
 whole GADT type checing was redone in 6.9. However, with 6.8.2 I still get
 the same error.

Comment:

 Indeed type inference is being changed a lot at the moment, by Manuel, so
 I'm assigning this to him.  Thanks very much fr a nice boiled-down
 example.

 Simon

-- 
Ticket URL: <http://hackage.haskell.org/trac/ghc/ticket/2151#comment:1>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler