Fix decompsePiCos and visible type application
authorSimon Peyton Jones <simonpj@microsoft.com>
Mon, 9 Jul 2018 16:20:06 +0000 (17:20 +0100)
committerSimon Peyton Jones <simonpj@microsoft.com>
Tue, 10 Jul 2018 08:28:43 +0000 (09:28 +0100)
Trac #15343 was caused by two things

First, in TcHsType.tcHsTypeApp, which deals with the type argment
in visible type application, we were failing to call
solveLocalEqualities. But the type argument is like a user type
signature so it's at least inconsitent not to do so.

I thought that would nail it.  But it didn't. It turned out that we
were ended up calling decomposePiCos on a type looking like this
    (f |> co) Int

where co :: (forall a. ty) ~ (t1 -> t2)

Now, 'co' is insoluble, and we'll report that later.  But meanwhile
we don't want to crash in decomposePiCos.

My fix involves keeping track of the type on both sides of the
coercion, and ensuring that the outer shape matches before
decomposing.  I wish there was a simpler way to do this. But
I think this one is at least robust.

I suppose it is possible that the decomposePiCos fix would
have cured the original report, but I'm leaving the one-line
tcHsTypeApp fix in too because it just seems more consistent.

compiler/typecheck/TcFlatten.hs
compiler/typecheck/TcHsType.hs
compiler/types/Coercion.hs
compiler/types/Coercion.hs-boot
compiler/types/Type.hs
testsuite/tests/dependent/should_fail/T15343.hs [new file with mode: 0644]
testsuite/tests/dependent/should_fail/T15343.stderr [new file with mode: 0644]
testsuite/tests/dependent/should_fail/all.T

index ee13091..529fbaf 100644 (file)
@@ -1315,10 +1315,16 @@ flatten_args_slow orig_binders orig_inner_ki orig_fvs orig_roles orig_tys
     go acc_xis acc_cos lc [] inner_ki roles tys
       | Just k   <- tcGetTyVar_maybe inner_ki
       , Just co1 <- liftCoSubstTyVar lc Nominal k
