CODEWITHSUNDEEP
haskelltype-familiesdata-kinds
rampion
rampion

Reputation: 89113

Why doesn't GHC resolve this type family instance?

In the following code, GHC is unable to match Obj Hask with *, despite the declaration that type instance Obj Hask = * just above.

What's preventing this?

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE TypeFamilies #-}

module Minimal where

type family Obj t :: *

type family Arr t :: Obj t -> Obj t -> *

data Hask

type instance Obj Hask = *

type instance Arr Hask = (->)

-- Minimal.hs:15:26: error:
--     • Couldn't match kind ‘Obj Hask’ with ‘*’
--       Expected kind ‘Obj Hask -> Obj Hask -> *’,
--         but ‘(->)’ has kind ‘* -> * -> *’
--     • In the type ‘(->)’
--       In the type instance declaration for ‘Arr’
--    |
-- 15 | type instance Arr Hask = (->)
--    |                          ^^^^

It's able to note the equivalence if I give it a nudge

{-# LANGUAGE StandaloneKindSignatures #-}
-- …
type Function :: Obj Hask -> Obj Hask -> *
type Function = (->)

type instance Arr Hask = Function
-- compiles just fine

Upvotes: 3

Views: 105

Answers (1)

Li-yao Xia
Li-yao Xia

Reputation: 33519

This is the one spot where type families surprisingly don't "just work".

GHC internally splits declarations into groups and can't use a type instance to typecheck things in its own group. Adding intermediate declarations affects this grouping, which is why things may or may not typecheck depending on that.

Another more reliable way to break groups is to add empty Template Haskell splices ($(return []) or newDeclarationGroup).

See also GHC issues #22257 and #12088.

Upvotes: 6

Related Questions