[GHC] #14507: Core Lint error with Type.Reflection and pattern synonyms

21 Nov 2017


      #14507: Core Lint error with Type.Reflection and pattern synonyms
-------------------------------------+-------------------------------------
           Reporter:  Iceland_jack   |             Owner:  (none)
               Type:  bug            |            Status:  new
           Priority:  normal         |         Milestone:
          Component:  Compiler       |           Version:  8.2.1
           Keywords:                 |  Operating System:  Unknown/Multiple
  PatternSynonyms                    |
       Architecture:                 |   Type of failure:  None/Unknown
  Unknown/Multiple                   |
          Test Case:                 |        Blocked By:
           Blocking:                 |   Related Tickets:
Differential Rev(s):                 |         Wiki Page:
-------------------------------------+-------------------------------------
 {{{#!hs
 {-# Language PatternSynonyms, ViewPatterns, GADTs, ConstraintKinds,
 RankNTypes, KindSignatures, PolyKinds, ScopedTypeVariables, DataKinds,
 TypeInType, TypeOperators, TypeApplications, TypeFamilies,
 TypeFamilyDependencies #-}

 import Type.Reflection
 import Prelude
 import Data.Kind

 data Dict c where
   Dict :: c => Dict c

 data N = O | S N

 foo :: forall (kind::k') (a::k). TypeRep kind -> TypeRep a -> Maybe (kind
 :~~: k, TypeRep a)
 foo krep rep = do
   HRefl <- eqTypeRep krep (typeRepKind rep)
   pure (HRefl, rep)

 pattern Bloop' :: forall k' (a::k). Typeable k' => k':~~:k -> TypeRep
 (a::k) -> TypeRep (a::k)
 pattern Bloop' hrefl rep <- (foo (typeRep @k') -> Just (hrefl, rep))
   where Bloop' HRefl rep = rep

 type family
   SING = (res :: k -> Type) | res -> k where
   -- Core Lint error disappears with this line:
   SING = (TypeRep :: N -> Type)

 pattern RepN :: forall (a::kk). Typeable a => N~kk => SING a -> TypeRep
 (a::kk)
 pattern RepN tr <- Bloop' (HRefl::N:~~:kk) (tr :: TypeRep (a::N))
   where RepN tr = tr

 asTypeable :: TypeRep a -> Dict (Typeable a)
 asTypeable rep =
   withTypeable rep
     Dict

 pattern TypeRep :: () => Typeable a => TypeRep a
 pattern TypeRep <- (asTypeable -> Dict)
   where TypeRep = typeRep

 -- error
 pattern SO = RepN TypeRep
 }}}

 triggers “Core Lint errors” on 8.2.1, 8.3.20170920 when run with `ghci
 -ignore-dot-ghci -dcore-lint`.

-- 
Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14507
GHC http://www.haskell.org/ghc/
The Glasgow Haskell Compiler