Type inference breaks on constraint-kinded parameter used by a Rank-2 callback
Apologies in advance if the terminology in the summary is incorrect, I'm not really sure of the proper terms to use here
The following code:
{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE ScopedTypeVariables #-}
module Scratch where
import Prelude
data Foo
= FooA Int
| FooB String
useFoo :: forall cls a . (cls Int, cls String) => (forall k . cls k => k -> a) -> Foo -> a
useFoo f (FooA a) = f a
useFoo f (FooB b) = f b
seems like it should be able to infer the cls
type parameter to useFoo
based on the first argument, but instead calling with kshow
gives the following error message:
>>> useFoo show (FooA 1)
<interactive>:52:1: error:
• Could not deduce: (cls0 Int, cls0 String)
arising from a use of ‘useFoo’
• In the expression: useFoo show (FooA 1)
In an equation for ‘it’: it = useFoo show (FooA 1)
<interactive>:52:8: error:
• Couldn't match type ‘a’ with ‘String’
‘a’ is untouchable
inside the constraints: cls0 k
bound by a type expected by the context:
forall k. cls0 k => k -> a
at <interactive>:52:1-20
‘a’ is a rigid type variable bound by
the inferred type of it :: a at <interactive>:52:1-20
Possible fix: add a type signature for ‘it’
Expected type: k -> a
Actual type: k -> String
• In the first argument of ‘useFoo’, namely ‘show’
In the expression: useFoo show (FooA 1)
In an equation for ‘it’: it = useFoo show (FooA 1)
• Relevant bindings include it :: a (bound at <interactive>:52:1)
Type-applying useFoo
works as expected:
>>> :set -XTypeApplications
>>> useFoo @Show show (FooA 1)
"1"
This broke both with and without ScopedTypeVariables
Trac metadata
Trac field | Value |
---|---|
Version | 8.2.2 |
Type | Bug |
TypeOfFailure | OtherFailure |
Priority | normal |
Resolution | Unresolved |
Component | Compiler |
Test case | |
Differential revisions | |
BlockedBy | |
Related | |
Blocking | |
CC | |
Operating system | |
Architecture |