I can't figure out why the following code doesn't compile with the October 2n GHC 6.10 beta (-XTypeFamilies -XFlexibleContexts) when the type declaration is not commented out. module T where type family RangeTrait c class InputRange r where remaining :: r -> Bool advance :: r -> r class (InputRange (RangeTrait s)) => Sequence s where erase :: RangeTrait s -> IO (RangeTrait s) -- erase_range :: (Sequence s) => RangeTrait s -> IO (RangeTrait s) erase_range r = if remaining r then do r' <- erase r erase_range r' else return r GHCi says the type is precisely as specified in the comment. However, when I activate the type declaration, GHC complains: T.hs:16:22: Couldn't match expected type `RangeTrait s' against inferred type `RangeTrait s2' In the first argument of `erase', namely `r' In a stmt of a 'do' expression: r' <- erase r In the expression: do r' <- erase r erase_range r' T.hs:17:22: Couldn't match expected type `RangeTrait s1' against inferred type `RangeTrait s2' In the first argument of `erase_range', namely `r'' In the expression: erase_range r' In the expression: do r' <- erase r erase_range r' Any suggestions? Is this a bug in GHC?
-- erase_range :: (Sequence s) => RangeTrait s -> IO (RangeTrait s)
This can't work, as you can see after desugaring:
-- erase_range :: (Sequence s,RangeTrait s~rs) => rs -> IO rs
There is nowhere to get 's' from, unless you start applying type families backwards, from results to parameters.
type family RangeTrait c class (InputRange (RangeTrait s)) => Sequence s where erase :: RangeTrait s -> IO (RangeTrait s)
Perhaps this shouldn't be accepted, or should trigger a warning. In the class declaration, and in any instance definitions, 's' will be bound in the head, so seems to be known locally, but 's' won't be known in any use of 'erase' outside the class declaration/instance definition. The only way to make 's' known to 'erase' would be via '{-# LANGUAGE ScopedTypeVariables #-}'.
-- erase_range :: (Sequence s) => RangeTrait s -> IO (RangeTrait s) erase_range r = if remaining r then do r' <- erase r erase_range r' else return r
GHCi says the type is precisely as specified in the comment.
That (the inference result) does look like a bug, since 's' is bound locally, but not linked to any object that could fix it. The error message should mention the hoped-for type, and the reason why that type won't work. Which 's' did you want 'erase_range' to use to select an instance of 'Sequence'? If you absolutely insist on that type, you could move the function into the class, but then it will be just as difficult to use as 'erase'. Btw, is there a list of common TF pitfalls somewhere? Some example items so far seem to be: 1 'C a => TF a', where 'a' isn't determinable 2 'TF a' is not fully polymorphic 3 'TF a' is not a decomposable type constructor, it stands only for itself, or for its result (in that way it is more like a defined function application) For 1/2, it is helpful to flatten type family applications: - 'C a => TF a' becomes: '(C a,TF a~tfa) => tfa' - 'TF a' becomes: 'TF a~tfa => tfa' For 3, it is helpful to imagine the arity of type families being marked by braces, to distinguish type family parameters from any constructor parameters, in case the type family reduces to a type constructor: - Given 'type family TF2 a :: * -> *', 'TF2 a b' becomes: '{TF2 a} ~ tfa => tfa b' Claus
Claus Reinke wrote:
Btw, is there a list of common TF pitfalls somewhere? Some example items so far seem to be:
1 'C a => TF a', where 'a' isn't determinable 2 'TF a' is not fully polymorphic 3 'TF a' is not a decomposable type constructor, it stands only for itself, or for its result (in that way it is more like a defined function application)
For 1/2, it is helpful to flatten type family applications:
- 'C a => TF a' becomes: '(C a,TF a~tfa) => tfa' - 'TF a' becomes: 'TF a~tfa => tfa'
For 3, it is helpful to imagine the arity of type families being marked by braces, to distinguish type family parameters from any constructor parameters, in case the type family reduces to a type constructor:
- Given 'type family TF2 a :: * -> *', 'TF2 a b' becomes: '{TF2 a} ~ tfa => tfa b'
It should rather be a type-level programming FAQ: Re 1: Ambiguous signatures are a general problem. However, they are syntactically harder to recognise with TFs. Re 2: Applies to GADTs as well. Re 3: I have always been wondering whether we want special syntax for the application of synonym families. That would make it syntactically easier to recognise ambiguous signatures and indicarte syntactically were decomposition is admisible. BTW, part of the problem is that H98 is not entirely consistent with its use of upper and lower case identifiers. Strictly speaking, already vanilla type synonyms should have been lower case as they are a simple form of functions on types (you cannot use decomposition on them!) Then, synonym families could be lower-case, too. Manuel
* Claus Reinke:
-- erase_range :: (Sequence s) => RangeTrait s -> IO (RangeTrait s)
This can't work, as you can see after desugaring:
-- erase_range :: (Sequence s,RangeTrait s~rs) => rs -> IO rs
There is nowhere to get 's' from, unless you start applying type families backwards, from results to parameters.
Thanks. Indeed, this is a bug in my reading of the specification (and the original even had that Sequence argument). I was led astray by the fact that the type checker accepted the class declaration, even though there's no really good way to provide a concrete implementation. Another example I encountered is this: class Foo f where foo :: f -> g -- oops, typo It was very difficult for me to spot this one, too. 8-/
Florian Weimer:
I can't figure out why the following code doesn't compile with the October 2n GHC 6.10 beta (-XTypeFamilies -XFlexibleContexts) when the type declaration is not commented out.
It's a bug that the code is accepted *without* the signature, as the signature is ambiguous: http://hackage.haskell.org/trac/ghc/ticket/1897 This is not because the code fails to be type-safe, but because (a) you can't use the function erase_range anyway and (b) that it is accepted without a signature, but not with the signature leads to confusion, as you experienced. BTW, the method 'erase' in your code has the same problem. Manuel
module T where
type family RangeTrait c
class InputRange r where remaining :: r -> Bool advance :: r -> r
class (InputRange (RangeTrait s)) => Sequence s where erase :: RangeTrait s -> IO (RangeTrait s)
-- erase_range :: (Sequence s) => RangeTrait s -> IO (RangeTrait s) erase_range r = if remaining r then do r' <- erase r erase_range r' else return r
GHCi says the type is precisely as specified in the comment. However, when I activate the type declaration, GHC complains:
T.hs:16:22: Couldn't match expected type `RangeTrait s' against inferred type `RangeTrait s2' In the first argument of `erase', namely `r' In a stmt of a 'do' expression: r' <- erase r In the expression: do r' <- erase r erase_range r'
T.hs:17:22: Couldn't match expected type `RangeTrait s1' against inferred type `RangeTrait s2' In the first argument of `erase_range', namely `r'' In the expression: erase_range r' In the expression: do r' <- erase r erase_range r'
Any suggestions? Is this a bug in GHC? _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
participants (3)
-
Claus Reinke -
Florian Weimer -
Manuel M T Chakravarty