diff options
| author | Richard Eisenberg <rae@cs.brynmawr.edu> | 2018-07-19 00:16:13 -0400 |
|---|---|---|
| committer | Richard Eisenberg <rae@cs.brynmawr.edu> | 2018-07-23 10:23:11 -0400 |
| commit | af624071fa063158d6e963e171280676f9c0a0b0 (patch) | |
| tree | 44280edcacae6538fc241e64dff37071724c1ae3 /compiler/types/Coercion.hs | |
| parent | a606750b36862367d038813f9fe7170f93c36222 (diff) | |
| download | haskell-af624071fa063158d6e963e171280676f9c0a0b0.tar.gz | |
Fix some casts.
This fixes #15346, and is a team effort between Ryan Scott and
myself (mostly Ryan). We discovered two errors related to FC's
"push" rules, one in the TPush rule (as implemented in pushCoTyArg)
and one in KPush rule (it shows up in liftCoSubstVarBndr).
The solution: do what the paper says, instead of whatever random
thoughts popped into my head as I was actually implementing.
Also fixes #15419, which is actually the same underlying problem.
Test case: dependent/should_compile/T{15346,15419}.
Diffstat (limited to 'compiler/types/Coercion.hs')
| -rw-r--r-- | compiler/types/Coercion.hs | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/compiler/types/Coercion.hs b/compiler/types/Coercion.hs index 2ca5151f78..1557ce0c88 100644 --- a/compiler/types/Coercion.hs +++ b/compiler/types/Coercion.hs @@ -1812,7 +1812,7 @@ liftCoSubstVarBndrUsing fun lc@(LC subst cenv) old_var Pair k1 _ = coercionKind eta new_var = uniqAway (getTCvInScope subst) (setVarType old_var k1) - lifted = Refl (TyVarTy new_var) + lifted = GRefl Nominal (TyVarTy new_var) (MCo eta) new_cenv = extendVarEnv cenv old_var lifted -- | Is a var in the domain of a lifting context? |