#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

#10450: Poor type error message when an argument is insufficently polymorphic -------------------------------------+------------------------------------- Reporter: sjcjoosten | Owner: Type: task | 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 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. }}}

New description: When pattern matching, "let/where" and "case" have different behaviours. 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 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 sjcjoosten): I already emailed this comment, but it did not show up in trac, so I am adding it again (sorry for cross-posting) I agree that there is no bug. To follow up on writing a simpler version (your version does not work, because it does not map "foo"), it can be done using impredicative types, and the helper function "bar": {{{#!hs bar :: (forall x. [Phantom x]) -> [forall x. Phantom x] bar [] = [] bar lst = help h ++ bar tl where (h:tl) = lst help :: (forall x. Phantom x) -> [forall x. Phantom x] help (Phantom x) = [Phantom x] typeAnnotatedMap3 :: forall y. (forall x. [Phantom x]) -> [Phantom y] typeAnnotatedMap3 lst = map foo (bar lst) }}} I don't use Impredicative types because I do not understand them. For example, I don't get why this won't typecheck (bar does the same): {{{#!hs bar2 :: (forall x. [Phantom x]) -> [forall x. Phantom x] bar2 [] = [] bar2 lst = help h : bar2 tl where (h:tl) = lst help :: (forall x. Phantom x) -> forall x. Phantom x help (Phantom x) = Phantom x }}} Since we're improving error messages in this ticket, I would really like to know why the skolemn variable {{{x0}}} (probably arising from {{{forall x. Phantom x}}}) could not be matched to {{{forall x. Phantom x}}}, but the only error I got was: {{{ Couldn't match expected type ‘forall x. Phantom x’ with actual type ‘Phantom x0’ In the first argument of ‘(:)’, namely ‘help h’ In the expression: help h : bar tl }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10450#comment:3 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler