[GHC] #10450: RankNTypes type check on pattern match of "let" behaves different from "case"

[GHC]

#10450: RankNTypes type check on pattern match of "let" behaves different from
"case"
-------------------------------------+-------------------------------------
              Reporter:  sjcjoosten  |             Owner:
                  Type:  bug         |            Status:  new
              Priority:  low         |         Milestone:
             Component:  Compiler    |           Version:  7.8.2
  (Type checker)                     |  Operating System:  Unknown/Multiple
              Keywords:  RankNTypes  |   Type of failure:  GHC rejects
          Architecture:              |  valid program
  Unknown/Multiple                   |        Blocked By:
             Test Case:              |   Related Tickets:
              Blocking:              |
Differential Revisions:              |
-------------------------------------+-------------------------------------
 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.
 }}}

--
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/10450>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler