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