GHC currently takes the following (non-Haskell 98) attitude to type synonyms: first expand type synonyms only then check for partial applications of type synonyms then perform type checking So in his case type for f expands to: f :: m () -> m () test :: Int -> Int You can see how the type for test comes out: Thing (Const Int) = Const Int () = Int Now GHC tries to unify m () with Int and fails, as it should. The error message is phrased in terms of the original un-expanded types, which is usually a good thing but on this occasion gives a rather odd looking error message. GHC shouldn't really do this lazy checking unless you say -fglasgow-exts Simon | -----Original Message----- | From: Samuel E. Moelius III [mailto:usmoeliu@mcs.drexel.edu] | Sent: 04 May 2002 20:45 | To: haskell-cafe@haskell.org | Subject: Using "type" | | | I apologize if this question has been asked before... | | It seems to me the following code should be legal: | | type Thing m = m () | | type Const a b = a | | f :: Thing m -> Thing m | f x = x | | test :: Thing (Const Int) -> Thing (Const Int) | test = f | | However, GHC gives the following error: | | Couldn't match `Thing m' against `Thing (Const Int)' | Expected type: Thing m | Inferred type: Thing (Const Int) | Expected type: Thing (Const Int) -> Thing (Const Int) | Inferred type: Thing m -> Thing m | | But if you change the definition of Const | | newtype Const a b = MakeConst a | | the code compiles fine. | | Is this the desired behavior? | | Is it the case that when you have quantification of a type | variable of | kind * -> * (in this case, m), that variable may only become | bound to a | type constructor? | | Sam Moelius | | _______________________________________________ | Haskell-Cafe mailing list | Haskell-Cafe@haskell.org | http://www.haskell.org/mailman/listinfo/haskell-cafe |