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

3 Aug 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'd like Richard E's opinion on all this
...
To me your example raises the question of whether it's even possible to
Me too. We also need to think about how a solution for this ticket would
 hold up under an implementation of #11962.

 figure out the dependencies. You probably believe that your "add extra
 edges" does so. But I still don't know exactly what those edges are. Maybe
 you could take a comment in this ticket to explain your algorithm
 precisely?

 After a bit of thought I came up with a simple change to my last example:

 {{{#!hs
 -- A.hs
 {-# LANGUAGE TypeFamilies #-}
 {-# LANGUAGE PolyKinds #-}
 {-# LANGUAGE TypeInType #-}

 module A where

 import Data.Kind

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

 data family F (t :: Type) :: Open t -> Type
 }}}

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

 module B where

 import Data.Kind
 import A

 data Q

 type instance Open Q = Bool

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

 The difference is that the data family is defined in `A.hs` and the family
 `Closed` is no longer necessary, as the data family is enough to obscure
 the `Open` dependency. `B.hs` as given above will not pass with my
 approach, but swap the two instance declarations and it's fine.
...
So perhaps this small modification to my algorithm will work ...
The modification sounds good, but I share your worry and I think we're
 actually in for a bit more thinking.

 {{{#!hs
 {-# LANGUAGE TypeFamilies #-}
 {-# LANGUAGE PolyKinds #-}
 {-# LANGUAGE TypeInType #-}
 {-# LANGUAGE UndecidableInstances #-}

 module A2 where

 import Data.Kind

 type family Open1 (t :: Type) :: Type

 type family Open2 (t :: Type) (q :: Open1 t) :: Type
 }}}

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

 module B where

 import Data.Kind
 import A2

 type instance Open1 () = Bool
 type instance Open2 () 'True = Char
 }}}

 The instance `Open1 ()` needs to come before `Open2 () 'True` to get that
 `Open1 () ~ Bool`, but how are we to know this? Maybe we always check
 smaller instances (fewer parameters) before bigger ones?
...
Sorry to be slow... I'm on holiday.
No problem, enjoy it!

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