Add exception for `KnownNat` and `KnownSymbol` in super classes.
authorIavor S. Diatchki <diatchki@galois.com>
Thu, 16 Apr 2015 16:47:28 +0000 (09:47 -0700)
committerIavor S. Diatchki <diatchki@galois.com>
Thu, 16 Apr 2015 16:47:28 +0000 (09:47 -0700)
The situation is similar to `Typeable`---we can't set the evidence
outside the solver because we have custom solving rules.  This is safe
because the computed super-class instances can't possibly depend
on the new instance.

compiler/typecheck/TcInstDcls.hs
testsuite/tests/typecheck/should_compile/TcCustomSolverSuper.hs [new file with mode: 0644]
testsuite/tests/typecheck/should_compile/all.T

index b1a28c7..119998a 100644 (file)
@@ -43,7 +43,8 @@ import Class
 import Var
 import VarEnv
 import VarSet
-import PrelNames  ( typeableClassName, genericClassNames )
+import PrelNames  ( typeableClassName, genericClassNames
+                  , knownNatClassName, knownSymbolClassName )
 import Bag
 import BasicTypes
 import DynFlags
@@ -1065,9 +1066,10 @@ tcSuperClasses dfun_id cls tyvars dfun_evs inst_tys dfun_ev_binds fam_envs sc_th
       | (sc_co, norm_sc_pred) <- normaliseType fam_envs Nominal sc_pred
                                  -- sc_co :: sc_pred ~ norm_sc_pred
       , ClassPred cls tys <- classifyPredType norm_sc_pred
-      , className cls /= typeableClassName
-        -- `Typeable` has custom solving rules, which is why we exclude it
-        -- from the short cut, and fall through to calling the solver.
+      , not (usesCustomSolver cls)
+        -- Some classes (e.g., `Typeable`, `KnownNat`) have custom solving
+        -- rules, which is why we exclude it from the short cut,
+        -- and fall through to calling the solver.
 
       = do { sc_ev_tm <- emit_sc_cls_pred norm_sc_pred cls tys
            ; sc_ev_id <- newEvVar sc_pred
@@ -1109,6 +1111,18 @@ tcSuperClasses dfun_id cls tyvars dfun_evs inst_tys dfun_ev_binds fam_envs sc_th
                        ; traceTc "tcSuperClass 3" (ppr sc_pred $$ ppr sc_ev)
                        ; return (ctEvTerm sc_ev) } }
 
+
+
+-- | Do we use a custom solver, which is safe to use when solving super-class
+-- constraints.
+usesCustomSolver :: Class -> Bool
+usesCustomSolver cls = name == typeableClassName
+                    || name == knownNatClassName
+                    || name == knownSymbolClassName
+  where
+  name = className cls
+
+
 -------------------
 checkInstConstraints :: (EvBindsVar -> TcM result)
                      -> TcM (Implication, result)
diff --git a/testsuite/tests/typecheck/should_compile/TcCustomSolverSuper.hs b/testsuite/tests/typecheck/should_compile/TcCustomSolverSuper.hs
new file mode 100644 (file)
index 0000000..c401e1c
--- /dev/null
@@ -0,0 +1,24 @@
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE FlexibleInstances #-}
+module TcCustomSolverSuper where
+
+import GHC.TypeLits
+import Data.Typeable
+
+{-
+
+When solving super-class instances, GHC solves the evidence without
+using the solver (see `tcSuperClasses` in `TcInstDecls`).
+
+However, some classes need to be excepted from this behavior,
+as they have custom solving rules, and this test checks that
+we got this right.
+-}
+
+
+class (Typeable x, KnownNat x)    => C x
+class (Typeable x, KnownSymbol x) => D x
+
+instance C 2
+instance D "2"
+
index d7b3fad..e60fdc8 100644 (file)
@@ -449,3 +449,4 @@ test('T10177', normal, compile, [''])
 test('T10185', expect_broken(10185), compile, [''])
 test('T10195', normal, compile, [''])
 test('T10109', normal, compile, [''])
+test('TcCustomSolverSuper', normal, compile, [''])