Opened 6 months ago
Last modified 4 months ago
#14038 new bug
TypeApplications regression in GHC HEAD: ‘p0’ is untouchable inside the constraints: ()
Reported by: | RyanGlScott | Owned by: | |
---|---|---|---|
Priority: | high | Milestone: | 8.4.1 |
Component: | Compiler (Type checker) | Version: | 8.3 |
Keywords: | TypeApplications | Cc: | goldfire |
Operating System: | Unknown/Multiple | Architecture: | Unknown/Multiple |
Type of failure: | None/Unknown | Test Case: | |
Blocked By: | #14119 | Blocking: | |
Related Tickets: | #13877 | Differential Rev(s): | |
Wiki Page: |
Description
This file:
{-# LANGUAGE AllowAmbiguousTypes #-} {-# LANGUAGE ConstraintKinds #-} {-# LANGUAGE ExistentialQuantification #-} {-# LANGUAGE GADTs #-} {-# LANGUAGE RankNTypes #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TypeApplications #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE TypeInType #-} {-# LANGUAGE TypeOperators #-} module Eliminator where import Data.Kind (Type) data family Sing (a :: k) data instance Sing (z :: [a]) where SNil :: Sing '[] SCons :: Sing x -> Sing xs -> Sing (x:xs) data TyFun :: Type -> Type -> Type type a ~> b = TyFun a b -> Type infixr 0 ~> type family Apply (f :: k1 ~> k2) (x :: k1) :: k2 type a @@ b = Apply a b infixl 9 @@ data FunArrow = (:->) -- ^ '(->)' | (:~>) -- ^ '(~>)' class FunType (arr :: FunArrow) where type Fun (k1 :: Type) arr (k2 :: Type) :: Type class FunType arr => AppType (arr :: FunArrow) where type App k1 arr k2 (f :: Fun k1 arr k2) (x :: k1) :: k2 type FunApp arr = (FunType arr, AppType arr) instance FunType (:->) where type Fun k1 (:->) k2 = k1 -> k2 instance AppType (:->) where type App k1 (:->) k2 (f :: k1 -> k2) x = f x instance FunType (:~>) where type Fun k1 (:~>) k2 = k1 ~> k2 instance AppType (:~>) where type App k1 (:~>) k2 (f :: k1 ~> k2) x = f @@ x infixr 0 -?> type (-?>) (k1 :: Type) (k2 :: Type) (arr :: FunArrow) = Fun k1 arr k2 elimList :: forall (a :: Type) (p :: [a] -> Type) (l :: [a]). Sing l -> p '[] -> (forall (x :: a) (xs :: [a]). Sing x -> Sing xs -> p xs -> p (x:xs)) -> p l elimList = elimListPoly @(:->) elimListTyFun :: forall (a :: Type) (p :: [a] ~> Type) (l :: [a]). Sing l -> p @@ '[] -> (forall (x :: a) (xs :: [a]). Sing x -> Sing xs -> p @@ xs -> p @@ (x:xs)) -> p @@ l elimListTyFun = elimListPoly @(:~>) @_ @p elimListPoly :: forall (arr :: FunArrow) (a :: Type) (p :: ([a] -?> Type) arr) (l :: [a]). FunApp arr => Sing l -> App [a] arr Type p '[] -> (forall (x :: a) (xs :: [a]). Sing x -> Sing xs -> App [a] arr Type p xs -> App [a] arr Type p (x:xs)) -> App [a] arr Type p l elimListPoly SNil pNil _ = pNil elimListPoly (SCons x (xs :: Sing xs)) pNil pCons = pCons x xs (elimListPoly @arr @a @p @xs xs pNil pCons)
Typechecks in GHC 8.2.1 without issue, but fails in GHC HEAD:
$ ghc5/inplace/bin/ghc-stage2 --interactive Bug.hs GHCi, version 8.3.20170725: http://www.haskell.org/ghc/ :? for help Loaded GHCi configuration from /home/rgscott/.ghci [1 of 1] Compiling Eliminator ( Bug.hs, interpreted ) Bug.hs:59:12: error: • Couldn't match type ‘p0’ with ‘p’ because type variables ‘a1’, ‘p’ would escape their scope These (rigid, skolem) type variables are bound by the type signature for: elimList :: forall a1 (p :: [a1] -> *) (l :: [a1]). Sing l -> p '[] -> (forall (x :: a1) (xs :: [a1]). Sing x -> Sing xs -> p xs -> p (x : xs)) -> p l at Bug.hs:(54,1)-(58,15) Expected type: Sing l -> p '[] -> (forall (x :: a1) (xs :: [a1]). Sing x -> Sing xs -> p xs -> p (x : xs)) -> p l Actual type: Sing l -> App [a1] (':->) * p0 '[] -> (forall (x :: a1) (xs :: [a1]). Sing x -> Sing xs -> App [a1] (':->) * p0 xs -> App [a1] (':->) * p0 (x : xs)) -> App [a1] (':->) * p0 l • In the expression: elimListPoly @(:->) In an equation for ‘elimList’: elimList = elimListPoly @(:->) • Relevant bindings include elimList :: Sing l -> p '[] -> (forall (x :: a1) (xs :: [a1]). Sing x -> Sing xs -> p xs -> p (x : xs)) -> p l (bound at Bug.hs:59:1) | 59 | elimList = elimListPoly @(:->) | ^^^^^^^^^^^^^^^^^^^ Bug.hs:59:12: error: • Couldn't match type ‘p0’ with ‘p’ ‘p0’ is untouchable inside the constraints: () bound by a type expected by the context: forall (x :: a1) (xs :: [a1]). Sing x -> Sing xs -> App [a1] (':->) * p0 xs -> App [a1] (':->) * p0 (x : xs) at Bug.hs:59:12-30 ‘p’ is a rigid type variable bound by the type signature for: elimList :: forall a1 (p :: [a1] -> *) (l :: [a1]). Sing l -> p '[] -> (forall (x :: a1) (xs :: [a1]). Sing x -> Sing xs -> p xs -> p (x : xs)) -> p l at Bug.hs:(54,1)-(58,15) Expected type: Sing x -> Sing xs -> App [a1] (':->) * p0 xs -> App [a1] (':->) * p0 (x : xs) Actual type: Sing x -> Sing xs -> p xs -> p (x : xs) • In the expression: elimListPoly @(:->) In an equation for ‘elimList’: elimList = elimListPoly @(:->) • Relevant bindings include elimList :: Sing l -> p '[] -> (forall (x :: a1) (xs :: [a1]). Sing x -> Sing xs -> p xs -> p (x : xs)) -> p l (bound at Bug.hs:59:1) | 59 | elimList = elimListPoly @(:->) | ^^^^^^^^^^^^^^^^^^^
A workaround is to explicitly apply p
with TypeApplications
in line 59:
elimList = elimListPoly @(:->) @_ @p
Change History (14)
comment:1 Changed 6 months ago by
Related Tickets: | → #13877 |
---|
comment:2 Changed 6 months ago by
Richard, in a -DDEBUG
compiler this falls over with
Following filled tyvar a_a225[tau:2] = a_a220[sk:2] Unfilled tyvar a_a220[sk:2] flatten/appty (p0_a226[tau:2] |> T14038.D:R:Funk1:->k2[0] <k1>_N <k2>_N) '[] p0_a226[tau:2] '[] nominal nominal flatten } p0_a226[tau:2] '[] New coercion hole: a23h Emitting new coercion holeghc-stage1: panic! (the 'impossible' happened) (GHC version 8.3.20170726 for x86_64-unknown-linux): piResultTy Fun [a_a220[sk:2]] (':->) * '[] Call stack: ?callStack, called at compiler/utils/Util.hs:1394:50 in ghc:Util prettyCurrentCallStack, called at compiler/utils/Outputable.hs:1133:58 in ghc:Outputable callStackDoc, called at compiler/utils/Outputable.hs:1137:37 in ghc:Outputable pprPanic, called at compiler/types/Type.hs:949:35 in ghc:Type Please report this as a GHC bug: http://www.haskell.org/ghc/reportabug
I think what is happening is that we start with (p0_a226 |> co) '[]
,
where p0_a226 :: Fun [a_a220[sk:2]] (':->) *
, and co
casts it to
a function type. But then flattening throws away the cats, apparently,
and we try to form (mkAppTy p0_a226 '[])
, which is simply ill-kinded.
I have (again) lost track of what is supposed to happen here.
comment:3 Changed 6 months ago by
Cc: | goldfire added |
---|
Commit 8e15e3d370e9c253ae0dbb330e25b72cb00cdb76 (Improve error messages around kind mismatches.
) caused this regression.
comment:5 Changed 6 months ago by
This may be fixed by #12919, which I plan to tackle in the next few days.
comment:6 Changed 6 months ago by
My local fix for #12919 does fix this. But then a deeper bug lurks.
The problem is that the App
instance for (:~>)
gets type-checked with a coercion in its patterns. Of course, the type-family matcher can't deal with a coercion pattern -- what would such a thing mean anyway? So it does something stupid. In this case, the stupid thing is that the match result contains an unbound variable, but it could conceivably do a different stupid thing tomorrow.
The solution, of course, is to make sure that type patterns never contain coercions. I've been meaning to do this for a long time, regardless. (I don't think there's a ticket to track the idea, though.) I see two possible approaches:
- Parameterize the code in TcHsType to know whether it's reading a pattern or a normal type, and don't make coercions in patterns.
- Have TcHsType proceed normally, but rip the coercions out after-the-fact.
What to do in the spots where the coercions used to be? Insert bare coercion variables, which can then be solved for. Some perhaps-outdated thoughts on this are here, but those notes were meant more for myself than anyone else.
While we're thinking about this, another question I've pondered for a while: should type patterns be a separate datatype in GHC than Type
? For example, a type pattern never has a type function nor a forall. It won't have meaningful CastTy
s or CoercionTy
s either. With this change, the pure unifier could perhaps be simplified.
In any case, more thought is necessary.
comment:7 Changed 5 months ago by
Blocked By: | 14119 added |
---|
comment:8 Changed 5 months ago by
I've made a new ticket to discuss how to deal with type patterns at #14119, which this ticket is blocked by.
comment:12 Changed 5 months ago by
comment:6 says:
The problem is that the App instance for (:~>) gets type-checked with a coercion in its patterns
Can you boil this out into a simple case? I'm lost.
Have TcHsType proceed normally, but rip the coercions out after-the-fact.
That's what happens in Rules. See DsBinds.decomposeRuleLhs
.
comment:13 Changed 5 months ago by
#13938 may be another manifestation.
It'd be good to nail this one.
If this bug is fixed, we should see if the program in https://ghc.haskell.org/trac/ghc/ticket/13877#comment:2 panics or not, since whether it panics or not is masked by the bug in this ticket.