Opened 3 years ago
Closed 16 months ago
#11995 closed bug (fixed)
Can't infer type
Reported by: | Iceland_jack | Owned by: | |
---|---|---|---|
Priority: | normal | Milestone: | 8.2.2 |
Component: | Compiler (Type checker) | Version: | 8.1 |
Keywords: | TypeInType | Cc: | |
Operating System: | Unknown/Multiple | Architecture: | Unknown/Multiple |
Type of failure: | None/Unknown | Test Case: | |
Blocked By: | Blocking: | ||
Related Tickets: | Differential Rev(s): | ||
Wiki Page: |
Description (last modified by )
{-# LANGUAGE RankNTypes, LambdaCase, TypeOperators, TypeInType, UnicodeSyntax, GADTs #-} module T11995 where import Data.Kind data NP :: forall k. (ĸ → Type) → ([k] → Type) where Nil :: NP f '[] (:*) :: f x → NP f xs → NP f (x:xs) newtype K a b = K a deriving Show unK (K a) = a h'collapse :: NP (K a) xs -> [a] h'collapse = \case Nil -> [] K x:*xs -> x : h'collapse xs
if we replace xs
by an underscore:
tJN0.hs:13:29-30: error: … • Could not deduce: (xs :: [ĸ]) ~~ ((':) ĸ x xs :: [ĸ]) from the context: ((k :: *) ~~ (ĸ :: *), (t :: [k]) ~~ ((':) ĸ x xs :: [ĸ])) bound by a pattern with constructor: :* :: forall k (f :: k -> *) (x :: k) (xs :: [k]). f x -> NP k k f xs -> NP k k f ((':) k x xs), in a case alternative at /tmp/tJN0.hs:13:3-9 ‘xs’ is a rigid type variable bound by a pattern with constructor: :* :: forall k (f :: k -> *) (x :: k) (xs :: [k]). f x -> NP k k f xs -> NP k k f ((':) k x xs), in a case alternative at /tmp/tJN0.hs:13:3 Expected type: NP ĸ k (K ĸ a) t Actual type: NP ĸ ĸ (K ĸ a) xs • In the first argument of ‘h'collapse’, namely ‘xs’ In the second argument of ‘(:)’, namely ‘h'collapse xs’ In the expression: x : h'collapse xs • Relevant bindings include xs :: NP ĸ ĸ (K ĸ a) xs (bound at /tmp/tJN0.hs:13:8) h'collapse :: NP ĸ k (K ĸ a) t -> [a] (bound at /tmp/tJN0.hs:11:1) Compilation failed.
Should it not be able to infer that?
The Glorious Glasgow Haskell Compilation System, version 8.1.20160419
Change History (5)
comment:1 Changed 2 years ago by
Description: | modified (diff) |
---|---|
Keywords: | TypeInType added |
comment:2 Changed 2 years ago by
comment:5 Changed 16 months ago by
Milestone: | → 8.2.2 |
---|---|
Resolution: | → fixed |
Status: | merge → closed |
Merged to ghc-8.2
.
Note: See
TracTickets for help on using
tickets.
This is correct behavior.
Though I failed to find a mention of the fact in either the user manual or in the Haskell 2010 report, a function can use polymorphic recursion only when given a type signature. The Wikipedia page on polymorphic recursion may be helpful. When you stub out the
xs
with an underscore, GHC considers the type signature to be incomplete and it does type inference -- not type checking -- on the function. Your function is polymorphically recursive, and so this fails.Still remaining to do: