[GHC] #10450: Poor type error message when an argument is insufficently polymorphic

[GHC]

#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