Opened 15 months ago
Last modified 14 months ago
#11995 new bug
Can't infer type
Reported by: | Iceland_jack | Owned by: | |
---|---|---|---|
Priority: | normal | Milestone: | |
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 (2)
comment:1 Changed 14 months ago by
Description: | modified (diff) |
---|---|
Keywords: | TypeInType added |
comment:2 Changed 14 months ago by
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: