[GHC] #11506: uType_defer can defer too long
#11506: uType_defer can defer too long -------------------------------------+------------------------------------- Reporter: goldfire | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.1 Keywords: | Operating System: Unknown/Multiple Architecture: | Type of failure: None/Unknown Unknown/Multiple | Test Case: | Blocked By: Blocking: | Related Tickets: Differential Rev(s): | Wiki Page: -------------------------------------+------------------------------------- Here is the test case: {{{ {-# LANGUAGE PolyKinds, ExistentialQuantification, ScopedTypeVariables, TypeFamilies, TypeInType #-} module Bug where import Data.Proxy import Data.Kind type family ProxyType where ProxyType = (Proxy :: Type -> Type) data T = forall a. MkT (ProxyType a) foo (MkT (_ :: Proxy a)) = const True (undefined :: a) }}} This should be accepted. But I get {{{ Bug.hs:13:53: error: • Expected a type, but ‘a’ has kind ‘k10’ • In an expression type signature: a In the second argument of ‘const’, namely ‘(undefined :: a)’ In the expression: const True (undefined :: a) }}} Why should it be accepted? GHC can infer that the existential `a` in `MkT` has kind `Type`. (Indeed this works.) Then, we should unify the pattern signature `Proxy k1 a1` with `ProxyType a2`; the latter expands to `Proxy Type a2` and we get `k1 := Type` and `a1 := a2`, allowing `undefined :: a` to be accepted. Why doesn't it work? When checking the pattern type signature in `foo`, GHC then checks if `ProxyType a2` is a subtype of `Proxy k1 a1`. This check is deferred because of the type family. In a short while, GHC needs to know that `a` has kind `Type` to make sure that `undefined :: a` is well-typed. At this point, it doesn't know that `a` has kind `Type` (because the unification was deferred), and so an error is issued. I'm not sure how to resolve this. This is indeed a consequence of `TypeInType`, but it seems more to do with solver engineering than the new `TypeInType` stuff. And there is an easy workaround: just add a kind signature. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11506 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#11506: uType_defer can defer too long -------------------------------------+------------------------------------- Reporter: goldfire | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.1 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by simonpj): It's more than solver engineering. A pretty fundamental assumption is that a user-writen type signature (at least one without wildcards) specifies a ''fully-defined'' type. No unification variables; a fully defined type. Not necessarily closed; e.g. here the type sig for 'g' is fully defined although it mentions 'a': {{{ f :: forall a. blah f x = let g :: a -> a g x = x in ... }}} But pattern signatures threaten this happy story. They bring into scope a type variable as a name for a type that may not yet be fully defined, and certainly isn't here. Much simpler situations can do this too: {{{ f (x::a, b) = let g :: a -> a g = ... in ... }}} Here `a` will end up being the name of a unification variable. This hasn't caused trouble before, but now it is. If we switched off on- the-fly unification, and did everything in the solver, I bet a lot more instances would pop up. What's irritating is that the ability to name unification variables (or type variables with as-yet-unknown kinds) is not really sought. It's just hard to exclude. One possible solution would be to make pattern signatures do matching (not unification) with the "expected" type, and then insist that the scoped type variable matched a skolem. Another would be to treat type variables bound in this way more like wildards. If we have {{{ f :: _ -> Maybe _ or <expression> :: _ -> Int }}} then we use ''inference'' not checking, and simply use the signature as a "shape" against which the inferred type is matched. So a type signature with any wildcards is NOT treated as a fully defined type. Maybe a type signature with a free type variable bound by a pattern signature should be treated similarly. The machinery to do so is all there now. Uggle. I doubt I'll get to this quickly. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11506#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
participants (1)
-
GHC