Pattern synonyms allow unlifted top-level bindings -- and they're thunks!

Feeling like being abusive to GHC (and in thinking about https://github.com/ghc-proposals/ghc-proposals/pull/265), I gave it this:

{-# LANGUAGE PatternSynonyms, MagicHash #-}

module Main where

import Debug.Trace
import GHC.Exts

pattern Strange <- 0#
  where Strange = case trace "evaluating now" 0 of
                    I# n -> n

main = do
  putStrLn "Starting"
  print (I# Strange)

Two strange things happened:

1. This program was accepted, despite the fact that Strange is a top-level unlifted binding.

2. Strange is actually a thunk. I see Starting in the output before evaluating now.

As I was writing this up, I realized that I probably knew this, deep down, having seen the implementation of this all (where a magical Void# parameter is added to unlifted pattern synonyms). But this should, at least, be documented in the manual, where I could not find it in the pattern synonyms section.