Re: [GHC] #14668: Ordering of declarations can cause typechecking to fail

2 Dec 2018

      #14668: Ordering of declarations can cause typechecking to fail
-------------------------------------+-------------------------------------
        Reporter:  heptahedron       |                Owner:  (none)
            Type:  bug               |               Status:  new
        Priority:  normal            |            Milestone:
       Component:  Compiler (Type    |              Version:  8.2.1
  checker)                           |
      Resolution:                    |             Keywords:  TypeInType
Operating System:  Unknown/Multiple  |         Architecture:
                                     |  Unknown/Multiple
 Type of failure:  None/Unknown      |            Test Case:
      Blocked By:                    |             Blocking:
 Related Tickets:  #12088, #12643,   |  Differential Rev(s):
  #15561                             |
       Wiki Page:                    |
-------------------------------------+-------------------------------------
Changes (by RyanGlScott):

 * related:   => #12088, #12643, #15561

Comment:

 This is almost surely a duplicate of #12088 (see also #12643 and #15561,
 which are other surely-duplicates of #12088).

 Here are two tricks to making these sorts of programs compile:

 1. `TemplateHaskell`. Using an empty Template Haskell splice can often
 force GHC's SCC analysis to come to its senses and do the right thing. As
 an example, the following variations of danilo2's program in comment:4
 compiles:

 {{{#!hs
 {-# LANGUAGE TemplateHaskell #-}
 {-# LANGUAGE TypeFamilies #-}
 {-# LANGUAGE TypeInType #-}
 {-# LANGUAGE TypeOperators #-}

 module Type.Data.Map where

 import Prelude
 import Data.Kind

 type family KeyKind (obj :: Type) :: Type
 type family ValKind (obj :: Type) :: Type

 type family Get (key :: KeyKind a) (obj :: a) :: ValKind a

 data Map (k :: Type) (v :: Type) = Map [(k,v)]

 type instance KeyKind (Map k v) = k
 type instance ValKind (Map k v) = v

 $(pure [])

 type instance Get k ('Map ('(k,v) ': _)) = v
 }}}

 2. Closed type families. As I discovered recently in #15561, open and
 closed type families behave differently in SCC analysis, so it turns out
 that turning `ValKind` into a closed type family makes danilo2's program
 compile as well:

 {{{#!hs
 {-# LANGUAGE TemplateHaskell #-}
 {-# LANGUAGE TypeFamilies #-}
 {-# LANGUAGE TypeInType #-}
 {-# LANGUAGE TypeOperators #-}

 module Type.Data.Map where

 import Prelude
 import Data.Kind

 type family KeyKind (obj :: Type) :: Type
 type family ValKind (obj :: Type) :: Type where
   ValKind (Map k v) = v

 type family Get (key :: KeyKind a) (obj :: a) :: ValKind a

 data Map (k :: Type) (v :: Type) = Map [(k,v)]

 type instance Get k ('Map ('(k,v) ': _)) = v

 type instance KeyKind (Map k v) = k
 }}}

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