Misleading "Kind mis-match on LHS of default declaration" error

This program fails to typecheck, unsurprisingly:

{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE TypeFamilies #-}
module Bug where

class C a where
  type T a :: k
  type T a = Int

But the error message it gives threw me for a loop initially:

$ /opt/ghc/8.2.1/bin/ghci Bug.hs
GHCi, version 8.2.0.20170704: http://www.haskell.org/ghc/  :? for help
Loaded GHCi configuration from /home/rgscott/.ghci
[1 of 1] Compiling Bug              ( Bug.hs, interpreted )

Bug.hs:7:3: error:
    • Kind mis-match on LHS of default declaration for ‘T’
    • In the default type instance declaration for ‘T’
      In the class declaration for ‘C’
  |
7 |   type T a = Int
  |   ^^^^^^^^^^^^^^
Failed, 0 modules loaded.

The LHS of the default declaration is perfectly fine - the real source of the error is the RHS!

Trac metadata

Trac field	Value
Version	8.0.1
Type	Bug
TypeOfFailure	OtherFailure
Priority	normal
Resolution	Unresolved
Component	Compiler (Type checker)
Test case
Differential revisions
BlockedBy
Related
Blocking
CC
Operating system
Architecture

changed weight to 5

added Tbug Trac import typechecker labels

I suppose we could just remove the phrase "on LHS" as a simple fix.

What's curious is that in other situations, the error message you get for mismatched kinds in type family defaults is much clearer. For instance:

λ> class C a where { type T a; type T a = 4 }

<interactive>:1:40: error:
    • Expected a type, but ‘4’ has kind ‘GHC.Types.Nat’
    • In the type ‘4’
      In the default type instance declaration for ‘T’
      In the class declaration for ‘C’

That is much, much better than the vague "Kind mis-match on LHS of default declaration" message we get in the original program. I wonder if GHC can arrange for this "Expected a type, but foo has kind Bar" error message to trigger for the original program as well.

added TypeFamilies label

added error messages label

I think the error message (reporting about the LHS) is actually OK, but we need to give more context, by printing out that

• The user's code expands to type T @Star a = Int, and

• That type family defaults cannot instantiate variables.

The problem is that it's not at all obvious to me how to know when to print out type T a = Int versus type T @Star a = Int (i.e., how to know when the issue stems from a kind argument). This is the entirety of the code that performs this validity check:

       ; case tcMatchTys pats (mkTyVarTys (tyConTyVars fam_tc)) of
           Just subst -> return (Just (substTyUnchecked subst rhs_ty, loc) )
           Nothing    -> failWithTc (defaultAssocKindErr fam_tc)

This lumps all left-hand side arguments into a single pats list on checks them with tcMatchTys. I'm not aware of a way to make this analysis finer-grained.

I think that use of tcMatchTys is a bit overkill, actually. In a correct declaration, the pats there will all be bare type variables. The "target" (the mkTyVarTys ...) are also (clearly) just type variables. So we can just build a substitution. In an incorrect declaration, one or more pats will either be a non-type-variable or a repeated one. So just check for this. If the bad argument is an invisible one, now you know how to print. Perhaps the tcMatchTys is shorter to write, but it implies a subtler check than what we really need here.

Hm, how does this sound as a potential error message?

    • Illegal associated type family default declaration:                                          
        ‘type T @{k} @* a = Int’                                                                   
        The arguments to ‘T’ must all be type variables                                            
    • In the default type instance declaration for ‘T’                                             
      In the class declaration for ‘C’                                                             
  |                                                                                                
7 |   type T a = Int                                                                               
  |   ^^^^^^^^^^^^^^

It would be nice to somehow note that the k there is the kind of a, not the k in the previous line. But that's seems quite hard to do. I suppose the message is OK, then. Thanks!

mentioned in commit RyanGlScott/ghc@59e01983

mentioned in merge request !696 (closed)

!696 (closed)

mentioned in commit RyanGlScott/ghc@9a3d26f9

mentioned in commit 33b0a291

closed via merge request !705 (merged)

Testsuite-tests: T13971

mentioned in commit erthalion/ghc@e6234488

Ack, I don't think the fix in !696 (closed) was quite right. In particular, I just realized that GHC HEAD now accepts this erroneous program, which was previously rejected:

{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE TypeFamilies #-}
module Bug where

import Data.Kind

class C (a :: j) where
  type T (a :: j) (b :: k)
  type T (a :: k) (b :: k) = k

This program is ill formed since j and k ought to be distinct type variables, but they aren't in the default equation. However, since they're both type variables, they both squeak by the new validity check.

reopened

I still say !696 (closed) was a step in the right direction. It just needs to add one more check (for repeated variables).

mentioned in merge request !889 (merged)

!889 (merged) should clear this last hurdle.

changed milestone to %8.10.1

mentioned in commit 936b3e4f

closed via commit 78a5c4ce

Testsuite-tests: indexed-types/should_fail/T13971b

mentioned in commit 78a5c4ce

added Pnormal label

mentioned in issue #18648 (closed)