Opened 4 years ago

Last modified 3 years ago

#10450 new task

Poor type error message when an argument is insufficently polymorphic

Reported by: sjcjoosten Owned by:
Priority: low Milestone:
Component: Compiler (Type checker) Version: 7.8.2
Keywords: RankNTypes, TypeErrorMessages Cc:
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: GHC rejects valid program Test Case:
Blocked By: Blocking:
Related Tickets: Differential Rev(s):
Wiki Page:

Description (last modified by sjcjoosten)

When pattern matching, "let/where" and "case" have different behaviours.

Currently, this is accepted (a version using 'where' instead of 'let' type-checks too):

{-# 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:

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.

Change History (4)

comment:1 Changed 4 years ago by simonpj

Description: modified (diff)
Summary: RankNTypes type check on pattern match of "let" behaves different from "case"Poor type error message when an argument is insufficently polymorphic

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.

comment:2 Changed 4 years ago by sjcjoosten

Type: bugtask

comment:3 Changed 4 years ago by sjcjoosten

Description: modified (diff)

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":

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):

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

comment:4 Changed 3 years ago by simonpj

Keywords: TypeErrorMessages added
Note: See TracTickets for help on using tickets.