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

* 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

#16356: Unexpected type application in default declaration -------------------------------------+------------------------------------- Reporter: int-index | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 8.6.3 checker) | Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by RyanGlScott): The [https://downloads.haskell.org/~ghc/8.6.3/docs/html/users_guide/glasgow_exts.... #associated-type-synonym-defaults users' guide section] on associated type family defaults is probably the closest thing to a specification of how they must be structured: 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. 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 [https://gitlab.haskell.org/ghc/ghc/blob/04b7f4c1c6ea910ab378f27c5f9efd6c88f6... 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). -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/16356#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#16356: Unexpected type application in default declaration -------------------------------------+------------------------------------- Reporter: int-index | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 8.6.3 checker) | Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by RyanGlScott): Upon further thought, I downplayed the amount of effort required to make this work in comment:1. [https://gitlab.haskell.org/ghc/ghc/blob/2e8f664957dc3763dc4375894b8dc4d046d2... This code] in `TcTyClsDecls.tcDefaultAssocDecl` is problematic: {{{#!hs 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: {{{#!hs 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. [https://gitlab.haskell.org/ghc/ghc/blob/2e8f664957dc3763dc4375894b8dc4d046d2... This] is how GHC represents ordinary type family equations: {{{#!hs type FamInstEqn pass rhs = HsImplicitBndrs pass (FamEqn pass (HsTyPats pass) rhs) }}} And [https://gitlab.haskell.org/ghc/ghc/blob/2e8f664957dc3763dc4375894b8dc4d046d2... this] is how GHC represents associated type family defaults: {{{#!hs 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 `FamInstEqn`s, 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 informative about which of its arguments are VKAs or not. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/16356#comment:3 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler