Commit 89c8d4d2 authored by Richard Eisenberg's avatar Richard Eisenberg Committed by Ben Gamari

Fix #13909 by tweaking an error message.

GHC was complaining about numbers of arguments when the real
problem is impredicativity.

test case: typecheck/should_fail/T13909
parent 3edbf5c6
......@@ -2019,8 +2019,11 @@ mkExpectedActualMsg ty1 ty2 (TypeEqOrigin { uo_actual = act
| otherwise = text "kind" <+> quotes (ppr exp)
num_args_msg = case level of
TypeLevel -> Nothing
KindLevel
| not (isMetaTyVarTy exp) && not (isMetaTyVarTy act)
-- if one is a meta-tyvar, then it's possible that the user
-- has asked for something impredicative, and we couldn't unify.
-- Don't bother with counting arguments.
-> let n_act = count_args act
n_exp = count_args exp in
case n_act - n_exp of
......@@ -2035,6 +2038,8 @@ mkExpectedActualMsg ty1 ty2 (TypeEqOrigin { uo_actual = act
| otherwise = text "more arguments to" -- n > 1
_ -> Nothing
_ -> Nothing
maybe_num_args_msg = case num_args_msg of
Nothing -> empty
Just m -> m
......
{-# LANGUAGE TypeInType #-}
module T13909 where
import Data.Kind
data Hm (k :: Type) (a :: k) :: Type
class HasName (a :: k) where
getName :: proxy a -> String
instance HasName Hm where
getName _ = "Hm"
T13909.hs:11:18: error:
• Expected kind ‘k0’, but ‘Hm’ has kind ‘forall k -> k -> *’
• In the first argument of ‘HasName’, namely ‘Hm’
In the instance declaration for ‘HasName Hm’
......@@ -455,4 +455,5 @@ test('T13902', normal, compile_fail, [''])
test('T11963', normal, compile_fail, [''])
test('T14000', normal, compile_fail, [''])
test('T14055', normal, compile_fail, [''])
test('T13909', normal, compile_fail, [''])
test('T14232', normal, compile_fail, [''])
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment