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)
commitaedbf7f1c402ecbcb5ff192d5fb4dd6dd4771bf8
tree0e782ee467b45f4914215863a38833849a2b26d8
parentfd0f0334189c0c5c9b186bd1b009f706d3d86086
Fix decompsePiCos and visible type application

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