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 )
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
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 |
comment:2 Changed 4 years ago by
Type: | bug → task |
---|
comment:3 Changed 4 years ago by
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
Keywords: | TypeErrorMessages added |
---|
Why don't you write
which works just fine?
To answer your specific question,
let
does generalisation, whilecase
does not.typeAnnotatedMap
, the type ofptail
is generalised (by thelet
) toforall a. [Phantom a]
. So thetypeAnnotatedMap
has an argument that is sufficiently polymorphic.typeAnnotatedMap1
, the type ofptail
is[Phantom x0]
, where the call tointList
(incase intList of...
) is instantiated at typex0
. But that means that the calltypeAnnotatedMap1 ptail
fails, because the type ofptail
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.