Commit 7a439e7b authored by Richard Eisenberg's avatar Richard Eisenberg Committed by Ben Gamari

Fix #15787 by squashing a coercion hole.

In type-incorrect code, we can sometimes let a coercion
hole make it through the zonker. If this coercion hole then
ends up in the environment (e.g., in the type of a data
constructor), then it causes trouble later.

This patch avoids trouble by substituting the coercion hole
for its representative CoVar. Really, any coercion would do,
but the CoVar was very handy.

test case: polykinds/T15787

(cherry picked from commit 4427315a)
parent cfc3ad1f
......@@ -1673,7 +1673,9 @@ zonkCoHole env hole@(CoercionHole { ch_ref = ref, ch_co_var = cv })
, text "Type-correct unfilled coercion hole"
<+> ppr hole )
; cv' <- zonkCoVar cv
; return $ mkHoleCo (hole { ch_co_var = cv' }) } }
; return $ mkCoVarCo cv' } }
-- This will be an out-of-scope variable, but keeping
-- this as a coercion hole led to #15787
zonk_tycomapper :: TyCoMapper ZonkEnv TcM
zonk_tycomapper = TyCoMapper
......
{-# Language RankNTypes #-}
{-# Language TypeApplications #-}
{-# Language DataKinds #-}
{-# Language PolyKinds #-}
{-# Language GADTs #-}
{-# Language TypeFamilies #-}
import Data.Kind
class Ríki (ob :: Type) where
type Hom :: ob -> ob -> Type
data
Kl_kind :: forall ob . (ob -> ob) -> ob -> Type where
Kl :: k -> Kl_kind (m :: ob -> ob) k
type family
UnKl (kl :: Kl_kind m k) = (res :: k) where
UnKl (Kl a) = a
T15787.hs:15:43: error:
• Expected kind ‘ob’, but ‘k’ has kind ‘*’
• In the second argument of ‘Kl_kind’, namely ‘k’
In the type ‘Kl_kind (m :: ob -> ob) k’
In the definition of data constructor ‘Kl’
......@@ -193,3 +193,4 @@ test('T15116a', normal, compile_fail, [''])
test('T15170', normal, compile, [''])
test('T14939', normal, compile, ['-O'])
test('T15577', normal, compile_fail, ['-O'])
test('T15787', normal, compile_fail, [''])
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment