#12882: Unexpected constraint when using ExistentialQuantification -------------------------------------+------------------------------------- Reporter: danilo2 | Owner: Type: bug | Status: new Priority: high | Milestone: Component: Compiler (Type | Version: 8.0.1 checker) | Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by mpickering): Can you paste your whole file please? It isn't clear which extensions you have turned on to get the first example to compile. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12882#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#12882: Unexpected constraint when using ExistentialQuantification -------------------------------------+------------------------------------- Reporter: danilo2 | Owner: Type: bug | Status: closed Priority: normal | Milestone: Component: Compiler (Type | Version: 8.0.1 checker) | Resolution: invalid | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by mpickering): OK - I got it to compile now, I was missing scoped type variables. Here is the more usual way to write your data type. {{{ {-# LANGUAGE ExistentialQuantification #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE GADTs #-} import Data.Typeable data Elem t where Elem :: Typeable t => Int -> Elem t tst1 :: forall a. Elem a -> TypeRep tst1 (Elem _) = typeRep (Proxy :: Proxy a) }}} Then it is clear why you must pattern match on `Elem` in order to discover that you have the `Typeable` constraint. You could have another constructor which doesn't bind it. For example, {{{ data Elem t where Elem :: Typeable t => Int -> Elem t Elem2 :: t -> Elem t }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12882#comment:3 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#12882: Unexpected constraint when using ExistentialQuantification -------------------------------------+------------------------------------- Reporter: danilo2 | Owner: Type: bug | Status: closed Priority: normal | Milestone: Component: Compiler (Type | Version: 8.0.1 checker) | Resolution: invalid | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by rwbarton): But presumably the reason you want the type checker to know `t` is an instance of `Typeable` is in order to use functions which use the constraint, like `typeRep`. And the `Typeable t` dictionary is exactly what will be used at runtime to implement that function. So, there is no getting around the need for the dictionary, either passed into your function as a constraint `Typeable t =>` or unpacked from the data as in `tst1`. (I'm a bit confused how you think this could work at runtime. Maybe you are imagining that a function receives information about its type parameters at runtime and could use that data to look up the needed `Typeable` instance in some global table? Actually, there is no type data at runtime aside from what you explicitly introduce in the form of `Typeable` contexts nor any table of instances. And even `Typeable` is not that special, and could be reimplemented to some extent by a used-defined class.) -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12882#comment:5 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#12882: Unexpected constraint when using ExistentialQuantification -------------------------------------+------------------------------------- Reporter: danilo2 | Owner: Type: bug | Status: closed Priority: normal | Milestone: Component: Compiler (Type | Version: 8.0.1 checker) | Resolution: invalid | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by rwbarton): Well there is no problem if you write `data` instead of `newtype`, above. But of course the `Foo a` dictionary must be stored within an `ImplicitFoo a`, so that it can provide the implementation of `foo` at runtime. You cannot think of the constraint `Foo a` as a box to be checked off to satisfy some bureaucratic type checker. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12882#comment:7 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler