Support typechecking of type literals in backpack

Backpack is unable to type check signatures that expect a data which
is a type level literal. This was reported in issue #15138. These
commits are a fix for this. It also includes a minimal test case that
was mentioned in the issue.

Reviewers: bgamari, ezyang, goldfire

Reviewed By: bgamari, ezyang

Subscribers: simonpj, ezyang, rwbarton, thomie, carter

GHC Trac Issues: #15138

Differential Revision: https://phabricator.haskell.org/D4951

5 files changed, 55 insertions, 1 deletions

diff --git a/compiler/typecheck/TcRnDriver.hs b/compiler/typecheck/TcRnDriver.hs
index 4449d67c29..cc9518f68b 100644
--- a/compiler/typecheck/TcRnDriver.hs
+++ b/compiler/typecheck/TcRnDriver.hs
@@ -1016,7 +1016,6 @@ checkBootTyCon is_boot tc1 tc2
   = ASSERT(tc1 == tc2)
     checkRoles roles1 roles2 `andThenCheck`
     check (eqTypeX env syn_rhs1 syn_rhs2) empty   -- nothing interesting to say
-
   -- This allows abstract 'data T a' to be implemented using 'type T = ...'
   -- and abstract 'class K a' to be implement using 'type K = ...'
   -- See Note [Synonyms implement abstract data]
@@ -1031,6 +1030,17 @@ checkBootTyCon is_boot tc1 tc2
     -- So for now, let it all through (it won't cause segfaults, anyway).
     -- Tracked at #12704.
 
+  -- This allows abstract 'data T :: Nat' to be implemented using
+  -- 'type T = 42' Since the kinds already match (we have checked this
+  -- upfront) all we need to check is that the implementation 'type T
+  -- = ...' defined an actual literal.  See #15138 for the case this
+  -- handles.
+  | not is_boot
+  , isAbstractTyCon tc1
+  , Just (_,ty2) <- synTyConDefn_maybe tc2
+  , isJust (isLitTy ty2)
+  = Nothing
+
   | Just fam_flav1 <- famTyConFlav_maybe tc1
   , Just fam_flav2 <- famTyConFlav_maybe tc2
   = ASSERT(tc1 == tc2)
diff --git a/compiler/types/Type.hs b/compiler/types/Type.hs
index 3a3048d773..ac1c8b9261 100644
--- a/compiler/types/Type.hs
+++ b/compiler/types/Type.hs
@@ -48,6 +48,7 @@ module Type (
 
         mkNumLitTy, isNumLitTy,
         mkStrLitTy, isStrLitTy,
+        isLitTy,
 
         getRuntimeRep_maybe, getRuntimeRepFromKind_maybe,
 
@@ -856,6 +857,11 @@ isStrLitTy ty | Just ty1 <- coreView ty = isStrLitTy ty1
 isStrLitTy (LitTy (StrTyLit s)) = Just s
 isStrLitTy _                    = Nothing
 
+-- | Is this a type literal (symbol or numeric).
+isLitTy :: Type -> Maybe TyLit
+isLitTy ty | Just ty1 <- coreView ty = isLitTy ty1
+isLitTy (LitTy l)                    = Just l
+isLitTy _                            = Nothing
 
 -- | Is this type a custom user error?
 -- If so, give us the kind and the error message.
diff --git a/testsuite/tests/backpack/should_run/T15138.bkp b/testsuite/tests/backpack/should_run/T15138.bkp
new file mode 100644
index 0000000000..7cb9eeb804
--- /dev/null
+++ b/testsuite/tests/backpack/should_run/T15138.bkp
@@ -0,0 +1,36 @@
+{-# LANGUAGE ConstraintKinds             #-}
+{-# LANGUAGE DataKinds                   #-}
+{-# LANGUAGE KindSignatures              #-}
+{-# LANGUAGE MultiParamTypeClasses       #-}
+{-# LANGUAGE FlexibleInstances           #-}
+{-# LANGUAGE TypeFamilies                #-}
+{-# LANGUAGE FlexibleContexts            #-}
+
+unit indef where
+
+   signature Abstract where
+     import GHC.TypeLits
+     data NatType :: Nat
+
+   module Util where
+     import Abstract
+     import Data.Proxy
+     import GHC.TypeLits
+
+     natTypeToInteger :: KnownNat NatType => Proxy NatType -> Integer
+     natTypeToInteger = natVal
+
+unit concrete where
+   module Concrete where
+     type NatType = 32
+
+
+unit main where
+   dependency indef[Abstract=concrete:Concrete] (Util as MyUtil)
+
+   module Main where
+     import Data.Proxy
+     import MyUtil
+
+     main :: IO ()
+     main = do print $ natTypeToInteger Proxy
diff --git a/testsuite/tests/backpack/should_run/T15138.stdout b/testsuite/tests/backpack/should_run/T15138.stdout
new file mode 100644
index 0000000000..f5c89552bd
--- /dev/null
+++ b/testsuite/tests/backpack/should_run/T15138.stdout
@@ -0,0 +1 @@
+32
diff --git a/testsuite/tests/backpack/should_run/all.T b/testsuite/tests/backpack/should_run/all.T
index 48ed0c6310..61277b8f31 100644
--- a/testsuite/tests/backpack/should_run/all.T
+++ b/testsuite/tests/backpack/should_run/all.T
@@ -8,3 +8,4 @@ test('bkprun07', normal, backpack_run, [''])
 test('bkprun08', normal, backpack_run, [''])
 test('bkprun09', normal, backpack_run, ['-O'])
 test('T13955', normal, backpack_run, [''])
+test('T15138', normal, backpack_run, [''])