#10450: Poor type error message when an argument is insufficently polymorphic -------------------------------------+------------------------------------- Reporter: sjcjoosten | Owner: Type: bug | Status: new Priority: low | Milestone: Component: Compiler (Type | Version: 7.8.2 checker) | Keywords: RankNTypes Resolution: | Architecture: Operating System: Unknown/Multiple | Unknown/Multiple Type of failure: GHC rejects | Test Case: valid program | Blocking: Blocked By: | Differential Revisions: Related Tickets: | -------------------------------------+------------------------------------- Old description:
When pattern matching, "let/where" and "case" have different behaviours. I believe this to be a bug, and my hope is that all of the following should be accepted.
Currently, this is accepted (a version using 'where' instead of 'let' type-checks too): {{{#!hs {-# LANGUAGE RankNTypes, ScopedTypeVariables #-} module Main where
data Phantom x = Phantom Int deriving Show
foo :: forall y. (forall x. (Phantom x)) -> Phantom y foo (Phantom x) = Phantom (x+1) -- trying to map foo over a list, this is the only way I can get it to work typeAnnotatedMap :: (forall x. [Phantom x]) -> [Phantom y] typeAnnotatedMap intList = case intList of [] -> [] _ -> let (phead:ptail) = intList in foo phead : typeAnnotatedMap ptail }}}
The following are not accepted: {{{#!hs typeAnnotatedMap :: (forall x. [Phantom x]) -> [Phantom y] typeAnnotatedMap intList = case intList of [] -> [] (phead:ptail) -> foo phead : typeAnnotatedMap ptail
typeAnnotatedMap :: (forall x. [Phantom x]) -> [Phantom y] typeAnnotatedMap [] = [] typeAnnotatedMap (phead:ptail) = foo phead : typeAnnotatedMap ptail }}}
The switches "ImpredicativeTypes" and "NoImpredicativeTypes" only change GHC's behaviour in the following example, for which I understand (but don't like) that it is not accepted, its error message is fine: {{{#!hs typeAnnotatedMap :: (forall x. [Phantom x]) -> [Phantom y] typeAnnotatedMap lst = map foo lst }}}
Tested this on 7.8.2. Version 7.6.3 and 7.4.2 seem to behave the same. Sorry for not testing this on the latest version.
Should this not be a bug, it would help if the type checker would somehow point me in the direction of the solution (first version) when I write any one of the 'problem cases'. The current type error is something like: {{{ Couldn't match type ‘x0’ with ‘x’ because type variable ‘x’ would escape its scope This (rigid, skolem) type variable is bound by a type expected by the context: [Phantom x] }}} More helpful would be something like:
{{{ Your pattern match bound the following types to a shared skolem variable: ptail :: [Phantom x0] (bound at rankNtest.hs:11:25) phead :: Phantom x0 (bound at rankNtest.hs:11:19) You may have intended to use a "let" or "where" pattern-match instead. }}}
New description: When pattern matching, "let/where" and "case" have different behaviours. I believe this to be a bug, and my hope is that all of the following should be accepted. Currently, this is accepted (a version using 'where' instead of 'let' type-checks too): {{{#!hs {-# LANGUAGE RankNTypes, ScopedTypeVariables #-} module Main where data Phantom x = Phantom Int deriving Show foo :: forall y. (forall x. (Phantom x)) -> Phantom y foo (Phantom x) = Phantom (x+1) -- trying to map foo over a list, this is the only way I can get it to work typeAnnotatedMap :: (forall x. [Phantom x]) -> [Phantom y] typeAnnotatedMap intList = case intList of [] -> [] _ -> let (phead:ptail) = intList in foo phead : typeAnnotatedMap ptail }}} The following are not accepted: {{{#!hs typeAnnotatedMap1 :: (forall x. [Phantom x]) -> [Phantom y] typeAnnotatedMap1 intList = case intList of [] -> [] (phead:ptail) -> foo phead : typeAnnotatedMap1 ptail typeAnnotatedMap2 :: (forall x. [Phantom x]) -> [Phantom y] typeAnnotatedMap2 [] = [] typeAnnotatedMap2 (phead:ptail) = foo phead : typeAnnotatedMap2 ptail }}} The switches "ImpredicativeTypes" and "NoImpredicativeTypes" only change GHC's behaviour in the following example, for which I understand (but don't like) that it is not accepted, its error message is fine: {{{#!hs typeAnnotatedMap :: (forall x. [Phantom x]) -> [Phantom y] typeAnnotatedMap lst = map foo lst }}} Tested this on 7.8.2. Version 7.6.3 and 7.4.2 seem to behave the same. Sorry for not testing this on the latest version. Should this not be a bug, it would help if the type checker would somehow point me in the direction of the solution (first version) when I write any one of the 'problem cases'. The current type error is something like: {{{ Couldn't match type ‘x0’ with ‘x’ because type variable ‘x’ would escape its scope This (rigid, skolem) type variable is bound by a type expected by the context: [Phantom x] }}} More helpful would be something like: {{{ Your pattern match bound the following types to a shared skolem variable: ptail :: [Phantom x0] (bound at rankNtest.hs:11:25) phead :: Phantom x0 (bound at rankNtest.hs:11:19) You may have intended to use a "let" or "where" pattern-match instead. }}} -- Comment (by simonpj): Why don't you write {{{ typeAnnotatedMap :: (forall x. [Phantom x]) -> [Phantom y] typeAnnotatedMap x = x }}} which works just fine? To answer your specific question, `let` does generalisation, while `case` does not. * In `typeAnnotatedMap`, the type of `ptail` is generalised (by the `let`) to `forall a. [Phantom a]`. So the `typeAnnotatedMap` has an argument that is sufficiently polymorphic. * In `typeAnnotatedMap1`, the type of `ptail` is `[Phantom x0]`, where the call to `intList` (in `case intList of...`) is instantiated at type `x0`. But that means that the call `typeAnnotatedMap1 ptail` fails, because the type of `ptail` is insufficiently polymorphic. So I don't think this is a bug. I grant that error messags for insufficiently-polymorphic arguments are not good; so I'll leave this ticket open for that treason, with a new title. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10450#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler