Premature specialization of numeric literals with Typed Holes
Summary
Numeric literals are specialized to Integer which trips up the hole fit algorithm.
Steps to reproduce
Suppose I forgot about Map.singleton, and I wrote this code:
import qualified Data.Map as Map
what :: Map.Map String Int
what = _f "hello" 1GHC 8.10.2 will suggest mempty. The reason is that 1 gets specialized to Integer, which means that _f :: String -> Integer -> Map String Int, and there are no valid fits for it. We can fix this by either changing Int to Integer or adding a type annotation to 1.
If we generalize the Map, this still doesn't work:
what :: forall a. Num a => Map.Map String a
what = _f "hello" 1/home/matt/map.hs:6:8: error:
• Found hole: _f :: [Char] -> Integer -> Map.Map String a
Where: ‘a’ is a rigid type variable bound by
the type signature for:
what :: forall a. Num a => Map.Map String a
at /home/matt/map.hs:5:1-43
Or perhaps ‘_f’ is mis-spelled, or not in scope
• In the expression: _f
In the expression: _f "hello" 1
In an equation for ‘what’: what = _f "hello" 1
• Relevant bindings include
what :: Map.Map String a (bound at /home/matt/map.hs:6:1)
Constraints include Num a (from /home/matt/map.hs:5:1-43)
Valid hole fits include
mempty :: forall a. Monoid a => a
with mempty @([Char] -> Integer -> Map.Map String a)
(imported from ‘Prelude’ at /home/matt/map.hs:1:1
(and originally defined in ‘GHC.Base’))
|
6 | what = _f "hello" 1
| ^^The only way to get the right suggestion is to force 1 to remain polymorphic with a type signature.
{-# language ScopedTypeVariables #-}
import qualified Data.Map as Map
what :: forall a. Num a => Map.Map String a
what = _f "hello" (1 :: a)/home/matt/map.hs:6:8: error:
• Found hole: _f :: [Char] -> a -> Map.Map String a
Where: ‘a’ is a rigid type variable bound by
the type signature for:
what :: forall a. Num a => Map.Map String a
at /home/matt/map.hs:5:1-43
Or perhaps ‘_f’ is mis-spelled, or not in scope
• In the expression: _f
In the expression: _f "hello" (1 :: a)
In an equation for ‘what’: what = _f "hello" (1 :: a)
• Relevant bindings include
what :: Map.Map String a (bound at /home/matt/map.hs:6:1)
Constraints include Num a (from /home/matt/map.hs:5:1-43)
Valid hole fits include
Map.singleton :: forall k a. k -> a -> Map.Map k a
with Map.singleton @String @a
(imported qualified from ‘Data.Map’ at /home/matt/map.hs:3:1-32
(and originally defined in ‘Data.Map.Internal’))
mempty :: forall a. Monoid a => a
with mempty @([Char] -> a -> Map.Map String a)
(imported from ‘Prelude’ at /home/matt/map.hs:1:1
(and originally defined in ‘GHC.Base’))
|
6 | what = _f "hello" (1 :: a)
| ^^Curiously, this also fails to suggest Map.singleton:
{-# language AllowAmbiguousTypes, ScopedTypeVariables #-}
import qualified Data.Map as Map
what :: forall a. Num a => Map.Map String Int
what = _f "hello" (1 :: a)It can't unify _f :: String -> a -> Map.Map String Int with Map.singleton :: String -> Int -> Map.Map String Int.
I tried this with mempty instead of 1, but that actually works:
import qualified Data.Map as Map
import Data.Monoid (Sum)
what :: Map.Map String (Sum Int)
what = _f "hello" mempty[1 of 1] Compiling Main ( /home/matt/map.hs, interpreted )
/home/matt/map.hs:5:8: error:
• Found hole: _f :: [Char] -> t0 -> Map.Map String (Sum Int)
Where: ‘t0’ is an ambiguous type variable
Or perhaps ‘_f’ is mis-spelled, or not in scope
• In the expression: _f
In the expression: _f "hello" mempty
In an equation for ‘what’: what = _f "hello" mempty
• Relevant bindings include
what :: Map.Map String (Sum Int) (bound at /home/matt/map.hs:5:1)
Valid hole fits include
Map.delete :: forall k a. Ord k => k -> Map.Map k a -> Map.Map k a
with Map.delete @String @(Sum Int)
(imported qualified from ‘Data.Map’ at /home/matt/map.hs:1:1-32
(and originally defined in ‘Data.Map.Internal’))
Map.singleton :: forall k a. k -> a -> Map.Map k a
with Map.singleton @String @(Sum Int)
(imported qualified from ‘Data.Map’ at /home/matt/map.hs:1:1-32
(and originally defined in ‘Data.Map.Internal’))
seq :: forall a b. a -> b -> b
with seq @[Char] @(Map.Map String (Sum Int))
(imported from ‘Prelude’ at /home/matt/map.hs:1:1
(and originally defined in ‘GHC.Prim’))
|
5 | what = _f "hello" mempty
| ^^
/home/matt/map.hs:5:19: error:
• Ambiguous type variable ‘t0’ arising from a use of ‘mempty’
prevents the constraint ‘(Monoid t0)’ from being solved.
Probable fix: use a type annotation to specify what ‘t0’ should be.
These potential instances exist:
instance Num a => Monoid (Sum a)
-- Defined in ‘base-4.14.1.0:Data.Semigroup.Internal’
instance Ord k => Monoid (Map.Map k v)
-- Defined in ‘Data.Map.Internal’
instance Monoid a => Monoid (IO a) -- Defined in ‘GHC.Base’
...plus 9 others
...plus 22 instances involving out-of-scope types
(use -fprint-potential-instances to see them all)
• In the second argument of ‘_f’, namely ‘mempty’
In the expression: _f "hello" mempty
In an equation for ‘what’: what = _f "hello" mempty
|
5 | what = _f "hello" mempty
| ^^^^^^
Failed, no modules loaded.Surprisingly enough, it suggests seq, which relies on the Monoid instance for Map! But it doesn't suggest mempty which should fit with mempty @(_ -> Map _ _) (via Monoid r => Monoid (x -> r)).
Expected behavior
Instead of specializing 1 :: Num a => a to Integer and then searching for hole fits, search for hole fits with the general signature. eg _f :: Num a => String -> a -> Map String Int. Map.singleton (as a valid specialization of the typed hole) should fit.
Environment
- GHC version used: 8.10.2
Optional:
- Operating System:
- System Architecture: