Unexpected type application in default declaration

All of these work:

{-# LANGUAGE PolyKinds, TypeApplications, TypeFamilies, FlexibleInstances #-}

import Data.Kind (Type)

data B (a :: k)

type family FClosed :: k -> Type where
  FClosed @k = B @k

type family FOpen :: k -> Type
type instance FOpen @k = B @k

class FAssocClass k where
  type FAssoc :: k -> Type

instance FAssocClass k where
  type FAssoc @k = B @k

This one doesn't:

class FAssocDefaultClass k where
  type FAssocDefault :: k -> Type
  type FAssocDefault @k = B @k

A.hs:21:23: error:
    Unexpected type application @k
    In the default declaration for ‘FAssocDefault’
   |
21 |   type FAssocDefault @k = B @k
   |

So, what are the rules of the game? Let's fix this and document in the User's Guide.

Trac metadata

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

changed weight to 5

added Tbug Trac import typechecker labels

The users' guide section on associated type family defaults is probably the closest thing to a specification of how they must be structured:

Note the following points:

• The instance keyword is optional.
• There can be at most one default declaration for an associated type synonym.
• A default declaration is not permitted for an associated //data// type.
• The default declaration must mention only type //variables// on the left hand side, and the right hand side must mention only type variables that are explicitly bound on the left hand side. This restriction is relaxed for //kind variables//, however, as the right hand side is allowed to mention kind variables that are implicitly bound on the left hand side.
• Unlike the associated type family declaration itself, the type variables of the default instance are independent of those of the parent class.

Here are some examples:

class C (a :: Type) where
type F1 a :: Type
type instance F1 a = [a]     -- OK
type instance F1 a = a->a    -- BAD; only one default instance is allowed

type F2 b a                  -- OK; note the family has more type
--     variables than the class
type instance F2 c d = c->d  -- OK; you don't have to use 'a' in the type instance

type F3 a
type F3 [b] = b              -- BAD; only type variables allowed on the LHS

type F4 a
type F4 b = a                -- BAD; 'a' is not in scope  in the RHS

type F5 a :: [k]
type F5 a = ('[] :: [x])     -- OK; the kind variable x is implicitly
bound by an invisible kind pattern
on the LHS

type F6 a
type F6 a =
Proxy ('[] :: [x])         -- BAD; the kind variable x is not bound,
even by an invisible kind pattern

type F7 (x :: a) :: [a]
type F7 x = ('[] :: [a])     -- OK; the kind variable a is implicitly
bound by the kind signature of the
LHS type pattern

Unless I'm missing something, I don't see anything in here which would explicitly forbid type FAssocDefault @k = B @k. I'm inclined to support allowing it.

In fact, the only reason GHC disallows it at the moment it due to a validity check in in RdrHsSyn.checkTyVars. It might be interesting to see what happens if you remove that validity check. Well, to be more precise, if you remove that validity check for associated type family defaults—we can't just remove the check entirely, since checkTyVars is also used to check the type variable binders for classes, data types, type synonyms, and type family declarations, where we currently disallow visible kind applications (#15782).

I agree that this should work.

Upon further thought, I downplayed the amount of effort required to make this work in ticket:16356#comment:168952. This code in TcTyClsDecls.tcDefaultAssocDecl is problematic:

tcDefaultAssocDecl fam_tc [dL->L loc (FamEqn { feqn_tycon = L _ tc_name
                                             , feqn_pats = hs_tvs
                                             , feqn_rhs = hs_rhs_ty })]
  | HsQTvs { hsq_ext = HsQTvsRn { hsq_implicit = imp_vars}
           , hsq_explicit = exp_vars } <- hs_tvs
  = -- <elided>
            fam_arity = length (tyConVisibleTyVars fam_tc)

       -- <elided>

       -- Arity check
       ; checkTc (exp_vars `lengthIs` fam_arity)
                 (wrongNumberOfParmsErr fam_arity)

Unless the number of exp_vars is exactly the number of visible arguments that the type family expects, then wrongNumberOfParmsErr will throw an error. Unfortunately, it turns out that exp_vars //includes// visible kind arguments! In other words, if you have this:

class FAssocDefaultClass k where
  type FAssocDefault :: k -> Type
  type FAssocDefault @k = B @k

Then exp_vars = [k] and fam_arity = 0, which means that GHC will mistakenly reject FAssocDefault under the guise that it supplies too many arguments.

---

Why, then, does this problem not occur for ordinary type family equations? It turns out that it's because GHC stores the ASTs for each form of declaration in subtly different ways. This is how GHC represents ordinary type family equations:

type FamInstEqn pass rhs
  = HsImplicitBndrs pass (FamEqn pass (HsTyPats pass) rhs)

And this is how GHC represents associated type family defaults:

type TyFamDefltEqn pass = FamEqn pass (LHsQTyVars pass) (LHsType pass)

The important bit here is the second argument to FamEqn, which represents the patterns in the type family equation. In FamInstEqns, the patterns are HsTyPats, which distinguish between ordinary arguments and visible kind arguments. In TyFamDefltEqn, however, the patterns are LHsQTyVars. AFAICT, LHsQTyVars do not make any sort of distinction between ordinary arguments and visible kind arguments, instead only caring about explicitly vs. implicitly quantified variables.

---

How, then, should we change things to allow VKAs in type family defaults? One option is to try switching out LHsQTyVars for HsTyPats in TyFamDefltEqn. I'm not clear as to why we're using LHsQTyVars in the first place, however, so it's possible that there actually is a good reason for its existence here. If so, another alternative would be to somehow augment LHsQTyVars with information about which of its arguments are VKAs or not.

mentioned in issue #16110 (closed)

mentioned in merge request !947 (merged)

mentioned in commit 1225879f

mentioned in commit 2fb8db8a

mentioned in commit ec8f0a02

closed via commit 6efe04de

added Pnormal label

mentioned in issue #16762 (closed)