[GHC] #11812: Template Haskell can induce non-unique Uniques

[GHC]

#11812: Template Haskell can induce non-unique Uniques
-------------------------------------+-------------------------------------
        Reporter:  goldfire          |                Owner:  (none)
            Type:  bug               |               Status:  new
        Priority:  normal            |            Milestone:
       Component:  Template Haskell  |              Version:  8.1
      Resolution:                    |             Keywords:
Operating System:  Unknown/Multiple  |         Architecture:
                                     |  Unknown/Multiple
 Type of failure:  None/Unknown      |            Test Case:
      Blocked By:                    |             Blocking:
 Related Tickets:                    |  Differential Rev(s):
       Wiki Page:                    |
-------------------------------------+-------------------------------------
Description changed by RyanGlScott:

Old description:

> When quoting a Template Haskell expression (or type), you can get your
> hands on renamed variables. These variables have assigned Uniques. If you
> then use the same variable locally in ''different'' top-level
> expressions, chaos can ensue. It's certainly expected that something
> bizarre would happen if you used the same Unique twice within the same
> scope, but it surprised me that using the same Unique twice in different
> scopes would cause a problem.
>
> Below is the rather hard-won reduced test case:
>
> {{{
> {-# LANGUAGE TemplateHaskell, PolyKinds, RankNTypes, TypeFamilies #-}
>
> module Bug where
>
> import Language.Haskell.TH
> import Data.Type.Equality
>
> type Const a b = a
>
> $( do ForallT [PlainTV n] _ _ <- [t| forall n. n |]
>     let noBang = Bang NoSourceUnpackedness NoSourceStrictness
>     return [ClosedTypeFamilyD
>             (TypeFamilyHead (mkName "F1")
>              [ KindedTV (mkName "a") (VarT n)
>              , PlainTV (mkName "b") ]
>              (KindSig (VarT n))
>              Nothing)
>             [TySynEqn [VarT (mkName "a"), VarT (mkName "b")]
>                       (ConT ''Const `AppT` VarT (mkName "a")
>                                     `AppT` (ConT (mkName "T1") `AppT`
> VarT (mkName "a")
>                                                                `AppT`
> VarT (mkName "b")))]
>            ,DataD
>             []
>             (mkName "T1")
>             [ KindedTV (mkName "a") (VarT n)
>             , PlainTV (mkName "b")
>             , PlainTV (mkName "c")]
>             Nothing
>             [NormalC (mkName "K1")
>              [(noBang, ConT ''(:~:) `AppT` VarT (mkName "c")
>                                     `AppT` (ConT (mkName "F1") `AppT`
> VarT (mkName "a")
>                                                                `AppT`
> VarT (mkName "b")))]]
>             []])
> }}}
>
> This blob produces
>
> {{{
> type family F1 (a :: n_auRf) b :: n_auRf where
> F1 a b = Const a (T1 a b)
> data T1 (a :: n_auRf) b c = K1 ((:~:) c (F1 a b))
> }}}
>
> which compiles fine when typed in directly. Note that this hinges on the
> `SigTv` behavior of kind variables in non-CUSK declarations, but I don't
> think that's the nub of the problem.
>
> What happens is this: during renaming, the `n`s are renamed to have the
> same `Unique`, because `n` is `Exact`. Type-checking invents `SigTv`s for
> each `n`. Naturally, both `n`s have ''different'' `IORef`s stored in
> their `TcTyVarDetails`. When the two `n`s are compared during checking,
> though, their `Unique`s are the same, and so nothing happens -- even
> though they should be unified. The upshot is that we get one logical
> variable `n` with different `IORef`s in different occurrences, causing
> chaos.
>
> It might be reasonable to punt on this, but we should document in the
> manual what the problem is. It puzzled me for quite a while when the
> problem came up in real code!

New description:

 When quoting a Template Haskell expression (or type), you can get your
 hands on renamed variables. These variables have assigned Uniques. If you
 then use the same variable locally in ''different'' top-level expressions,
 chaos can ensue. It's certainly expected that something bizarre would
 happen if you used the same Unique twice within the same scope, but it
 surprised me that using the same Unique twice in different scopes would
 cause a problem.

 Below is the rather hard-won reduced test case:

 {{{
 {-# LANGUAGE TemplateHaskell, PolyKinds, RankNTypes, TypeFamilies #-}

 module Bug where

 import Language.Haskell.TH
 import Data.Type.Equality

 type Const a b = a

 $(do ForallT [PlainTV n] _ _ <- [t| forall n. n |]
      let noBang = Bang NoSourceUnpackedness NoSourceStrictness
      return [ClosedTypeFamilyD
              (TypeFamilyHead (mkName "F1")
               [ KindedTV (mkName "a") (VarT n)
               , PlainTV (mkName "b") ]
               (KindSig (VarT n))
               Nothing)
              [TySynEqn [VarT (mkName "a"), VarT (mkName "b")]
                        (ConT ''Const `AppT` VarT (mkName "a")
                                      `AppT` (ConT (mkName "T1") `AppT`
 VarT (mkName "a")
                                                                 `AppT`
 VarT (mkName "b")))]
             ,DataD
              []
              (mkName "T1")
              [ KindedTV (mkName "a") (VarT n)
              , PlainTV (mkName "b")
              , PlainTV (mkName "c")]
              Nothing
              [NormalC (mkName "K1")
               [(noBang, ConT ''(:~:) `AppT` VarT (mkName "c")
                                     `AppT` (ConT (mkName "F1") `AppT` VarT
 (mkName "a")
                                                                 `AppT`
 VarT (mkName "b")))]]
              []])
 }}}

 This blob produces

 {{{
 type family F1 (a :: n_auRf) b :: n_auRf where
   F1 a b = Const a (T1 a b)
 data T1 (a :: n_auRf) b c = K1 ((:~:) c (F1 a b))
 }}}

 which compiles fine when typed in directly. Note that this hinges on the
 `SigTv` behavior of kind variables in non-CUSK declarations, but I don't
 think that's the nub of the problem.

 What happens is this: during renaming, the `n`s are renamed to have the
 same `Unique`, because `n` is `Exact`. Type-checking invents `SigTv`s for
 each `n`. Naturally, both `n`s have ''different'' `IORef`s stored in their
 `TcTyVarDetails`. When the two `n`s are compared during checking, though,
 their `Unique`s are the same, and so nothing happens -- even though they
 should be unified. The upshot is that we get one logical variable `n` with
 different `IORef`s in different occurrences, causing chaos.

 It might be reasonable to punt on this, but we should document in the
 manual what the problem is. It puzzled me for quite a while when the
 problem came up in real code!

--

-- 
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/11812#comment:2>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler