Error on pattern matching of an existential whose context includes a type function
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?
Trac metadata
Trac field | Value |
---|---|
Version | 7.4.2 |
Type | Bug |
TypeOfFailure | OtherFailure |
Priority | normal |
Resolution | Unresolved |
Component | Compiler (Type checker) |
Test case | |
Differential revisions | |
BlockedBy | |
Related | |
Blocking | |
CC | oleg@okmij.org |
Operating system | |
Architecture |