Closed LightAndLight closed 1 year ago
Fixing this caused another type error test case to regress:
25.ipso
class Show a where
show : a -> String
instance Show Int where
show = int.toString
prettyArray : Show a => Array a -> String
prettyArray arr =
"[${
if int.eq (array.length arr) 0
then ""
else
array.foldl
(\acc el -> "${acc}, ${show el}")
(array.index 0 arr)
(array.slice 1 (array.length arr - 1) arr)
}]"
main : IO ()
main = print (prettyArray [0, 1, 2, 3, 4])
Expected output:
25.ipso:15:9: error: expected type "String", got type "a"
|
15 | (array.index 0 arr)
| ^
Actual output:
25.ipso:15:24: error: expected type "Array String", got type "Array a"
|
15 | (array.index 0 arr)
| ^
What's happening here?
We end up checking that array.index 0 arr
has type String
. array.index
has type forall x. Int -> Array x -> x
. x
is instantiated to String
, and then arr : Array a
is checked against Array String
. Array String
is expected but arr : Array a
is provided, so that's where the type error occurs.
I prefer type variable instantiation to be driven by a function's arguments rather than its return type. In this case I want x
to be instantiated to a
, and infer that array.index 0 arr : a
, and report that we expect array.index 0 arr
to have type String
but it has type a
.
I'm wary that all this may be heuristic and I might never have a system that reports all errors the way I want. Are there any situations where I'd be okay with type variable instantiation flowing from the return type?
I guess I'm okay with it when the type information comes from a user-supplied signature. The reason I created this issue was because I didn't push the known return type through the type variables of array.foldl
.
Here's an interesting situation based on the prior post: where should the type error be reported for the following?
first! : Array a -> String
first! arr =
array.index 0 arr
The behaviour prior to this issue was to report expected "String", got "a"
for array.index 0 arr
. That's what I prefer.
But for the array.foldl
call, which has a very similar structure, this isn't what I wanted. I want to report the type error inside the argument to the function.
When I change the type checker to return the argument-local error for array.foldl
, it also returns an argument-local for the above first
definition, saying that arg
was expected to be Array String
but was actually Array a
.
Also, interestingly, the changes I made give an error I don't like for the eta-reduced version of first!
(first! = array.index 0
), saying that it expected array.index
to have type Int -> Array a -> String
but it actually had type Int -> Array a -> a
.
What are the differences between all these definitions, and is there a principle I can generalise over?
array.foldl
first : Array a -> (| Some : a, None : () |)
first =
array.foldl
(\result item ->
case result of
None () -> item
Some _ -> result
)
(None ())
array.foldl : (b -> a -> b) -> b -> Array a -> b
Ideal error: argument-local
Type flow:
array.foldl ... ... <= Array a -> (| Some : a, None : () |)
(\result item -> ...) <= (| Some : a, None : () |) -> a -> (| Some : a, None : () |)
item <= (| Some : a, None : () |)
array.index
(eta-expanded)first! : Array a -> String
first! arr =
array.index 0 arr
Ideal error: whole expression
Type flow:
array.index 0 arr => a
a == String
array.index
(eta-reduced)first! : Array a -> String
first! =
array.index 0
Ideal error: whole expression
Type flow:
array.index 0 => Array a -> a
Array a -> a == Array a -> String
What does GHC do?
first :: [a] -> Maybe a
first =
foldl
(\result item ->
case result of
Nothing -> item
Just _ -> result
)
Nothing
---
1.hs:6:20: error:
• Couldn't match expected type ‘Maybe a’ with actual type ‘a’
‘a’ is a rigid type variable bound by
the type signature for:
first :: forall a. [a] -> Maybe a
at 1.hs:1:1-23
• In the expression: item
In a case alternative: Nothing -> item
In the expression:
case result of
Nothing -> item
Just _ -> result
• Relevant bindings include
item :: a (bound at 1.hs:4:14)
result :: Maybe a (bound at 1.hs:4:7)
first :: [a] -> Maybe a (bound at 1.hs:2:1)
|
6 | Nothing -> item
| ^^^^
first :: [a] -> String
first arr =
arr !! 0
---
2.hs:3:3: error:
• Couldn't match type ‘a’ with ‘String’
Expected: [String]
Actual: [a]
‘a’ is a rigid type variable bound by
the type signature for:
first :: forall a. [a] -> String
at 2.hs:1:1-22
• In the first argument of ‘(!!)’, namely ‘arr’
In the expression: arr !! 0
In an equation for ‘first’: first arr = arr !! 0
• Relevant bindings include
arr :: [a] (bound at 2.hs:2:7)
first :: [a] -> String (bound at 2.hs:2:1)
|
3 | arr !! 0
| ^^^
first :: [a] -> String
first =
(!! 0)
---
3.hs:3:4: error:
• Couldn't match type ‘a’ with ‘String’
Expected: [a] -> String
Actual: [a] -> a
‘a’ is a rigid type variable bound by
the type signature for:
first :: forall a. [a] -> String
at 3.hs:1:1-22
• In the expression: !! 0
In an equation for ‘first’: first = (!! 0)
• Relevant bindings include
first :: [a] -> String (bound at 3.hs:2:1)
|
3 | (!! 0)
| ^^^^
class Show' a where
show' :: a -> String
instance Show' Int where
show' = show
prettyArray :: Show' a => [a] -> String
prettyArray arr =
"[" ++
(if length arr == 0
then ""
else
foldl
(\acc el -> acc ++ ", " ++ show el)
(arr !! 0)
arr
) ++
"]"
---
4.hs:15:10: error:
• Couldn't match type ‘a’ with ‘[Char]’
Expected: [[Char]]
Actual: [a]
‘a’ is a rigid type variable bound by
the type signature for:
prettyArray :: forall a. Show' a => [a] -> String
at 4.hs:7:1-39
• In the first argument of ‘(!!)’, namely ‘arr’
In the second argument of ‘foldl’, namely ‘(arr !! 0)’
In the expression:
foldl (\ acc el -> acc ++ ", " ++ show el) (arr !! 0) arr
• Relevant bindings include
arr :: [a] (bound at 4.hs:8:13)
prettyArray :: [a] -> String (bound at 4.hs:8:1)
|
15 | (arr !! 0)
| ^^^
In #382 I've compromised by making the type errors match those given by GHC.
test.ipso
Expected output:
Actual output: