Re: [GHC] #12088: Promote data family instance constructors

14 Jul 2016

      #12088: Promote data family instance constructors
-------------------------------------+-------------------------------------
        Reporter:  alexvieth         |                Owner:
            Type:  feature request   |               Status:  new
        Priority:  normal            |            Milestone:
       Component:  Compiler (Type    |              Version:  8.1
  checker)                           |
      Resolution:                    |             Keywords:  TypeInType
Operating System:  Unknown/Multiple  |         Architecture:
 Type of failure:  GHC rejects       |  Unknown/Multiple
  valid program                      |            Test Case:
      Blocked By:                    |             Blocking:
 Related Tickets:  #11348            |  Differential Rev(s):  Phab:D2272
       Wiki Page:                    |
-------------------------------------+-------------------------------------

Comment (by alexvieth):

 I've spent some more time studying this and now I'm even more convinced
 that we should stay with my solution. Take a look at these modules:

 {{{#!hs
 -- A.hs
 {-# LANGUAGE TypeFamilies #-}
 {-# LANGUAGE KindSignatures #-}
 {-# LANGUAGE UndecidableInstances #-}

 module A where

 import Data.Kind

 type family Closed (t :: Type) :: Type where
   Closed t = Open t

 type family Open (t :: Type) :: Type
 }}}

 {{{#!hs
 -- B.hs
 {-# LANGUAGE TypeFamilies #-}
 {-# LANGUAGE TypeInType #-}
 {-# LANGUAGE DataKinds #-}
 {-# LANGUAGE KindSignatures #-}
 {-# LANGUAGE GADTs #-}

 module B where

 import Data.Kind
 import A

 data Q

 data family F (t :: Type) :: Closed t -> Type

 type instance Open Q = Bool

 data instance F Q r where
   F0 :: F Q 'True
 }}}

 The point is that `type instance Open Q` must be checked before `data
 instance F Q r`, even though we can't see this dependency, as it's hidden
 in `A.hs`.

 With Simon's suggestion, dependency analysis of B gives `[data Q, data
 family F, type instance Open Q, data instance F Q r]` and then it's
 reordered to get `[data Q, type instance Open Q, data family F, data
 instance F Q r]` (insert `type instance Open Q` as early as possible, then
 do the same for `data instance F Q r`). It's all good! But if we change
 the order of the definitions in the source file, we get a different
 result!

 {{{#!hs
 -- B.hs
 {-# LANGUAGE TypeFamilies #-}
 {-# LANGUAGE TypeInType #-}
 {-# LANGUAGE DataKinds #-}
 {-# LANGUAGE KindSignatures #-}
 {-# LANGUAGE GADTs #-}

 module B where

 import Data.Kind
 import A

 data family F (t :: Type) :: Closed t -> Type

 data Q

 type instance Open Q = Bool

 data instance F Q r where
   F0 :: F Q 'True
 }}}

 Here we get `[data family F t, data Q, type instance Open Q, data instance
 F Q r]`, and then we reorder it to `[data family F t, data Q, type
 instance F Q r, type instance Open Q]` (first put `type instance Open Q`
 as soon as possible, then put `data instance F Q r` as soon as possible,
 which is right after `data Q`). Checking `type instance F Q r` causes a
 failure because we don't have `type instance Open Q` yet.

 The issue: this algorithm doesn't discover that `type instance Open Q` can
 go before `data family F t`.  Whether it fails as above depends upon the
 order in which we choose to merge instance declarations into the
 `TyClDecl` list, but in any case there will be a way to make it fail based
 on the order of declarations.

 Taking some `TyClDecl` order and then inserting the `InstDecl`s without
 ever re-ordering the `TyClDecl`s will not work. A more complicated
 algorithm is needed. The one I've implemented doesn't have this problem,
 thanks to the artificial dependency of `data family F t` on `type instance
 Open Q`.

 I should also add that I don't think `TyClGroup` should be changed to have
 only singleton `InstDecl` groups. I'd say it's good that this type
 represents the actual dependency structure, regardless of whether it's
 valid according to the type checker. We'll let the type checker programs
 determine that after the groups are made, but having the renamer do this
 would be overextending the responsibilities of the renamer.

--
Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12088#comment:8
GHC http://www.haskell.org/ghc/
The Glasgow Haskell Compiler