Re: [GHC] #289: class context restrictions in GADT types not assumed

#289: class context restrictions in GADT types not assumed
----------------------------------------+-----------------------------------
    Reporter:  ashley-y                 |        Owner:  simonpj 
        Type:  bug                      |       Status:  assigned
    Priority:  normal                   |    Milestone:          
   Component:  Compiler (Type checker)  |      Version:  6.4     
    Severity:  normal                   |   Resolution:  None    
    Keywords:                           |   Difficulty:  Unknown 
Architecture:  Unknown                  |           Os:  Unknown 
----------------------------------------+-----------------------------------
Changes (by simonpj):

  * architecture:  => Unknown
  * difficulty:  => Unknown
  * os:  => Unknown

Old description:

> {{{
> I think this should compile:
>
>         class C a where
>                 f :: a -> Bool
>
>         data T a where
>                 MkT :: (C a) => a -> T a
>
>         tf1 :: T Int -> Bool
>         tf1 (MkT aa) = f aa
>
>         tf2 :: T a -> Bool
>         tf2 (MkT aa) = f aa
>
> tf1 does not give an error, but tf2 does. The type signature for tf2
> should not need a class context, just as there's no "C Int" instance.
>
> ThingEncoding.hs:32:23:
>     No instance for (C a)
>       arising from use of `f' at ThingEncoding.hs:32:23
>     Probable fix: Add (C a) to the type signature(s) for `tf2'
>     In the definition of `tf2': tf2 (MkT aa) = f aa
>
> }}}

New description:

 {{{
 I think this should compile:

         class C a where
                 f :: a -> Bool

         data T a where
                 MkT :: (C a) => a -> T a

         tf1 :: T Int -> Bool
         tf1 (MkT aa) = f aa

         tf2 :: T a -> Bool
         tf2 (MkT aa) = f aa

 tf1 does not give an error, but tf2 does. The type signature for tf2
 should not need a class context, just as there's no "C Int" instance.

 ThingEncoding.hs:32:23:
     No instance for (C a)
       arising from use of `f' at ThingEncoding.hs:32:23
     Probable fix: Add (C a) to the type signature(s) for `tf2'
     In the definition of `tf2': tf2 (MkT aa) = f aa

 }}}

Comment:

 Here is another example from Stephanie Weirich.

 The reason I want this feature is that I want to conditionally include a
 context for an existentially quantified type variable.
 In other words, I want the following code to work:
 ------------------------------------
 class Foo a where
   foo :: a -> Int

 data T = forall a. T (G a)

 data G a = A | Foo a => B a

 doFoo :: T -> Int
 doFoo (T A) = 2
 doFoo (T (B x)) = foo x

-- 
Ticket URL: <http://hackage.haskell.org/trac/ghc/ticket/289>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler_______________________________________________
Glasgow-haskell-bugs mailing list
Glasgow-haskell-bugs@xxxxxxxxxxx
http://www.haskell.org/mailman/listinfo/glasgow-haskell-bugs