-      = do { let Pair flattened_kind _ = coercionKind co1
-                 (arg_cos, res_co)     = decomposePiCos flattened_kind tys co1
-                 casted_tys            = zipWith mkCastTy tys arg_cos
+      = do { let co1_kind              = coercionKind co1
+                 (arg_cos, res_co)     = decomposePiCos co1 co1_kind tys
+                 casted_tys            = ASSERT2( equalLength tys arg_cos
+                                                , ppr tys $$ ppr arg_cos )
+                                         zipWith mkCastTy tys arg_cos
+                    -- In general decomposePiCos can return fewer cos than tys,
+                    -- but not here; see "If we're at all well-typed..."
+                    -- in Note [Last case in flatten_args].  Hence the ASSERT.
                  zapped_lc             = zapLiftingContext lc
+                 Pair flattened_kind _ = co1_kind
                  (bndrs, new_inner)    = splitPiTys flattened_kind
 
            ; (xis_out, cos_out, res_co_out)
index 7e5fcef..463c7e0 100644 (file)
@@ -356,7 +356,10 @@ tcHsTypeApp :: LHsWcType GhcRn -> Kind -> TcM Type
 -- See Note [Recipe for checking a signature] in TcHsType
 tcHsTypeApp wc_ty kind
   | HsWC { hswc_ext = sig_wcs, hswc_body = hs_ty } <- wc_ty
-  = do { ty <- tcWildCardBindersX newWildTyVar Nothing sig_wcs $ \ _ ->
+  = do { ty <- solveLocalEqualities $
+               -- We are looking at a user-written type, very like a
+               -- signature so we want to solve its equalities right now
+               tcWildCardBindersX newWildTyVar Nothing sig_wcs $ \ _ ->
                tcCheckLHsType hs_ty kind
        ; ty <- zonkPromoteType ty
        ; checkValidType TypeAppCtxt ty
index 8493a4a..2ca5151 100644 (file)
@@ -271,43 +271,71 @@ decomposeFunCo r co = ASSERT2( all_ok, ppr co )
     Pair s1t1 s2t2 = coercionKind co
     all_ok = isFunTy s1t1 && isFunTy s2t2
 
--- | Decompose a function coercion, either a dependent one or a non-dependent one.
--- This is useful when you are trying to build (ty1 |> co) ty2 ty3 ... tyn, but
--- you are pulling the coercions to the right. For example of why you might want
--- to do so, see Note [Respecting definitional equality] in TyCoRep.
--- This might return *fewer* coercions than there are arguments, if the kind provided
--- doesn't have enough binders.
--- The types passed in are the ty2 ... tyn. If the results are (arg_cos, res_co),
--- then you should build
--- @(ty1 (ty2 |> arg_cos1) (ty3 |> arg_cos2) ... (tym |> arg_com)|> res_co) tym+1 ... tyn@.
-decomposePiCos :: Kind  -- of the function (ty1), used only to tell -> from ∀ from other
-               -> [Type] -> CoercionN -> ([CoercionN], CoercionN)
-decomposePiCos orig_kind orig_args orig_co = go [] orig_subst orig_kind orig_args orig_co
+{- Note [Pushing a coercion into a pi-type]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Suppose we have this:
+    (f |> co) t1 .. tn
+Then we want to push the coercion into the arguments, so as to make
+progress. For example of why you might want to do so, see Note
+[Respecting definitional equality] in TyCoRep.
+
+This is done by decomposePiCos.  Specifically, if
+    decomposePiCos co [t1,..,tn] = ([co1,...,cok], cor)
+then
+    (f |> co) t1 .. tn   =   (f (t1 |> co1) ... (tk |> cok)) |> cor) t(k+1) ... tn
+
+Notes:
+
+* k can be smaller than n! That is decomposePiCos can return *fewer*
+  coercions than there are arguments (ie k < n), if the kind provided
+  doesn't have enough binders.
+
+* If there is a type error, we might see
+       (f |> co) t1
+  where co :: (forall a. ty) ~ (ty1 -> ty2)
+  Here 'co' is insoluble, but we don't want to crash in decoposePiCos.
+  So decomposePiCos carefully tests both sides of the coercion to check
+  they are both foralls or both arrows.  Not doing this caused Trac #15343.
+-}
+
+decomposePiCos :: HasDebugCallStack
+               => CoercionN -> Pair Type  -- Coercion and its kind
+               -> [Type]
+               -> ([CoercionN], CoercionN)
+-- See Note [Pushing a coercion into a pi-type]
+decomposePiCos orig_co (Pair orig_k1 orig_k2) orig_args
+  = go [] (orig_subst,orig_k1) orig_co (orig_subst,orig_k2) orig_args
   where
-    orig_subst = mkEmptyTCvSubst $ mkInScopeSet $ tyCoVarsOfTypes (orig_kind : orig_args)
-                                                  `unionVarSet` tyCoVarsOfCo orig_co
-
-    go :: [CoercionN]   -- accumulator for argument coercions, reversed
-       -> TCvSubst      -- instantiating substitution
-       -> Kind          -- of the function being applied (unsubsted)
-       -> [Type]        -- arguments to that function
-       -> CoercionN     -- coercion originally applied to the function
+    orig_subst = mkEmptyTCvSubst $ mkInScopeSet $
+                 tyCoVarsOfTypes orig_args `unionVarSet` tyCoVarsOfCo orig_co
+
+    go :: [CoercionN]      -- accumulator for argument coercions, reversed
+       -> (TCvSubst,Kind)  -- Lhs kind of coercion
+       -> CoercionN        -- coercion originally applied to the function
+       -> (TCvSubst,Kind)  -- Rhs kind of coercion
+       -> [Type]           -- Arguments to that function
        -> ([CoercionN], Coercion)
-    go acc_arg_cos subst  ki  (ty:tys) co
-      | Just (kv, inner_ki) <- splitForAllTy_maybe ki
-        -- know       co :: (forall a:s1.t1) ~ (forall b:s2.t2)
-        --      function :: forall a:s1.t1
-        --                  (the function is not passed to decomposePiCos)
-        --            ty :: s2
-        -- need   arg_co :: s2 ~ s1
-        --        res_co :: t1[ty |> arg_co / a] ~ t2[ty / b]
-      = let arg_co = mkNthCo Nominal 0 (mkSymCo co)
-            res_co = mkInstCo co (mkGReflLeftCo Nominal ty arg_co)
-            subst' = extendTCvSubst subst kv ty
+    -- Invariant:  co :: subst1(k2) ~ subst2(k2)
+
+    go acc_arg_cos (subst1,k1) co (subst2,k2) (ty:tys)
+      | Just (a, t1) <- splitForAllTy_maybe k1
+      , Just (b, t2) <- splitForAllTy_maybe k2
+        -- know     co :: (forall a:s1.t1) ~ (forall b:s2.t2)
+        --    function :: forall a:s1.t1   (the function is not passed to decomposePiCos)
+        --           a :: s1
+        --           b :: s2
+        --          ty :: s2
+        -- need arg_co :: s2 ~ s1
+        --      res_co :: t1[ty |> arg_co / a] ~ t2[ty / b]
+      = let arg_co  = mkNthCo Nominal 0 (mkSymCo co)
+            res_co  = mkInstCo co (mkGReflLeftCo Nominal ty arg_co)
+            subst1' = extendTCvSubst subst1 a (ty `CastTy` arg_co)
+            subst2' = extendTCvSubst subst2 b ty
         in
-        go (arg_co : acc_arg_cos) subst' inner_ki tys res_co
+        go (arg_co : acc_arg_cos) (subst1', t1) res_co (subst2', t2) tys
 
-      | Just (_arg_ki, res_ki) <- splitFunTy_maybe ki
+      | Just (_s1, t1) <- splitFunTy_maybe k1
+      , Just (_s2, t2) <- splitFunTy_maybe k2
         -- know     co :: (s1 -> t1) ~ (s2 -> t2)
         --    function :: s1 -> t1
         --          ty :: s2
@@ -316,19 +344,17 @@ decomposePiCos orig_kind orig_args orig_co = go [] orig_subst orig_kind orig_arg
       = let (sym_arg_co, res_co) = decomposeFunCo Nominal co
             arg_co               = mkSymCo sym_arg_co
         in
-        go (arg_co : acc_arg_cos) subst res_ki tys res_co
+        go (arg_co : acc_arg_cos) (subst1,t1) res_co (subst2,t2) tys
 
-      | let substed_ki = substTy subst ki
-      , isPiTy substed_ki
-        -- This might happen if we have to substitute in order to see that the kind
-        -- is a Π-type.
-      = let subst'     = zapTCvSubst subst
-        in
-        go acc_arg_cos subst' substed_ki (ty:tys) co
+      | not (isEmptyTCvSubst subst1) || not (isEmptyTCvSubst subst2)
+      = go acc_arg_cos (zapTCvSubst subst1, substTy subst1 k1)
+                       co
+                       (zapTCvSubst subst2, substTy subst1 k2)
+                       (ty:tys)
 
       -- tys might not be empty, if the left-hand type of the original coercion
       -- didn't have enough binders
-    go acc_arg_cos _subst _ki _tys co = (reverse acc_arg_cos, co)
+    go acc_arg_cos _ki1 co _ki2 _tys = (reverse acc_arg_cos, co)
 
 -- | Attempts to obtain the type variable underlying a 'Coercion'
 getCoVar_maybe :: Coercion -> Maybe CoVar
index 6e6acd7..89aab44 100644 (file)
@@ -38,7 +38,7 @@ mkAxiomRuleCo :: CoAxiomRule -> [Coercion] -> Coercion
 isGReflCo :: Coercion -> Bool
 isReflCo :: Coercion -> Bool
 isReflexiveCo :: Coercion -> Bool
-decomposePiCos :: Kind -> [Type] -> Coercion -> ([Coercion], Coercion)
+decomposePiCos :: HasDebugCallStack => Coercion -> Pair Type -> [Type] -> ([Coercion], Coercion)
 coVarKindsTypesRole :: HasDebugCallStack => CoVar -> (Kind, Kind, Type, Type, Role)
 coVarRole :: CoVar -> Role
 
index 45b1b74..0833665 100644 (file)
@@ -669,7 +669,7 @@ the type checker (e.g. when matching type-function equations).
 mkAppTy :: Type -> Type -> Type
   -- See Note [Respecting definitional equality], invariant (EQ1).
 mkAppTy (CastTy fun_ty co) arg_ty
-  | ([arg_co], res_co) <- decomposePiCos (typeKind fun_ty) [arg_ty] co
+  | ([arg_co], res_co) <- decomposePiCos co (coercionKind co) [arg_ty]
   = (fun_ty `mkAppTy` (arg_ty `mkCastTy` arg_co)) `mkCastTy` res_co
 
 mkAppTy (TyConApp tc tys) ty2 = mkTyConApp tc (tys ++ [ty2])
@@ -691,7 +691,7 @@ mkAppTys (CastTy fun_ty co) arg_tys  -- much more efficient then nested mkAppTy
                                      -- in TyCoRep
   = foldl AppTy ((mkAppTys fun_ty casted_arg_tys) `mkCastTy` res_co) leftovers
   where
-    (arg_cos, res_co) = decomposePiCos (typeKind fun_ty) arg_tys co
+    (arg_cos, res_co) = decomposePiCos co (coercionKind co) arg_tys
     (args_to_cast, leftovers) = splitAtList arg_cos arg_tys
     casted_arg_tys = zipWith mkCastTy args_to_cast arg_cos
 mkAppTys (TyConApp tc tys1) tys2 = mkTyConApp tc (tys1 ++ tys2)
diff --git a/testsuite/tests/dependent/should_fail/T15343.hs b/testsuite/tests/dependent/should_fail/T15343.hs
new file mode 100644 (file)
index 0000000..9bb59c8
--- /dev/null
@@ -0,0 +1,14 @@
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TypeApplications #-}
+{-# LANGUAGE TypeInType #-}
+module T15343 where
+
+import Data.Kind
+
+elimSing :: forall (p :: forall z. z). p
+elimSing = undefined
+
+data WhySym :: Type -> Type
+
+hsym = elimSing @WhySym
diff --git a/testsuite/tests/dependent/should_fail/T15343.stderr b/testsuite/tests/dependent/should_fail/T15343.stderr
new file mode 100644 (file)
index 0000000..79d81e5
--- /dev/null
@@ -0,0 +1,7 @@
+
+T15343.hs:14:18: error:
+    • Expecting one more argument to ‘WhySym’
+      Expected kind ‘forall z. z’, but ‘WhySym’ has kind ‘* -> *’
+    • In the type ‘WhySym’
+      In the expression: elimSing @WhySym
+      In an equation for ‘hsym’: hsym = elimSing @WhySym
index 1bc3f42..59d8037 100644 (file)
@@ -33,3 +33,5 @@ test('InferDependency', normal, compile_fail, [''])
 test('T15245', normal, compile_fail, [''])
 test('T15215', normal, compile_fail, [''])
 test('T15308', normal, compile_fail, ['-fno-print-explicit-kinds'])
+test('T15343', normal, compile_fail, [''])
+