[GHC] #10450: Poor type error message when an argument is insufficently polymorphic (was: RankNTypes type check on pattern match of "let" behaves different from "case")

[GHC]

#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