[GHC] #7849: Error on pattern matching of an existential whose context includes a type function
#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
#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: -----------------------------+---------------------------------------------- Comment(by goldfire): I agree that this is an obscure type error and needs some attention, but the needs for {{{-XGADTs}}} is sensible to me, here. After all, your {{{ASubj}}} datatype is a GADT, albeit using weird syntax. The prototypical GADT is like this: {{{ data Foo a where FInt :: Foo Int }}} But, you could write that same datatype like this: {{{ data Foo a = (a ~ Int) => FInt }}} A GADT really is just a normal datatype with equality constraints on its parameter(s). So, pattern matching on such a datatype should indeed require {{{-XGADTs}}}. -- Ticket URL: http://hackage.haskell.org/trac/ghc/ticket/7849#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
participants (1)
-
GHC