[GHC] #7849: Error on pattern matching of an existential whose context includes a type function

[GHC]

#7849: Error on pattern matching of an existential whose context includes a type
function
-----------------------------+----------------------------------------------
Reporter:  guest             |          Owner:                         
    Type:  bug               |         Status:  new                    
Priority:  normal            |      Component:  Compiler (Type checker)
 Version:  7.4.2             |       Keywords:                         
      Os:  Unknown/Multiple  |   Architecture:  Unknown/Multiple       
 Failure:  None/Unknown      |      Blockedby:                         
Blocking:                    |        Related:                         
-----------------------------+----------------------------------------------
 The following code
 {{{
 {-# LANGUAGE TypeFamilies #-}
 {-# LANGUAGE ExistentialQuantification #-}
 {-# LANGUAGE GADTs #-}

 module Ex where

 import Data.IORef

 class SUBJ subj where
     type SUBJ_Obs subj :: *
     unsubscribe' :: subj -> SUBJ_Obs subj -> IO ()

 data ASubj obs = forall subj. (SUBJ subj, SUBJ_Obs subj ~ obs) => ASubj
 subj
 -- data ASubj obs = forall subj. (SUBJ subj) => ASubj subj (obs ->
 SUBJ_Obs subj)

 class OBS obs where
     subscribed :: obs -> ASubj obs -> IO ()
     withdraw   :: obs -> IO ()

 -- The implementation of Obs
 data Obs = Obs{obs_subjects :: IORef [ASubj Obs]}

 instance OBS Obs where
     subscribed obs subj = modifyIORef (obs_subjects obs) (subj:)
     withdraw obs = do
       subjs <- readIORef (obs_subjects obs)
       writeIORef (obs_subjects obs) []
       mapM_ (\ (ASubj subj) -> unsubscribe' subj obs) subjs
 --    mapM_ (\ (ASubj subj cast) -> unsubscribe' subj (cast obs)) subjs

 }}}
 gives a rather obscure type error

 {{{
     Couldn't match type `b0' with `()'
       `b0' is untouchable
            inside the constraints (SUBJ subj, SUBJ_Obs subj ~ Obs)
            bound at a pattern with constructor
                       ASubj :: forall obs subj.
                                (SUBJ subj, SUBJ_Obs subj ~ obs) =>
                                subj -> ASubj obs,
                     in a lambda abstraction
     In the pattern: ASubj subj
     In the first argument of `mapM_', namely
       `(\ (ASubj subj) -> unsubscribe' subj obs)'
     In a stmt of a 'do' block:
       mapM_ (\ (ASubj subj) -> unsubscribe' subj obs) subjs
 -}
 }}}
 It is not even clear what b0 is: the code has no type variable named b.
 Incidentally, if I use the explicit cast (as in the commented out
 declaration of ASubj) and change the last line of withdraw accordingly (as
 shown in the commented out line), the code compiles.
 It seems that what I am trying to accomplish is reasonable.

 Incidentally, why GHC insists on the extension GADTs given that I already
 specified ExistentialQuantification? It seems when opening amn existential
 GADTs extension must be present. It seems ExistentialQuantification no
 longer has any point?

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